# CTL^{*} and ECTL^{*} as fragments of the modal μ-calculus

Conference paper

First Online:

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

## References

- [1]M. Ben-Ari, A. Pnueli and Z. Manna. “The temporal logic of branching time,”
*Acta Informatica***20**(1983) 207–226.Google Scholar - [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]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]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]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]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]E. M. Clarke and B. Mishra. “Automatic verification of asynchronous circuits,”
*Lecture Notes in Computer Science***164**(1983) 101–115.Google Scholar - [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]M. Dam. “Translating CTL
^{*}into the modal*μ*-calculus,” Tech. rep. ECSLFCS-90-123, University of Edinburgh (1990).Google Scholar - [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]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]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]E. A. Emerson and A. P. Sistla. “Deciding full branching time logic,”
*Information and Control***61**(1984) pp. 175–201.Google Scholar - [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]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]D. Gries. “An exercise in proving parallel programs correct,”
*Communications of the ACM***20**(1977) pp. 921–930.Google Scholar - [17]M. Hennessy and R. Milner. “Algebraic laws for nondeterminism and concurrency,”
*Journal of the ACM***32**(1985) 137–162.Google Scholar - [18]D. Kozen. “Results on the prepositional
*μ*-calculus,”*Theoretical Computer Science***27**(North-Holland, 1983) 333–354.Google Scholar - [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]R. McNaughton. “Testing and generating infinite sequences by a finite automaton,”
*Information and Control***9**(1966) 521–530.Google Scholar - [21]D. Niwinsky. “Fixed points vs. infinite generation,” in
*Proc. 3rd Ann. Symp. on Logic in Computer Science*(1988) 402–409.Google Scholar - [22]D. Park. “Concurrency and automata on infinite sequences,”
*Lecture Notes in Computer Science***104**(1981) 167–183.Google Scholar - [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]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]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]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]W. Thomas. “Star-free regular sets of
*ω*-sequences,”*Information and Control***42**(1979) 148–156.Google Scholar - [28]W. Thomas. “Computation tree logic and regular
*ω*-languages,”*Lecture Notes in Computer Science***354**(1988) 690–713.Google Scholar - [29]M. Y. Vardi and P. Wolper. “Yet another process logic,”
*Lecture Notes in Computer Science***164**(1984) 501–512.Google Scholar - [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]P. Wolper. “A translation from full branching time temporal logic to one letter propositional dynamic logic with looping,” unpublished manuscript.Google Scholar
- [32]P. Wolper. “Temporal logic can be more expressive,”
*Information and Control***56**(1983) 72–99.CrossRefGoogle Scholar - [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