Model Checking PDL with Indexed Grammars

Propositional Dynamic Logic (PDL) with Indexed Grammars:

Fischer and Ladner's Propositional Dynamic Logic [1] is a simple modal logic which incorporates regular languages (here: grammars) in the modalities in order to specify valid paths. A formula <G> φ is satisfied by a state s iff there is a path to some state t labeled with a word in the language induced by G in which φ holds. PDL satisfiability is EXPTIME-complete. Harel et al. extended PDL to context-free languages (CFL) and showed that it is highly undecidable [2]. In fact, the addition of certain single context-free languages to regular PDL suffices to establish undecidability.

Model checking however is in PTIME as shown by Lange [3]. The investigation of the model checking problem for even more expressive languages has not been proposed so far. It is not difficult to see that an extension to context-sensitive languages (CSL) renders the problem undecidable. An interesting class located strictly between CFL and CSL are the indexed languages (IL) for which PDL model checking is EXPTIME complete.

Syntax:

The following BNF defines the syntax:

φ ::= p | ¬ φ | φ ∨ φ | <G> φ

,where G is an (indexed) grammar as defined in [4]. See also the slides of this talk for an introduction plus a description of the model checking algorithm (note that we only show PSPACE hardness there).

Download & Documentation:

An implementation of the model checking algorithm is available on the tool documentation page.
The tool comes with a model specification language in which the input for the model checkers can be defined, i.e. a labeled transition system and a specification formula.

For installation and other instructions see the included README file or follow the links above.

Literature:

1. M.J. Fischer and R.E. Ladner.
   Propositional Dynamic Logic of Regular Programs.
   In: Journal of Computer and System Sciences, 18:194-211, 1979
   
2. D. Harel and A. Pnueli and J. Stavi.
   Propositional Dynamic Logic of Nonregular Programs.
   In: Journal of Computer and System Sciences, 26(2):222-243, 1983
   
3. M. Lange.
   Model Checking Propositional Dynamic Logic with All Extras.
   In: Journal of Applied Logic,, 4(1):39-49, 2005
   
4. A. Aho.
   Indexed Grammars - An Extension of Context-Free Grammars.
   In: Journal of the ACM, 15(4):647-671, 1968