Abstract
Formulae of the full computation tree logic CTL* are usually interpreted on infinite trees. In this paper, we propose how to interpret them on Ω-languages, i.e. on sets of infinite sequences, even if the Ω-language does not have a one-to-one corresponding tree representation.
Former address: GMD, Rheinstr. 75, D-64295 Darmstadt, Germany. Ulrich Nitsche is supported by the Swiss National Science Foundation.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
J. Berstel. Transductions and Context-Free Languages. Studienbücher Informatik. Teubner Verlag, Stuttgart, first edition, 1979.
E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In D. Kozen, editor, Logic of Programs 1981, volume 131 of Lecture Notes in Computer Science, pages 52–71. Springer Verlag, 1982.
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.
S. Eilenberg. Automata, Languages and Machines, volume A. Academic Press, New York, 1974.
E. A. Emerson. Temporal and modal logic. In van Leeuwen [15], pages 995–1072.
M. A. Harrison. Introduction to Formal Language Theory. Addison-Wesley, Reading, Mass., first edition, 1978.
J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages and Computation. Addison-Wesley, Reading, Mass., first edition, 1979.
O. Kupferman and M. Y. Vardi. Module checking. In R. Alur and T. A. Henzinger, editors, CAV'96, volume 1102 of Lecture Notes in Computer Science, pages 75–86, New Brunswick, N.J., 1996. Springer Verlag.
R. P. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton University Press, Princeton, New Jersey, first edition, 1994.
U. Nitsche. Verification of Co-Operating Systems and Behaviour Abstraction. PhD thesis, University of Frankfurt, Germany. handed in 1996.
U. Nitsche. Propositional linear temporal logic and language homomorphisms. In A. Nerode and Y. V. Matiyasevich, editors, Logical Foundations of Computer Science '94, St. Petersburg, volume 813 of Lecture Notes in Computer Science, pages 265–277. Springer Verlag, 1994.
U. Nitsche. A verification method based on homomorphic model abstraction. In Proceedings of the 13th Annual ACM Symposium on Principles of Distributed Computing, page 393, Los Angeles, 1994. ACM Press.
U. Nitsche. Verification and behavior abstraction — towards a tractable verification technique for large distributed systems. Journal of Systems and Software, 33(3):273–285, June 1996.
W. Thomas. Automata on infinite objects. In van Leeuwen [15], pages 133–191.
J. van Leeuwen, editor. Formal Models and Semantics, volume B of Handbook of Theoretical Computer Science. Elsevier, 1990.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nitsche, U. (1997). Interpretation of the full computation tree logic CTL* on sets of infinite sequences. In: Adian, S., Nerode, A. (eds) Logical Foundations of Computer Science. LFCS 1997. Lecture Notes in Computer Science, vol 1234. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63045-7_28
Download citation
DOI: https://doi.org/10.1007/3-540-63045-7_28
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63045-6
Online ISBN: 978-3-540-69065-8
eBook Packages: Springer Book Archive