Abstract
We consider concurrent two-person games played in real time, in which the players decide both which action to play, and when to play it. Such timed games differ from untimed games in two essential ways. First, players can take each other by surprise, because actions are played with delays that cannot be anticipated by the opponent. Second, a player should not be able to win the game by preventing time from diverging. We present a model of timed games that preserves the element of surprise and accounts for time divergence in a way that treats both players symmetrically and applies to all ω-regular winning conditions. We prove that the ability to take each other by surprise adds extra power to the players. For the case that the games are specified in the style of timed automata, we provide symbolic algorithms for their solution with respect to all ω-regular winning conditions. We also show that for these timed games, memory strategies are more powerful than memoryless strategies already in the case of reachability objectives.
Supported in part by the AFOSR MURI grant F49620-00-1-0327, the DARPA grant F33615-C-98-3614, the MARCO grant 98-DT-660, -the ONR grant N00014-02-1-0671, the NSF grants CCR-9988172, CCR-0225610, and CCR-0234690, the NSF CAREER award CCR-0132780, and the MIUR grant MEFISTO.
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.
Similar content being viewed by others
References
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comp. Sci. 126, 183–235 (1994)
Alur, R., de Alfaro, L., Henzinger, T.A., Mang, F.Y.C.: Automating modular verification. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 82–97. Springer, Heidelberg (1999)
Alur, R., Henzinger, T.A.: Modularity for timed and hybrid systems. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 74–88. Springer, Heidelberg (1997)
Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672–713 (2002)
Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. In: Proc. IFAC Symp. System Structure and Control, pp. 469–474. Elsevier, Amsterdam (1998)
Church, A.: Logic, arithmetics, and automata. In: Proc. Int. Congress of Mathematicians, 1962, pp. 23–35 (1963)
de Alfaro, L., Henzinger, T.A., Majumdar, R.: From verification to control: Dynamic programs for omega-regular objectives. In: Proc. Symp. Logic in Comp. Sci., pp. 279–290. IEEE, Los Alamitos (2001)
de Alfaro, L., Henzinger, T.A., Majumdar, R.: Symbolic algorithms for infinite-state games. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR 2001. LNCS, vol. 2154, pp. 536–550. Springer, Heidelberg (2001)
de Alfaro, L., Henzinger, T.A., Stoelinga, M.I.A.: Timed interfaces. In: Sangiovanni-Vincentelli, A.L., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol. 2491, pp. 108–122. Springer, Heidelberg (2002)
Emerson, E.A., Jutla, C.S.: Tree automata, mu-calculus, and determinacy. In: Proc. Symp. Foundations of Comp. Sci., pp. 368–377. IEEE, Los Alamitos (1991)
Faella, M., La Torre, S., Murano, A.: Dense real-time games. In: Proc. Symp. Logic in Comp. Sci., pp. 167–176. IEEE, Los Alamitos (2002)
Henzinger, T.A., Horowitz, B., Majumdar, R.: Rectangular hybrid games. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 320–335. Springer, Heidelberg (1999)
Henzinger, T.A., Kopke, P.W.: Discrete-time control for rectangular hybrid automata. Theor. Comp. Sci. 221, 369–392 (1999)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, Heidelberg (1991)
Maler, O., Pnueli, A., Sifakis, J.: On the synthesis of discrete controllers for timed systems. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 229–242. Springer, Heidelberg (1995)
Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. Symp. Principles of Programming Languages, pp. 179–190. ACM, New York (1989)
Ramadge, P.J.G., Wonham, W.M.: The control of discrete-event systems. IEEE Transactions on Control Theory 77, 81–98 (1989)
Segala, R., Gawlick, G., Søgaard-Andersen, J., Lynch, N.: Liveness in timed and untimed systems. Info. and Comput. 141, 119–171 (1998)
Thomas, W.: Automata on infinite objects. In: van Leeuwen, J. (ed.) Handbook Theor. Comp. Sci., vol. B, pp. 135–191. Elsevier, Amsterdam (1990)
Yi, W.: Real-time behaviour of asynchronous agents. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 502–520. Springer, Heidelberg (1990)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M. (2003). The Element of Surprise in Timed Games. In: Amadio, R., Lugiez, D. (eds) CONCUR 2003 - Concurrency Theory. CONCUR 2003. Lecture Notes in Computer Science, vol 2761. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45187-7_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-45187-7_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40753-9
Online ISBN: 978-3-540-45187-7
eBook Packages: Springer Book Archive