Model-Checking Pushdown Automata
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).