Abstract
A procedure for the analysis of state spaces is called symbolic if it manipulates not individual states, but sets of states that are represented by constraints. Such a procedure can be used for the analysis of infinite state spaces, provided termination is guaranteed. We present symbolic procedures, and corresponding termination criteria, for the solution of infinite-state games, which occur in the control and modular verification of infinite-state systems. To characterize the termination of symbolic procedures for solving infinite-state games, we classify these game structures into four increasingly restrictive categories:
-
1
Class 1 consists of infinite-state structures for which all safety and reachability games can be solved.
-
2
Class 2 consists of infinite-state structures for which all ω-regular games can be solved.
-
3
Class 3 consists of infinite-state structures for which all nested positive boolean combinations of ω-regular games can be solved.
-
4
Class 4 consists of infinite-state structures for which all nested boolean combinations of ω-regular games can be solved.
We give a structural characterization for each class, using equivalence relations on the state spaces of games which range from game versions of trace equivalence to a game version of bisimilarity. We provide infinite-state examples for all four classes of games from control problems for hybrid systems. We conclude by presenting symbolic algorithms for the synthesis of winning strategies (“controller synthesis”) for infinitestate games with arbitrary ω-regular objectives, and prove termination over all class-2 structures. This settles, in particular, the symbolic controller synthesis problem for rectangular hybrid systems.
This research was supported in part by the AFOSR MURI grant F49620-00-1-0327, the DARPA SEC grant F33615-C-98-3614, the MARCO GSRC grant 98-DT-660, the NSF Theory grant CCR-9988172, and the NSF ITR grant CCR-0085949.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
P. Abdulla and B. Jonsson. Verifying networks of timed automata. In TACAS 98, LNCS 1384, pp. 298–312. Springer-Verlag, 1998.
R. Alur and D. Dill. A theory of timed automata. Theoretical Computer Science, 126:183–235, 1994.
R. Alur, T. Henzinger, and O. Kupferman. Alternating-time temporal logic. In FOCS 97, pp. 100–109. IEEE Computer Society Press, 1997.
R. Alur, T. Henzinger, O. Kupferman, and M. Vardi. Alternating refinement relations. In CONCUR 97, LNCS 1466, pp. 163–178. Springer-Verlag, 1998.
A. Bouajjani, J.-C. Fernandez, and N. Halbwachs. Minimal model generation. In CAV 90, LNCS 531, pp. 197–203. Springer-Verlag, 1990.
J. Büchi and L. Landweber. Solving sequential conditions by finite-state strategies. Transactions of the AMS, 138:295–311, 1969.
E. Emerson and C. Jutla. Tree automata, mu-calculus, and determinacy. In FOCS 91, pp. 368–377. IEEE Computer Society Press, 1991.
E. Emerson, C. Jutla, and A. Sistla. On model checking for fragments of μ-calculus. In CAV 93, LNCS 697, pp. 385–396. Springer-Verlag, 1993.
T. Henzinger, P.-H. Ho, and H. Wong-Toi. HyTech: a model checker for hybrid systems. Software Tools for Technology Transfer, 1:110–122, 1997.
T. Henzinger, B. Horowitz, and R. Majumdar. Rectangular hybrid games. In CONCUR 99, LNCS 1664, pp. 320–335. Springer-Verlag, 1999.
T. Henzinger and R. Majumdar. A classification of symbolic transition systems. In STACS 2000, LNCS 1770, pp. 13–35. Springer-Verlag, 2000.
T. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic model checking for real-time systems. Information and Computation, 111:193–244, 1994.
P. Kanellakis and S. Smolka. CCS expressions, finite-state processes, and three problems of equivalence. Information and Computation, 86:43–68, 1990.
D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333–354, 1983.
O. Maler, A. Pnueli, and J. Sifakis. On the synthesis of discrete controllers for timed systems. In STACS 95, LNCS 900, pp. 229–242. Springer-Verlag, 1995.
R. McNaughton. Infinite games played on finite graphs. Annals of Pure and Applied Logic, 65:149–184, 1993.
A. Mostowski. Regular expressions for infinite trees and a standard form of automata. In Symp. Comp. Theory, LNCS 208, pp. 157–168. Springer-Verlag, 1984.
P. Ramadge and W. Wonham. Supervisory control of a class of discrete-event processes. SIAM J. Control and Optimization, 25:206–230, 1987.
W. Thomas. Automata on infinite objects. In J. van Leeuwen, ed., Handbook of Theoretical Computer Science, volume B, pp. 133–191. Elsevier, 1990.
W. Thomas. On the synthesis of strategies in infinite games. In STACS 95, LNCS 900, pp. 1–13. Springer-Verlag, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Alfaro, L., Henzinger, T.A., Majumdar, R. (2001). Symbolic Algorithms for Infinite-State Games. In: Larsen, K.G., Nielsen, M. (eds) CONCUR 2001 — Concurrency Theory. CONCUR 2001. Lecture Notes in Computer Science, vol 2154. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44685-0_36
Download citation
DOI: https://doi.org/10.1007/3-540-44685-0_36
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42497-0
Online ISBN: 978-3-540-44685-9
eBook Packages: Springer Book Archive