Tableaux and Algorithms for Propositional Dynamic Logic with Converse

摘要

This paper presents a prefixed tableaux claculus for Propositional Dynamic Logic with Converse based on a combination of different techniques such as prefixed tableaux for modal logics and model checkers for mu-calculus. We prove the correctness and completeness of the calculus and illustrate its features. We also discuss the transformation of the tableaux method (naively NEXPTIME) into an EXPTIME algorithm.