Propositional dynamic logic of regular programs

摘要

We introduce a fundamental propositional logical system based on modal logic for describing correctness, termination and equivalence of programs. We define a formal syntax and semantics for the propositional dynamic logic of regular programs and give several consequences of the definition. Principal conclusions are that deciding satisfiability of length n formulas requires time dn/logn for some d > 1, and that satisfiability can be decided in nondeterministic time cn for some c. We provide applications of the decision procedure to regular expressions, Ianov schemes, and classical systems of modal logic.