Deterministic propositional dynamic logic: Finite models, complexity, and completeness

摘要

Let p be a formula in deterministic propositional dynamic logic. A decision procedure for the satisfiability of p is given along with a construction of a finite model for every satisfiable p. The decision procedure runs in deterministic time 2cn and the size of the model is bounded by n2 · 4n, where n is the length of p. Finally, a complete axiomatization for deterministic propositional dynamic logic is given, based on the Segerberg axoms for propositional dynamic logic.