Abstract
We investigate Or E x, a temporal logic for specifying open systems. Path properties in Or E x are expressed using ε-regular expressions, while similar logics for open systems, such as ATL* of Alur et al., use LTL for this purpose. Our results indicate that this distinction is an important one. In particular, we show that Orex has a more efficient model-checking procedure than ATL*, even though it is strictly more expressive. To this end, we present a single-exponential model-checking algorithm for Or E x; the model-checking problem for ATL* in contrast is provably double-exponential.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
R. Alur, T.A. Henzinger, and O. Kupferman. Alternating-time temporal logic. In Proceedings of the 38th IEEE Symposium on the Foundations of Computer Science. IEEE Press, 1997.
E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-time temporal logic. In D. Kozen, editor, Proceedings of the Workshop on Logic of Programs, Yorktown Heights, volume 131 of Lecture Notes in Computer Science, pages 52–71. Springer-Verlag, 1981.
E. M. Clarke, O. Grumberg, H. Hiraishi, S. Jha, D. E. Long, K. L. McMillan, and L. A. Ness. Verification of the Future+ cache coherence protocol. Formal Methods in System Design, 6:217–232, 1995.
E. A. Emerson and J. Y. Halpern. ‘Sometime’ and ‘not never’ revisited: On branching versus linear time temporal logic. Journal of the ACM, 33(1):151–178, 1986.
E.A. Emerson and C. Jutla. The complexity of tree automata and logics of programs. In Proceedings of the IEEE FOCS, 1988.
E.A. Emerson and C. Jutla. On simultaneously determinising and comple-menting !-automata. In Proceedings of the IEEE FOCS, 1989.
David Harel. Dynamic logic. In Handbook of Philosophical Logic, Volume II. Reidel, 1984.
G. J. Holzmann. The model checker SPIN. IEEE Trans. on Software Engineering, 23(5):279–295, 1997.
Orna Kupferman and Moshe Vardi. Module checking. In Proceedings of CAV’96, LNCS 1102. Springer-Verlag, 1996.
K. L. McMillan. Symbolic Model Checking. Kluwer Academic, 1993.
R. Parikh. Propositional game logic. In Proceedings of 24th IEEE FOCS, pages 195–200, 1983.
A. Pnueli. The temporal logic of programs. In Proceedings of the IEEE Symposium on the Foundations of Computing Science. IEEE Press, 1976.
P.J.G. Ramadge and W.M. Wonham. The control of discrete-event systems. IEEE Trans. on Control Theory, 77:81–98, 1989.
S. Safra. On complexity of !-automata. In In the Proceedings of the 29th FOCS, 1988.
W. Thomas. Automata on infinite objects. In Handbook of Theoretical Computer Science, Volume B. Elsevier Science Publishers, 1990.
M. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Symposium on Logic in Computer Science (LICS’ 86), pages 332–344, Cambridge, Massachusetts, June 1986. Computer Society Press.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mukund, M., Narayan Kumar, K., Smolka, S.A. (1999). Faster Model Checking for Open Systems. In: Thiagarajan, P.S., Yap, R. (eds) Advances in Computing Science — ASIAN’99. ASIAN 1999. Lecture Notes in Computer Science, vol 1742. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46674-6_20
Download citation
DOI: https://doi.org/10.1007/3-540-46674-6_20
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66856-5
Online ISBN: 978-3-540-46674-1
eBook Packages: Springer Book Archive