Advertisement

CTL* and ECTL* as fragments of the modal μ-calculus

  • Mads Dam
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 581)

Keywords

Temporal Logic Propositional Variable Computation Tree Logic Boolean Combination Translation Procedure 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [1]
    M. Ben-Ari, A. Pnueli and Z. Manna. “The temporal logic of branching time,” Acta Informatica 20 (1983) 207–226.Google Scholar
  2. [2]
    J. C. Bradfield and C. P. Stirling. “Verifying temporal properties of processes,” Lecture Notes in Computer Science 458 (Springer,1990) pp. 115–125. To appear in Theoretical Computer Science.Google Scholar
  3. [3]
    M. C. Browne, E. M. Clarke, D. L. Dill and B. Mishra. “Automatic verification of sequential circuits using temporal logic,” IEEE Transactions on Computers C-35 (1986).Google Scholar
  4. [4]
    G. Bruns and S. Anderson. “The formalization and analysis of a communications protocol,” Tech. rep. ECS-LFCS-91-137, University of Edinburgh (1991).Google Scholar
  5. [5]
    E. M. Clarke and E. A. Emerson. “Design and synthesis of synchronisation skeletons using branching time temporal logic,” Lecture Notes in Computer Science 131 (1981) pp. 52–71.Google Scholar
  6. [6]
    E. M. Clarke, O. Grümberg and R. P. Kurshan. “A synthesis of two approaches for verifying finite state concurrent systems,” Manuscript, Carnegie-Mellon University (1987).Google Scholar
  7. [7]
    E. M. Clarke and B. Mishra. “Automatic verification of asynchronous circuits,” Lecture Notes in Computer Science 164 (1983) 101–115.Google Scholar
  8. [8]
    R. Cleaveland, J. Parrow and B. Steffen. “A semantics based verification tool for finite state systems,” Proc. 9th IFIP Symp. on Protocol Specification, Testing, and Verification North-Holland, 1989.Google Scholar
  9. [9]
    M. Dam. “Translating CTL* into the modal μ-calculus,” Tech. rep. ECSLFCS-90-123, University of Edinburgh (1990).Google Scholar
  10. [10]
    E. A. Emerson and J. Halpern. ““Sometimes” and “not never” revisited: On branching versus linear time.” Journal of the ACM 33 (1986) 151–178.Google Scholar
  11. [11]
    E. A. Emerson and C. S. Jutla. “The complexity of tree automata and logics of programs,” Proc. 29th Symp. on Foundations of Computer Science (1988) 328–337.Google Scholar
  12. [12]
    E. A. Emerson and C. Lei. “ Efficient model checking in fragments of the propositional mu-calculus,” in Proc. 1st Ann. Symp. on Logic in Computer Science (1986) 267–278.Google Scholar
  13. [13]
    E. A. Emerson and A. P. Sistla. “Deciding full branching time logic,” Information and Control 61 (1984) pp. 175–201.Google Scholar
  14. [14]
    M. J. Fischer and R. E. Ladner. “ Propositional dynamic logic of regular programs,” Journal of Computer and System Science 18 pp. 194–211.Google Scholar
  15. [15]
    D. Gabbay, A. Pnueli, S. Shelah and J. Stavi. “On the temporal analysis of fairness,” Proc. 7th ACM Symp. on Principles of Programming Languages (1980) 163–173.Google Scholar
  16. [16]
    D. Gries. “An exercise in proving parallel programs correct,” Communications of the ACM 20 (1977) pp. 921–930.Google Scholar
  17. [17]
    M. Hennessy and R. Milner. “Algebraic laws for nondeterminism and concurrency,” Journal of the ACM 32 (1985) 137–162.Google Scholar
  18. [18]
    D. Kozen. “Results on the prepositional μ-calculus,” Theoretical Computer Science 27 (North-Holland, 1983) 333–354.Google Scholar
  19. [19]
    O. Lichtenstein, A. Pnueli and L. Zuck. “The glory of the past,” Lecture Notes in Computer Science 193 (1985) 97–107.Google Scholar
  20. [20]
    R. McNaughton. “Testing and generating infinite sequences by a finite automaton,” Information and Control 9 (1966) 521–530.Google Scholar
  21. [21]
    D. Niwinsky. “Fixed points vs. infinite generation,” in Proc. 3rd Ann. Symp. on Logic in Computer Science (1988) 402–409.Google Scholar
  22. [22]
    D. Park. “Concurrency and automata on infinite sequences,” Lecture Notes in Computer Science 104 (1981) 167–183.Google Scholar
  23. [23]
    C. P. Stirling. “Modal and temporal logics,” to appear in: Handbook of Logic in Computer Science (S. Abramsky, D. Gabbay, T. Maibaum, eds.) Oxford University Press (1991).Google Scholar
  24. [24]
    C. P. Stirling and D. J. Walker. “Local model checking in the modal mucalculus,” Lecture Notes in Computer Science 351 (Springer, 1989) pp. 369–383. To appear in Theoretical Computer Science, 1991.Google Scholar
  25. [25]
    R. S. Streett. “Propositional dynamic logic of looping and converse is elementarily decidable,” Information and Control 54 (Academic Press, 1982) pp. 121–141.Google Scholar
  26. [26]
    R. S. Streett and E. A. Emerson. “An automata theoretic decision procedure for the propositional mu-calculus,” Information and Computation 81 (1989) 249–264.Google Scholar
  27. [27]
    W. Thomas. “Star-free regular sets of ω-sequences,” Information and Control 42 (1979) 148–156.Google Scholar
  28. [28]
    W. Thomas. “Computation tree logic and regular ω-languages,” Lecture Notes in Computer Science 354 (1988) 690–713.Google Scholar
  29. [29]
    M. Y. Vardi and P. Wolper. “Yet another process logic,” Lecture Notes in Computer Science 164 (1984) 501–512.Google Scholar
  30. [30]
    D. J. Walker. “Automated analysis of mutual exclusion algorithms using CCS,” Tech. rep. ECS-LFCS-89-91, University of Edinburgh (1989).Google Scholar
  31. [31]
    P. Wolper. “A translation from full branching time temporal logic to one letter propositional dynamic logic with looping,” unpublished manuscript.Google Scholar
  32. [32]
    P. Wolper. “Temporal logic can be more expressive,” Information and Control 56 (1983) 72–99.CrossRefGoogle Scholar
  33. [33]
    P. Wolper, M. Y. Vardi and A. P. Sistla. “Reasoning about infinite computation paths,” in: Proc. 24th IEEE Symp. on Foundations of Computer Science (1983) 185–194.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1992

Authors and Affiliations

  • Mads Dam
    • 1
  1. 1.Department of Computer ScienceUniversity of EdinburghScotland

Personalised recommendations