Skip to main content
SpringerLink
Log in

Computation tree logic and regular ω-languages

  • Technical Contributions
  • Conference paper
  • First Online:
Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency (REX 1988)

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

Abstract

The expressive power of branching time logics is studied in the framework of the theory of ω-automata and ω-languages. The systems CTL* (computation tree logic) and ECTL* (extended computation tree logic) are characterized in terms of star-free, resp. regular ω-languages. A further characterization of CTL* by a "non-counting property" for sets of trees shows that it is decidable whether an ECTL*-formula can be written as a CTL*-formula.

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.

7. References

  1. A. Arnold, A syntactic congruence for rational ω-languages, Theor. Comput. Sci. 39 (1985), 333–335.

    Article  Google Scholar 

  2. J.R. Büchi, On a decision method in restricted second order arithmetic, in: Logic, Methodology, and Philosophy of Science (E. Nagel et al., Eds.), Stanford Univ. Press 1962, pp. 1–11.

    Google Scholar 

  3. E.M. Clarke, O. Grümberg, R.P. Kurshan, A synthesis of two approaches for verifying finite state concurrent systems, manuscript, Carnegie Mellon Univ., Pittsburgh 1987.

    Google Scholar 

  4. J.A. Brzozowski, K. Culik II, A. Gabrielian, Classification of noncounting events, J. Comput. System Sci. 5 (1971), 41–53.

    Google Scholar 

  5. E.A. Emerson, J.Y. Halpern, "Sometimes" and "Not Never" revisited: On branching time versus linear time, J. Assoc. Comput. Mach. 33 (1986), 151–178.

    Google Scholar 

  6. E.A. Emerson, Temporal and modal logic, in: Handbook of Theoretical Computer Science (J. v. Leeuwen, Ed.), North-Holland, Amsterdam (to appear).

    Google Scholar 

  7. D. Gabbay, A. Pnueli, S. Shelah, J. Stavi, On the temporal analysis of fairness, in: 7th ACM Symp. on Principles of Programming Languages, Las Vegas, Nevada, 1980, 163–173.

    Google Scholar 

  8. J. Hintikka, Distributive normal forms in first-order logic, in: "Formal Systems and Recursive Functions" (J.N. Crossley, M.A.E. Dummett, Eds.), pp. 47–90, North-Holland, Amsterdam 1965.

    Google Scholar 

  9. T. Hafer, W. Thomas, Computation tree logic CTL* and path quantifiers in the monadic theory of the binary tree, in: Proc. 14th ICALP, Karlsruhe (T. Ottmann, Ed.), LNCS 267 (1987), 269–279.

    Google Scholar 

  10. H.J. Hoogeboom, G. Rozenberg, Infinitary languages: Basic theory and applications to concurrent systems, in: Current Trends in Concurrency (J.W. de Bakker et alt., Eds.), LNCS 224 (1986), 266–342.

    Google Scholar 

  11. R. McNaughton, S. Papert, Counter-Free Automata, MIT Press, Cambridge, Mass. 1971

    Google Scholar 

  12. D. Perrin, Recent results on automata and infinite words, in: Math. Found. of Comput. Sci. (M.P. Chytil, V. Koubek, Eds.), LNCS 176 (1984), 134–148.

    Google Scholar 

  13. A. Pnueli, The temporal logic of concurrent programs, Theor. Comput. Sci. 13 (1981), 45–60.

    Article  Google Scholar 

  14. A. Pnueli, Applications of temporal logic to the specification and verification of reactive systems: a survey of current trends, in: Current Trends in Concurrency (J.W. de Bakker et alt., Eds.), LNCS 224 (1986), 510–584.

    Google Scholar 

  15. M.O. Rabin, Decidability of second-order theories and automata on infinite trees, Trans. Amer. Math. Soc. 141 (1969), 1–35.

    Google Scholar 

  16. M.P. Schützenberger, On finite monoids having only trivial subgroups, Inform. Contr. 8 (1965), 190–194.

    Article  Google Scholar 

  17. W. Thomas, Star-free regular sets of ω-sequences, Inform. Contr. 42 (1979), 148–156.

    Article  Google Scholar 

  18. W. Thomas, On chain logic, path logic, and first-order logic over infinite trees, Proc. 2nd Symp. on Logic in Computer Sci., Ithaca, N.Y., 1987, 245–256.

    Google Scholar 

  19. W. Thomas, Automata on infinite objects (preliminary version), Aachener Informatik-Berichte 88/17, RWTH Aachen (to appear in: Handbook of Theoretical Computer Science, J.v. Leeuwen, Ed., North-Holland, Amsterdam).

    Google Scholar 

  20. M.Y. Vardi, P. Wolper, Yet another process logic, in: Logics of Programs (E. Clarke, D. Kozen, Eds.), LNCS 164 (1984), 501–512.

    Google Scholar 

  21. P. Wolper, Temporal logic can be more expressive, Inform. Contr. 56 (1983), 72–99.

    Article  Google Scholar 

  22. P. Wolper, M.Y. Vardi, A.P. Sistla, Reasoning about infinite computation paths, Proc. 24th Symp. on Found. of Comput. Sci., Tucson, Arizona, 1983, 185–194.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Lehrstuhl für Informatik II, RWTH Aachen, D-5100, Aachen

    Wolfgang Thomas

Authors
  1. Wolfgang Thomas
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

J. W. de Bakker W. -P. de Roever G. Rozenberg

Rights and permissions

Reprints and permissions

Copyright information

© 1989 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Thomas, W. (1989). Computation tree logic and regular ω-languages. In: de Bakker, J.W., de Roever, W.P., Rozenberg, G. (eds) Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency. REX 1988. Lecture Notes in Computer Science, vol 354. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0013041

Download citation

  • DOI: https://doi.org/10.1007/BFb0013041

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation