Model checking CTL Properties of Pushdown Systems

Igor Walukiewicz

To appear at Foundations of Software Technology and Theoretical Computer Science (FSTTCS2000), New Delhi, India, December 13-15 2000


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 $\a\in L$ decide if $\a$ 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.

Server START Conference Manager
Update Time 14 Aug 2000 at 17:41:23
Start Conference Manager
Conference Systems