Publication details

Programming Systems

Gert Smolka

Publications

Teaching

Software

Formalizations

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               

@INPROCEEDINGS{KaminskiEtAl:2011:HPDLDC,
  title = {Correctness and Worst-Case Optimality of Pratt-Style Decision Procedures for Modal and Hybrid Logics},
  author = {Mark Kaminski and Thomas Schneider and Gert Smolka},
  year = {2011},
  month = {Jul},
  editor = {Kai Brünnler and George Metcalfe},
  publisher = {Springer},
  booktitle = {TABLEAUX 2011},
  series = {LNCS (LNAI)},
  volume = {6793},
  pages = {196-210},
  note = {Long version.},
}

Login to edit