Skip to main content

Automata, tableaux, and temporal logics

Extended Abstract

  • Conference paper
  • First Online:

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

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  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., Characterizing Correctness Properties of Parallel Programs Using Fixpoints, Proc. ICALP 80, LNCS Vol. 85, Springer Verlag, 1980, pp. 169–181.

    Google Scholar 

  6. Emerson, E. A., and Clarke, E. M., Using Branching Time Logic to Synthesize Synchronization Skeletons, Science of Computer Programming, vol. 2, pp. 241–266, 1982.

    Google Scholar 

  7. 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 

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

    Google Scholar 

  9. Emerson, E. A., and Lei, C. L., Modalities for Model Checking: Branching Time Strikes Back, to be presented at the 12th Annual ACM Symposium on Principles of Programming Languages.

    Google Scholar 

  10. Emerson, E. A., and Sistla, A. P., Deciding Branching Time Logic, 16 Annual ACM Symp. on Theory of Computing, 1984.

    Google Scholar 

  11. Hossley, R., and Rackoff, C, The Emptiness Problem For Automata on Infinite Trees, Proc. 13th IEEE Symp. Switching and Automata Theory, pp. 121–124, 1972.

    Google Scholar 

  12. Koren, T. and Pnueli, A., There exist decidable context-free propositional dynamic logics, CMU Workshop on Logics of Programs, Springer LNCS #164, pp. 313–325, 1983.

    Google Scholar 

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

    Google Scholar 

  14. Manna, Z., and Pnueli, A., The modal logic of programs, Proc. 6th Int. Colloquium on Automata, Languages, and Programming, Springer-Verlag Lecture Notes in Computer Science #71, pp. 385–410, 1979.

    Google Scholar 

  15. Meyer, A. R., Weak Monadic Second Order Theory of Successor is Not Elementary Recursive, Boston Logic Colloquium, Springer-Verlag Lecture Notes in Mathematics #453, 1974.

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  19. Streett, R., Propositional Dynamic Logic of Looping and Converse (PhD Thesis), MIT Lab for Computer Science, TR-263, 1981. (a revised version appears in Information and Control, vol. 54, pp. 121–141, 1982.)

    Google Scholar 

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

    Google Scholar 

  21. Vardi, M., and Wolper, P., Yet Another Process Logic, CMU Workshop on Logics of Programs, Springer-Verlag, 1983.

    Google Scholar 

  22. Wolper, P., Vardi, M., and Sistla, A., Reasoning about Infinite Computations, 24th FOCS, 1983.

    Google Scholar 

  23. Vardi, M. and Wolper, P., Automata Theoretic Techniques for Modal Logics of Programs, pp. 446–455, STOC84.

    Google Scholar 

  24. Vardi, M. and Stockmeyer, L., Improved Upper and Lower Bounds for Modal Logics of Programs, to be presented at STOC85.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Rohit Parikh

Rights and permissions

Reprints and permissions

Copyright information

© 1985 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Emerson, E.A. (1985). Automata, tableaux, and temporal logics. In: Parikh, R. (eds) Logics of Programs. Logic of Programs 1985. Lecture Notes in Computer Science, vol 193. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-15648-8_7

Download citation

  • DOI: https://doi.org/10.1007/3-540-15648-8_7

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-15648-2

  • Online ISBN: 978-3-540-39527-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics