Skip to main content
SpringerLink
Log in

Completeness of a Branching-Time Logic with Possible Choices

  • Published:
Studia Logica Aims and scope Submit manuscript

Abstract

In this paper we present BTC, which is a complete logic for branchingtime whose modal operator quantifies over histories and whose temporal operators involve a restricted quantification over histories in a given possible choice. This is a technical novelty, since the operators of the usual logics for branching-time such as CTL express an unrestricted quantification over histories and moments. The value of the apparatus we introduce is connected to those logics of agency that are interpreted on branching-time, as for instance Stit Logics.

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

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Alur Rajeev, Henzinger Thomas, Kupferman Orna: ‘Alternating-time temporal logic’. Journal of ACM 49(5), 672–713 (2002)

    Article  Google Scholar 

  2. Belnap Nuel, Perloff Michael, Xu Ming: Facing the Future: agents and choices in our Indeterminist World. Oxford University Press, Oxford (2001)

    Google Scholar 

  3. Broersen Jan, Herzig Andreas, Troquard Nicolas: ‘From Coalition Logic to STIT’. Electronic Notes in Theoretical Computer Science 157, 23–35 (2006)

    Article  Google Scholar 

  4. Broersen Jan, Herzig Andreas, Troquard Nicolas: ‘Embedding ATL in Strategic STIT Logic of Agency’. Journal of Computation 16(5), 559–578 (2006)

    Google Scholar 

  5. Burgess John: ‘The Unreal Future. Theoria 44, 157–179 (1978)

    Article  Google Scholar 

  6. Burgess John: ‘Logic and time. J. of Symbolic Logic 44, 556–582 (1979)

    Article  Google Scholar 

  7. Burgess John: ‘Decidability for branching-time’. Studia Logica 39(2/3), 203–218 (1980)

    Article  Google Scholar 

  8. Clark Edmund, Emerson Ernest: ‘Using branching-time temporal logic to synthesise synchronisation skeletons’. Science of Computer Programming 2, 241–266 (1982)

    Article  Google Scholar 

  9. Chellas Brian: The Logical Form of Imperatives. Perry Lane Press, Stanford (1969)

    Google Scholar 

  10. Emerson Ernest, Halpern Joe: ‘Decision procedures and expressiveness in the temporal logic of branching-time’. Journal of Computer and Systems Science 30, 1–24 (1985)

    Article  Google Scholar 

  11. Emerson Ernest, Halpern Joe: “Sometimes’ and ‘not never’ revisited: on branching versus linear time’. Journal of the ACM 33, 151–178 (1986)

    Article  Google Scholar 

  12. Emerson, Ernest, and Sistla A. Prasad, ‘Deciding branching-time logic, Proceedings of the 16th ACM Symposium on Theory of Computing, 1984.

  13. Goranko Valentin, van Drimmelen Govert: ‘Complete axiomatization and decidability of Alternating-time temporal logic’. Theoretical Computer Science 353(1/3), 93–117 (2006)

    Article  Google Scholar 

  14. Herzig Andreas, Troquard Nicolas: ‘Knowing How to Play: Uniform Choices in Logics of Agency’. In: Weiss, G., Stone, P. (eds) 5th International Joint Conference on Autonomous Agents and Multi Agent Systems (AAMAS 2006), pp. 209–216. ACM Press, New York (2006)

    Chapter  Google Scholar 

  15. Horty, John, and Nuel Belnap, ‘The deliberative stit: A study of action, omission, and obligation’, Journal of Philosophical Logic, 24(6):583–644.

  16. Horty John: Agency and Deontic Logic. Oxford University Press, Oxford (2001)

    Book  Google Scholar 

  17. Øhrstøm Peter, Hasle Per: Temporal Logic: From Ancient Ideas to Artificial Intelligence. Kluwer, Dordrecht (1995)

    Google Scholar 

  18. Pauly Marc: ‘A Modal Logic for Coalitional Power in Games’. Journal of Logic and Computation 12, 149–166 (2002)

    Article  Google Scholar 

  19. Prior Arthur: Past, Present and Future. Clarendon University Press, Oxford (1967)

    Google Scholar 

  20. Reynolds Mark: ‘An axiomatization of full computation tree logic. Journal of Symbolic Logic 66, 1011–1057 (2001)

    Article  Google Scholar 

  21. Thomason Richmond: ‘Combination of Tense and Modality’. In: Gabbay, D., Guenthner, F. (eds) The Handbook of Philosophical Logic, pp. 135–165. Reidel, Dordrecht (1984)

    Google Scholar 

  22. Xu Ming: ‘Axioms for Deliberative STIT’. Journal of Philosophical Logic 27(5), 505–552 (1998)

    Article  Google Scholar 

  23. Zanardo Alberto: ‘A finite axiomatization of the set of strongly valid Ockamist formulas’. Journal of Philosophical Logic 14, 447–468 (1985)

    Article  Google Scholar 

  24. Zanardo Alberto: ‘Axiomatization of ‘Peircean’ branching-time logic’. Studia Logica 49, 183–195 (1990)

    Article  Google Scholar 

  25. Zanardo Alberto: ‘Undivided and Indistinguishable Histories in Branching-Time Logics’. Journal of Logic, Language and Information 7, 297–315 (1998)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Philosophy, Delft University of Technology, Jaffalaan 5, 2628 BX, Delft, Netherlands

    Roberto Ciuni

  2. Department of Pure and Applied Mathematics, University of Padova, Via Trieste 63, 35121, Padova, Italy

    Alberto Zanardo

Authors
  1. Roberto Ciuni
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Alberto Zanardo
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Roberto Ciuni.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Ciuni, R., Zanardo, A. Completeness of a Branching-Time Logic with Possible Choices. Stud Logica 96, 393–420 (2010). https://doi.org/10.1007/s11225-010-9291-1

Download citation

  • Received:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s11225-010-9291-1

Keywords

Search

Navigation