Bisimilar and Logically Equivalent Programs in PDL

AbstractIn standard Propositional Dynamic Logic (PDL) literature [D. Harel and D. Kozen and J. Tiuryn. Dynamic Logics. MIT Press, 2000; R. Goldblatt. Logics of Time and Computation. CSLI Lecture Notes 7. Stanford, 1992; P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Theoretical Tracts in Computer Science. Cambridge University Press, 2001] the semantics is given by Labeled Transition Systems, where for each program π we a associate a binary relation Rπ. Process Algebras [J.A. Bergstra, A. Ponse and S.A. Smolka (editors), Handbook of Process Algebra, Elsevier, 2001; W. J. Fokkink. Introduction to Process Algebra. Texts in Theoretical Computer Science. Springer, 2000; R. Milner. Communication and Concurrency. Prentice Hall, 1989; R. J. van Glabbleek, The Linear Time – Branching Time Spectrum I: The Semantics of Concrete, Sequential Processes. In Handbook of Process Algebra (J.A. Bergstra, A. Ponse and S.A. Smolka, eds.), Chapter 1, pp. 3–99, Elsevier, 2001] also give semantics to process (terms) by means of Labeled Transition Systems. In both formalisms, PDL and Process Algebra, the key notion to compare processes is bisimulation. In PDL, we also have the notion of logic equivalence, that can be used to prove that two programs π1 and π2 are logically equivalent ⊢〈π1〉φ↔〈π2〉φ. Unfortunately, logic equivalence and bisimulation do not match in PDL. Bisimilar programs are logic equivalent but the converse does not hold.This paper proposes a semantics and an axiomatization for PDL that makes logically equivalent programs also bisimilar. We prove soundness, completeness and the finite model property