Model-Checking Pushdown Automata

Javier Esparza


Pushdown automata (PDA) can be seen not only as language acceptors, but also as processes. As a process, the semantic of a PDA is no longer a language, but a -- possibly infinite -- Kripke structure (or transition system). Temporal logics can be used as query languages to describe properties of this structure. The model-checking problem consists of deciding whether the Kripke structure of a given PDA is model of a given temporal formula or not. Since the Kripke structure associated to a PDA can be infinite, the many existing model-checking techniques for finite structures cannot be applied. Several papers have proposed solutions to the model-checking problem for the modal mu-calculus, a particularly powerful temporal logic, or fragments thereof (Burkart und Steffen 92 und 94, Hungar und Steffen 93, Walukiewicz 96). In the talk I present algorithms for linear and branching-time logics, which I claim are easier to understand than the existing ones. These algorithms rely on a simple result of automata theory which is part of my undergraduate lecture on formal languages. This is joint work with Ahmed Bouajjani and Oded Maler, Verimag (Grenoble).