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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM 49, 672–713 (2002)
Axelsson, R., Hague, M., Kreutzer, S., Lange, M., Latte, M.: Extended computation tree logic. In: Fermüller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol. 6397, pp. 67–81. Springer, Heidelberg (2010)
Balbiani, P., Lorini, E.: Ockhamist propositional dynamic logic: a natural link between PDL and CTL*. Technical Report IRIT/RT–2013-12–FR, Institut de Recherche en Informatique de Toulouse (2013)
Belnap, N., Perloff, M., Xu, M.: Facing the future: agents and choices in our indeterminist world. Oxford University Press (2001)
Brown, M., Goranko, V.: An extended branching-time ockhamist temporal logic. Journal of Logic, Language and Information 8(2), 143–166 (1999)
Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1982)
Dam, M.: CTL* and ECTL* as fragments of the modal mu-calculus. Theoretical Computer Science 126(1), 77–96 (1994)
De Nicola, R., Vaandrager, F.W.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407–419. Springer, Heidelberg (1990)
Emerson, E.A., Halpern, J.: ‘Sometimes’ and ‘not never’ revisited: on branching versus linear time. Journal of the ACM 33, 151–178 (1986)
Emerson, E.A., Sistla, A.: Deciding full branching time logic. Information and Control 61, 175–201 (1984)
Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science. Formal Models and Semantics, vol. B. North-Holland Pub. Co./MIT Press (1990)
Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. Journal of Computer Systems Science 18(2), 194–211 (1979)
Goranko, V.: Coalition games and alternating temporal logics. In: Proc. of TARK 2001, pp. 259–272. Morgan Kaufmann (2001)
Harel, D.: Dynamic logic. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 2, pp. 497–604. Reidel, Dordrecht (1984)
Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (2000)
Masini, A., Viganò, L., Volpe, M.: Labelled natural deduction for a bundled branching temporal logic. Journal of Logic and Computation 21(6), 1093–1163 (2011)
McCabe-Dansted, J.C.: A tableau for the combination of CTL and BCTL. In: Proc. of TIME 2012, pp. 29–36. IEEE Computer Society (2012)
Németi, I.: Decidable versions of first order logic and cylindric-relativized set algebras. In: Csirmaz, L., Gabbay, D., de Rijke, M. (eds.) Logic Colloquium 1992, pp. 171–241. CSLI Publications (1995)
Nishimura, H.: Descriptively complete process logic. Acta Informatica 14, 359–369 (1980)
Pnueli, A.: The temporal logic of programs. In: Proc. of the Eighteenth Symposium on Foundations of Computer Science, pp. 46–57. IEEE Computer Society (1977)
Prior, A.: Past, Present, and Future. Clarendon Press, Oxford (1967)
Reynolds, M.: An axiomatization of full computation tree logic. Journal of Symbolic Logic 66(3), 1011–1057 (2001)
Reynolds, M.: A tableau for bundled CTL*. Journal of Logic and Computation 17(1), 117–132 (2007)
Reynolds, M.: A tableau for CTL*. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 403–418. Springer, Heidelberg (2009)
Stirling, C.: Modal and temporal logics. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science, vol. 2. Clarendon Press, Oxford (1992)
Streett, R.S.: Propositional dynamic logic of looping and converse is elementarily decidable. Information and Control 54(1-2), 121–141 (1982)
Thomason, R.: Combinations of tense and modality. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 2, pp. 135–165. Reidel, Dordrecht (1984)
Vardi, M.Y., Stockmeyer, L.J.: Improved upper and lower bounds for modal logics of programs. In: Proc. of the 17th Annual ACM Symposium on Theory of Computing, pp. 240–251. ACM (1985)
Wolper, P.: A translation from full branching time temporal logic to one letter propositional dynamic logic with looping. Unpublished manuscript (1982)
Zanardo, A.: Branching-time logic with quantification over branches: The point of view of modal logic. Journal of Symbolic Logic 61(1), 143–166 (1996)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Balbiani, P., Lorini, E. (2013). Ockhamist Propositional Dynamic Logic: A Natural Link between PDL and CTL*. In: Libkin, L., Kohlenbach, U., de Queiroz, R. (eds) Logic, Language, Information, and Computation. WoLLIC 2013. Lecture Notes in Computer Science, vol 8071. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39992-3_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-39992-3_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39991-6
Online ISBN: 978-3-642-39992-3
eBook Packages: Computer ScienceComputer Science (R0)