Skip to main content
SpringerLink
Log in

Deciding branching time logic: A triple exponential decision procedure for CTL

  • Conference paper
  • First Online:
Logics of Programs (Logic of Programs 1983)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 164))

Included in the following conference series:

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

5. Bibliography

  1. Abrahamson, K., Decidability and Expressiveness of Logics of Processes, PhD Thesis, Univ. of Washington, 1980.

    Google Scholar 

  2. Ben-Ari, M., Manna, Z., and Pnueli, A., The Temporal Logic of Branching Time. 8th Annual ACM Symp. on Principles of Programming Languages, 1981.

    Google Scholar 

  3. Clarke, E. M., and Emerson, E. A., Design and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic, Proceedings of the IBM Workshop on Logics of Programs, Springer-Verlag Lecture Notes in Computer Science #131, 1981.

    Google Scholar 

  4. Clarke, E. M., Emerson, E. A., and Sistla, A. P., Automatic Verification of Finite State Concurrent Programs: A Practical Approach, POPL83.

    Google Scholar 

  5. Emerson, E. A., and Clarke, E. M., Using Branching Time Logic to Synthesize Synchronization Skeletons, Tech. Report TR-208, Univ. of Texas, 1982. (to appear in SCP)

    Google Scholar 

  6. Emerson, E. A., and Halpern, J. Y., Decision Procedures and Expressiveness in the Temporal Logic of Branching Time. 14th Annual ACM Symp. on Theory of Computing, 1982.

    Google Scholar 

  7. Emerson, E. A., and Halpern, J. Y., 'sometimes’ and ‘Not Never’ Revisited: On Branching versus Linear Time. POPL83.

    Google Scholar 

  8. Emerson, E. A., Alternative Semantics for Temporal Logics, Tech. Report TR-182, Univ. of Texas, 1981. (To appear in TCS)

    Google Scholar 

  9. Fischer, M. J., and Ladner, R. E, Propositional Dynamic Logic of Regular Programs, JCSS vol. 18, pp. 194–211, 1979.

    Google Scholar 

  10. Gabbay, D., Pnueli, A., et al., The Temporal Analysis of Fairness. 7th Annual ACM Symp. on Principles of Programming Languages, 1980.

    Google Scholar 

  11. Lamport, L., "Sometimes" is Sometimes "Not Never." 7th Annual ACM Symp. on Principles of Programming Languages, 1980.

    Google Scholar 

  12. McNaughton, R., Testing and Generating Infinite Sequences by a Finite Automaton, Information and Control, vol. 9, 1966.

    Google Scholar 

  13. Pnueli, A., The Temporal Logic of Programs, 19th Annual Symp. on Foundations of Computer Science, 1977.

    Google Scholar 

  14. Pnueli, A., The Temporal Logic of Concurrent Programs, Theoretical Computer Science, V13, pp. 45–60, 1981.

    Google Scholar 

  15. Pnueli, A. and Sherman, R., Personal Communication, 1983.

    Google Scholar 

  16. Rabin, M., Decidability of Second order Theories and Automata on Infinite Trees, Trans. Amer. Math. Society, vol. 141, pp. 1–35, 1969.

    Google Scholar 

  17. Rabin, M., Automata on Infinite Trees and the Synthesis Problem, Hebrew Univ., Tech. Report no. 37, 1970.

    Google Scholar 

  18. Streett, R., Propositional Dynamic Logic of Looping and Converse (PhD Thesis), MIT Lab for Computer Science, TR-263, 1981. (a short version appears in STOC81)

    Google Scholar 

  19. Wolper, P., A Translation from Full Branching Time Temporal Logic to One Letter Propositional Dynamic Logic with Looping, unpublished manuscript, 1982.

    Google Scholar 

  20. Vardi, M., and Wolper, P., Yet Another Process Logic, this workshop, 1983.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Sciences Department, University of Texas, 78712, Austin, TX

    E. Allen Emerson

  2. Aiken Computation Lab, Harvard University, 02138, Cambridge, MA

    A. Prasad Sistla

Authors
  1. E. Allen Emerson
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. A. Prasad Sistla
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Edmund Clarke Dexter Kozen

Rights and permissions

Reprints and permissions

Copyright information

© 1984 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Allen Emerson, E., Prasad Sistla, A. (1984). Deciding branching time logic: A triple exponential decision procedure for CTL. In: Clarke, E., Kozen, D. (eds) Logics of Programs. Logic of Programs 1983. Lecture Notes in Computer Science, vol 164. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-12896-4_363

Download citation

  • DOI: https://doi.org/10.1007/3-540-12896-4_363

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-12896-0

  • Online ISBN: 978-3-540-38775-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation