×

Axiomatising extended computation tree logic. (English) Zbl 0893.68146

Summary: We present a sound and complete axiomatisation for extended computation tree logic. This language extends the standard computation tree logic CTL* by allowing path formulae to be expressed in linear time mu-calculus instead of linear-time temporal logic. The main novelties in the current paper are an inference rule in the axiom system reflecting the limit closure of paths, a new strongly aconjunctive deterministic normal form for formulae, and the way the completeness proof takes advantage of techniques provided by automata theory.

MSC:

68T27 Logic in artificial intelligence
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Banieqbal, B.; Barringer, H., Temporal logic with fixed points, (Temporal Logic in Specification, Lecture Notes in Computer Science, vol. 398 (1989), Springer: Springer Berlin), 62-74
[2] Barringer, H.; Kuiper, R.; Pnueli, A., A really abstract concurrent model and its temporal logic, (Proc. 13th ACM POPL (1986))
[3] Clarke, E.; Grumberg, O.; Kurshan, R. P., A synthesis of two approaches for verifying finite state concurrent systems, (Logic at Botik’89. Logic at Botik’89, Lecture Notes in Computer Science, vol. 363 (1989), Springer: Springer Berlin), 81-90 · Zbl 0688.68019
[4] Emerson, E. A., Alternative semantics for temporal logics, Theoret. Comput. Sci., 26, 121-130 (1983) · Zbl 0559.68050
[5] Emerson, E. A., Temporal and modal logic, (van Leeuwen, J., Handbook of Theoretical Computer Science (1990), Elsevier: Elsevier Amsterdam), 997-1072 · Zbl 0900.03030
[6] Emerson, E. A.; Halpern, J. Y., Decision procedures and expressiveness in the temporal logic of branching time, J. Comput. System Sci., 30, 1-24 (1985) · Zbl 0559.68051
[7] Emerson, E. A.; Jutla, C. S., Tree automata, mu-calculus, and determinacy, (Proc. 32nd FOCS (1991)), 368-377
[8] Emerson, E. A.; Sistla, A. P., Deciding full branching time logic, Inform. Control, 61, 175-201 (1984) · Zbl 0593.03007
[9] Gabbay, D.; Pnueli, A.; Shelah, S.; Stavi, J., On the temporal analysis of fairness, (Proc. of the 7th ACM POPL (1980)), 163-173
[10] Kaivola, R., Axiomatising linear time mu-calculus, (Proc. CONCUR’95. Proc. CONCUR’95, Lecture Notes in Computer Science, vol. 962 (1995), Springer: Springer Berlin), 423-437
[11] Kaivola, R., Using automata to characterise fixed point temporal logics, (Ph.D. Thesis (1997), Department of Computer Science, University of Edinburgh)
[12] Kozen, D., Results on the propositional μ-calculus, Theoret. Comput. Sci., 27, 333-354 (1983) · Zbl 0553.03007
[13] Lichtenstein, O., Decidability, completeness, and extensions of linear time temporal logic, (Ph.D. Thesis (1991), The Weizmann Institute of Science: The Weizmann Institute of Science Rehovot, Israel)
[14] McNaughton, R., Testing and generating infinite sequences by a finite automaton, Inform. Control, 9, 521-530 (1966) · Zbl 0212.33902
[15] Mostowski, A. W., Regular expressions for infinite trees and a standard form of automata, (Computation Theory, Proc. 5th Symp.. Computation Theory, Proc. 5th Symp., Lecture Notes in Computer Science, vol. 208 (1984), Springer: Springer Berlin), 157-168 · Zbl 0612.68046
[16] Stirling, C., Modal and temporal logics, (Abramsky, S.; etal., Handbook of Logic in Computer Science (1992), Oxford University Press: Oxford University Press Oxford), 477-563
[17] Stirling, C.; Walker, D., Local model checking in the modal mu-calculus, Theoret. Comput. Sci., 89, 161-177 (1991) · Zbl 0745.03027
[18] Streett, R. S.; Emerson, E. A., An automata theoretic decision procedure for the propositional mu-calculus, Inform. Comput., 81, 249-264 (1989) · Zbl 0671.03023
[19] Thomas, W., Computation tree logic and regular ω-languages, (Linear Time, Branching Time and Partial Order in Concurrency. Linear Time, Branching Time and Partial Order in Concurrency, Lecture Notes in Computer Science, vol. 354 (1988), Springer: Springer Berlin), 690-713
[20] Thomas, W., Automata on infinite objects, (van Leeuwen, J., Handbook of Theoretical Computer Science, vol. 2 (1989), North-Holland: North-Holland Amsterdam), 133-191 · Zbl 0900.68316
[21] Vardi, M. Y., A temporal fixpoint calculus, (Proc. 15th ACM POPL (1988)), 250-259
[22] Vardi, M. Y.; Wolper, P., Yet another process logic, (Logics of Programs. Logics of Programs, Lecture Notes in Computer Science, vol. 164 (1983), Springer: Springer Berlin), 501-512 · Zbl 0549.68020
[23] Vardi, M. Y.; Wolper, P., Reasoning about infinite computations, Inform. Comput., 115, 1-37 (1994) · Zbl 0827.03009
[24] Walukiewicz, I., Completeness of Kozen’s axiomatisation of the propositional μ-calculus, (Proc. 10th IEEE LICS (1995)), 14-24 · Zbl 1046.68628
[25] Wolper, P., Temporal logic can be more expressive, Inform. Control, 56, 72-99 (1983) · Zbl 0534.03009
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.