Publication details

Saarland University Computer Science

Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics

Mark Kaminski, Thomas Schneider, Gert Smolka

TABLEAUX 2011, Vol. 6793 of LNCS (LNAI), pp. 196-210, Springer, July 2011

We extend Pratt's worst-case optimal decision procedure for PDL to a richer logic with nominals, difference modalities, and inverse actions. We prove correctness and worst-case optimality. Our correctness proof is based on syntactic models called demos. The main theorem states that a formula is satisfiable if and only if it is contained in a demo. From this theorem the correctness of the decision procedure is easily obtained. Our development is modular and we extend it stepwise from modal logic with eventualities to the full logic.

Long version.
DOI (LNCS version): 10.1007/978-3-642-22119-4_16

Download PDF        Show BibTeX               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009