Model-Checking LTL with Pushdown Systems

Antonin Kucera

(Masaryk University Brno, Czech Republic)

Pushdown systems can be seen as a very natural model for systems with recursive procedures. Intuitively, the stack carries information about the history of activation records, and the top stack symbol corresponds to the instruction currently being executed. The finite control can, eg, keep auxiliary information about global variables, allocated memory, etc. When abstracting a real program to a pushdown automaton, the if-then-else command is usually replaced by a non-deterministic choice between the two possible branches. Hence, the abstracted model is non-deterministic even if the original program was completely deterministic. As the underlying dynamics of pushdown automata is defined in terms of transition systems, temporal logics can be used to express properties of such systems formally. Linear-time logics (like LTL) are suitable for describing properties of `runs', ie, possible computations. Their advantage over branching-time logics (like CTL) is that one can design rather efficient model-checking algorithms by adapting the automata-theoretic approach of Vardi and Wolper. We present such an algorithm, discussing some issues in detail. In particular, we consider the problem how to interpret atomic LTL propositions on pushdown automata without losing efficiency. We design so-called `regular' interpretations which assign to each atomic proposition of LTL an infinite set of pushdown configurations which is symbolically encodable by a finite-state automaton. We also show how to model-check LTL formulae wrt regular interpretations, presenting the associated complexity bounds. Finally, we also present several examples of practical applicability of our results to problems of data-flow analysis and security problems of JAVA programs.
Tuesday 6th March 2001, 14:00
Robert Recorde Room
Department of Computer Science