Skip to main content
SpringerLink
Log in

Decidability and Expressivity of Ockhamist Propositional Dynamic Logics

  • Conference paper
  • First Online:
Logics in Artificial Intelligence (JELIA 2016)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 10021))

Included in the following conference series:

  • 604 Accesses

Abstract

Ockhamist Propositional Dynamic Logic (\(\mathsf {OPDL}\)) is a logic unifying the family of dynamic logics and the family of branching-time temporal logics, two families of logic widely used in AI to model reactive systems and multi-agent systems (MAS). In this paper, we present two variants of this logic. These two logics share the same language and differ only in one semantic condition. The first logic embeds Bundled \(\textsf {CTL}^* \) while the second embeds \(\textsf {CTL}^* \). We provide a 2EXPTIME decision procedure for the satisfiability problem of each variant. The decision procedure for the first variant of \(\mathsf {OPDL}\) is based on the elimination of Hintikka sets while the decision procedure for the second variant relies on automata.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    The Ockhamist view of branching time is traditionally opposed to the Peircean view [13, 17]. According to the Peircean view, the truth of a temporal formula should be evaluated with respect either to some history or all histories starting in a given state.

  2. 2.

    Due to space restriction, this version of the paper contains only sketches of proofs of some theorems.

References

  1. Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  2. Balbiani, P., Lorini, E.: Ockhamist propositional dynamic logic: a natural link between PDL and CTL*. In: Libkin, L., Kohlenbach, U., Queiroz, R. (eds.) WoLLIC 2013. LNCS, vol. 8071, pp. 251–265. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39992-3_22

    Google Scholar 

  3. Belnap, N., Perloff, M., Xu, M.: Facing the Future: Agents and Choices in Our Indeterminist World. Oxford University Press, New York (2001)

    Google Scholar 

  4. Brown, M., Goranko, V.: An extended branching-time Ockhamist temporal logic. J. Logic Lang. Inform. 8(2), 143–166 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  5. Dam, M.: CTL* and ECTL* as fragments of the modal mu-calculus. Theoret. Comput. Sci. 126(1), 77–96 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  6. David, A., Schewe, S.: Deciding ATL\(^*\) satisfiability by tableaux. Technical report, Laboratoire IBISC - Université d’Evry Val-d’Essonne (2016)

    Google Scholar 

  7. Emerson, E., Sistla, A.: Deciding full branching time logic. Inf. Control 61, 175–201 (1984)

    Article  MathSciNet  MATH  Google Scholar 

  8. Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs. SIAM J. Comput. 29(1), 132–158 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  9. Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. J. Comput. Syst. Sci. 18(2), 194–211 (1979)

    Article  MathSciNet  MATH  Google Scholar 

  10. Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)

    MATH  Google Scholar 

  11. Piterman, N.: From nondeterministic Büchi and Streett automata to deterministic parity automata. In: Logic in Computer Science (LICS), pp. 255–264. IEEE Computer Society (2006)

    Google Scholar 

  12. Pratt, V.R.: Models of program logics. In: 20th Annual Symposium on Foundations of Computer Science, pp. 115–122. IEEE Computer Society (1979)

    Google Scholar 

  13. Prior, A.: Past, Present, and Future. Clarendon Press, Oxford (1967)

    Book  MATH  Google Scholar 

  14. Reynolds, M.: An axiomatization of full computation tree logic. J. Symbol. Logic 66(3), 1011–1057 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  15. Reynolds, M.: A tableau for bundled CTL*. J. Logic Comput. 17(1), 117–132 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  16. Streett, R.S.: Propositional dynamic logic of looping and converse is elementarily decidable. Inf. Control 54(1–2), 121–141 (1982)

    Article  MathSciNet  MATH  Google Scholar 

  17. Thomason, R.: Combinations of tense and modality. In: Gabbay, D., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 2, 2nd edn, pp. 135–165. Reidel, Dordrecht (1984)

    Chapter  Google Scholar 

  18. Vardi, M.Y., Wolper, P.: Yet another process logic (preliminary version). In: Clarke, E., Kozen, D. (eds.) Logic of Programs 1983. LNCS, vol. 164, pp. 501–512. Springer, Heidelberg (1984). doi:10.1007/3-540-12896-4_383

    Chapter  Google Scholar 

  19. Wolper, P.: A translation from full branching time temporal logic to one letter propositional dynamic logic with looping (unpublished manuscript)

    Google Scholar 

  20. Zanardo, A.: Branching-time logic with quantification over branches: the point of view of modal logic. J. Symbol. Logic 61(1), 143–166 (1996)

    Article  MathSciNet  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IRIT-CNRS, Toulouse University, Toulouse, France

    Joseph Boudou & Emiliano Lorini

Authors
  1. Joseph Boudou
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Emiliano Lorini
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Joseph Boudou .

Editor information

Editors and Affiliations

  1. Open University of Cyprus, Nicosia, Cyprus

    Loizos Michael

  2. University of Cyprus, Nicosia, Cyprus

    Antonis Kakas

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Boudou, J., Lorini, E. (2016). Decidability and Expressivity of Ockhamist Propositional Dynamic Logics. In: Michael, L., Kakas, A. (eds) Logics in Artificial Intelligence. JELIA 2016. Lecture Notes in Computer Science(), vol 10021. Springer, Cham. https://doi.org/10.1007/978-3-319-48758-8_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-48758-8_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-48757-1

  • Online ISBN: 978-3-319-48758-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation