## 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

## Abstract

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 Maintainer fsttcs20@cse.iitd.ernet.in.
 Conference Systems