Sciweavers

Share
FSTTCS
2000
Springer

Model Checking CTL Properties of Pushdown Systems

9 years 7 months ago
Model Checking CTL Properties of Pushdown Systems
: A pushdown system is a graph G(P) of configurations of a pushdown automaton P. The model checking problem for a logic L is: given a pushdown automaton P and a formula L decide if holds in the vertex of G(P) which is the initial configuration of P. Computation Tree Logic (CTL) and its fragment EF are considered. The model checking problems for CTL and EF are shown to be EXPTIME-complete and PSPACE-complete, respectively.
Igor Walukiewicz
Added 24 Aug 2010
Updated 24 Aug 2010
Type Conference
Year 2000
Where FSTTCS
Authors Igor Walukiewicz
Comments (0)
books