Expressibility results for linear-time and branching-time logics

  • E. M. Clarke
  • I. A. Draghicescu
Technical Contributions
Part of the Lecture Notes in Computer Science book series (LNCS, volume 354)


We investigate the expressive power of linear-time and branching-time temporal logics as fragments of the logic CTL*. We give a simple characterization of those CTL* formulas that can be expressed in linear-time logic. We also give a simple method for showing that certain CTL* formulas cannot be expressed in the branching-time logic CTL. Both results are illustrated with examples.

Key words

temporal logic linear-time logic branching-time logic computation tree logics fairness 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    E.M. Clarke A.P. Sistla. Complexity of propositional temporal logics. Journal of the Association for Computing Machinery, 32(3):733–749, July 1986.Google Scholar
  2. [2]
    M. Ben-Ari, Z. Manna, and A. Pneuli. The temporal logic of branching time. In 8th Annual ACM Symp. on Principles of Programming Languages, pages 164–177, 1981.Google Scholar
  3. [3]
    M. C. Browne, E. M. Clarke, and O. Grumberg. Characterizing Kripke structures in temporal logic. In 1987 Colloquium on Trees in Algebra and Programming, Pisa, Italy, March 1987.Google Scholar
  4. [4]
    E.M. Clarke and E.A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In Proc. of the Workshop on Logic of Programs, Springer-Verlag, Yorktown Heights, NY, 1981.Google Scholar
  5. [5]
    E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.CrossRefGoogle Scholar
  6. [6]
    E.A. Emerson and J.Y. Halpern. Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. System Sci., 30(1):1–24, 1985.CrossRefGoogle Scholar
  7. [7]
    E.A. Emerson and J.Y. Halpern. 'sometimes’ and ‘not never’ revisited: on branching versus linear time. In Proc. 10th ACM Symp. on Principles of Programming Languages, 1983.Google Scholar
  8. [8]
    G.E. Hughes and M.J. Creswell. An Introduction to Modal Logic. Methuen and Co., 1977.Google Scholar
  9. [9]
    L. Lamport. 'sometimes’ is sometimes ‘not never'. In Seventh Annual ACM Symposium on Principles of Programming Languages, pages 174–185, Association for Computing Machinery, Las Vegas, January 1980.Google Scholar
  10. [10]
    D. E. Muller. Infinite sequences and finite machines. In Proc. 4th Annual IEEE Symposium of Switching Theory and Logical Design, pages 3–16, 1963.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1989

Authors and Affiliations

  • E. M. Clarke
    • 1
  • I. A. Draghicescu
    • 1
  1. 1.Computer Science DepartmentCarnegie Mellon UniversityPittsburgh

Personalised recommendations