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

Ben-Ari, 1983, The temporal logic of branching time, Acta Inform., 20, 207, 10.1007/BF01257083 Bradfield, 1990, Verifying temporal properties of processes, Vol. 458, 115 Browne, 1986, Automatic verification of sequential circuits using temporal logic, IEEE Trans. Comput., C-35, 10.1109/TC.1986.1676711 Bruns, 1991, The formalization and analysis of a communications protocol Clarke, 1981, Design and synthesis of synchronisation skeletons using branching time temporal logic, Vol. 131, 52 Clarke, 1987, A synthesis of two approaches for verifying finite state concurrent systems Clarke, 1983, Automatic verification of asynchronous circuits, Vol. 164, 101 Cleaveland, 1990, Tableau-based model checking in the propositional mu-calculus, Acta Inform., 27, 725, 10.1007/BF00264284 Cleaveland, 1989, A semantics based verification tool for finite state systems Dam, 1990, Translating CTL∗ into the modal μ-calculus Emerson, 1986, “Sometimes” and “not never” revisited: on branching versus linear time, J. ACM, 33, 151, 10.1145/4904.4999 Emerson, 1988, The complexity of tree automata and logics of programs, Proc. 29th Symp. on Foundations of Computer Science, 328, 10.1109/SFCS.1988.21949 Emerson, 1986, Efficient model checking in fragments of the propositional mu-calculus, Proc. 1st Ann. Symp. on Logic on Computer Science, 267 Emerson, 1984, Deciding full branching time logic, Inform. and Control, 61, 175, 10.1016/S0019-9958(84)80047-9 Fischer, 1979, Propositional dynamic logic of regular programs, J. Comput. System Sci., 18, 194, 10.1016/0022-0000(79)90046-1 Gabbay, 1980, On the temporal analysis of fairness, Proc. 7th ACM Symp. on Principles of Programming Languages, 163 Gries, 1977, An exercise in proving parallel programs correct, Commun. ACM, 20, 921, 10.1145/359897.359903 Hennessy, 1985, Algebraic laws for nondeterminism and concurrency, J. ACM, 32, 137, 10.1145/2455.2460 Kozen, 1983, Results on the propositional μ-calculus, Theoret. Comput. Sci., 27, 333, 10.1016/0304-3975(82)90125-6 Lichtenstein, 1985, The glory of the past, Lecture Notes in Computer Science, Vol. 193, 97 McNaughton, 1966, Testing and generating infinite sequences by a finite automaton, Inform. and control, 9, 521, 10.1016/S0019-9958(66)80013-X Niwinsky, 1988, Fixed points vs. infinite generation, Proc. 3rd Ann. Symp. on Logic in Computer Science, 402 Park, 1981, Concurrency and automata on infinite sequences, Vol. 104, 167 Stirling, 1991, Modal and temporal logics Stirling, 1991, Local model checking in the modal mu-calculus, Theoret. Comput. Sci., 89, 161, 10.1016/0304-3975(90)90110-4 Streett, 1982, Propositional dynamic logic of looping and converse is elementarily decidable, Inform. and Control, 54, 121, 10.1016/S0019-9958(82)91258-X Streett, 1989, An automata theoretic decision procedure for the propositional mu-calculus, Inform. and Comput., 81, 249, 10.1016/0890-5401(89)90031-X Thomas, 1979, Star-free regular sets of ω-sequences, Inform. and Control, 42, 148, 10.1016/S0019-9958(79)90629-6 Thomas, 1988, Computation tree logic and regular ω-languages, Vol. 354, 690 Vardi, 1984, Yet another process logic, Vol. 164, 501 Walker, 1989, Automated analysis of mutual exclusion algorithms using CCS P. Wolper, A translation from full branching time temporal logic to one letter propositional dynamic logic with looping, unpublished manuscript. Wolper, 1983, Temporal logic can be more expressive, Inform. and Control, 56, 72, 10.1016/S0019-9958(83)80051-5 Wolper, 1983, Reasoning about infinite computation paths, Proc. 24th IEEE Symp. on Foundations of Computer Science, 185