Ockhamist propositional dynamic logic: A natural link between PDL and CTL

Abstract

We present a new logic called Ockhamist Propositional Dynamic Logic, OPDL, which provides a natural link between PDL and CTL*. We show that both PDL and CTL*can be polynomially embedded into OPDL in a rather simple and direct way. More generally, the semantics on which OPDL is based provides a unifying framework for making the dynamic logic family and the temporal logic family converge in a single logical framework. Decidability of the satisfiability problem for OPDL is studied in the paper. © 2013 Springer-Verlag Berlin Heidelberg.