Abstract
We propose a new model for timed games, based on concurrent game structures (CGSs). Compared to the classical timed game automata of Asarin et al. [8], our timed CGSs are “more concurrent”, in the sense that they always allow all the agents to act on the system, independently of the delay they want to elapse before their action. Timed CGSs weaken the “element of surprise” of timed game automata reported by de Alfaro et al. [15].
We prove that our model has nice properties, in particular that model-checking timed CGSs against timed ATL is decidable via region abstraction, and in particular that strategies are “region-stable” if winning objectives are. We also propose a new extension of TATL, containing ATL*, which we call TALTL. We prove that model-checking this logic remains decidable on timed CGSs. Last, we explain how our algorithms can be adapted in order to rule out Zeno (co-)strategies, based on the ideas of Henzinger et al. [15,20].
Work partly supported by project DOTS (ANR-06-SETI-003).
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
Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. & Comp. 104(1), 2–34 (1993)
Alur, R., Dill, D.: A theory of timed automata. TCS 126(2), 183–235 (1994)
Alur, R., Feder, T., Henzinger, T.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)
Alur, R., Henzinger, T.: A really temporal logic. J. ACM 41(1), 181–204 (1994)
Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. In: FOCS 1997, pp. 100–109. IEEE Computer Society Press, Los Alamitos (1997)
Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. J. ACM 49(5), 672–713 (2002)
Alur, R., Henzinger, T., Kupferman, O., Vardi, M.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 163–178. Springer, Heidelberg (1998)
Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. In: Proc. Symp. System Structure & Control, pp. 469–474. Elsevier, Amsterdam (1998)
Behrmann, G., David, A., Larsen, K.G.: A tutorial on UPPAAL. In: Bernardo, M., Corradini, F. (eds.) Formal Methods for the Design of Real-Time Systems. LNCS, vol. 3185, pp. 200–236. Springer, Heidelberg (2004)
Brihaye, Th., Laroussinie, F., Markey, N., Oreiby, G.: Timed concurrent game structures. Technical report, LSV, ENS Cachan, France (2007)
Büchi, J.R., Landweber, L.H.: Solving sequential conditions by finite-state strategies. Trans. AMS 138, 295–311 (1969)
Cassez, F., David, A., Fleury, E., Larsen, K.G., Lime, D.: Efficient on-the-fly algorithms for the analysis of timed games. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 66–80. Springer, Heidelberg (2005)
Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NuSMV: A new symbolic model verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol. 1633, pp. 495–499. Springer, Heidelberg (1999)
Daws, C., Olivero, A., Tripakis, S., Yovine, S.: The tool Kronos. In: Alur, R., Sontag, E.D., Henzinger, T. (eds.) Hybrid Systems III. LNCS, vol. 1066, pp. 208–219. Springer, Heidelberg (1996)
de Alfaro, L., Faella, M., Henzinger, T., Majumdar, R., Stoelinga, M.: The element of surprise in timed games. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 144–158. Springer, Heidelberg (2003)
De Wulf, M., Doyen, L., Markey, N., Raskin, J.-F.: Robustness and implementability of timed automata. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 118–133. Springer, Heidelberg (2004)
Emerson, E.: Temporal and modal logic. In: Handbook of Theoretical Computer Science, Formal Models and Sematics, vol. B, pp. 995–1072. Elsevier, Amsterdam (1990)
Gawlick, R., Segala, R., Søgaard-Andersen, J., Lynch, N.: Liveness in timed and untimed systems. In: Shamir, E., Abiteboul, S. (eds.) ICALP 1994. LNCS, vol. 820, pp. 166–177. Springer, Heidelberg (1994)
Harding, A., Ryan, M., Schobbens, P.-Y.: A new algorithm for strategy synthesis in LTL games. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 477–492. Springer, Heidelberg (2005)
Henzinger, T., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real time systems. Inf. & Comp. 111(2), 193–244 (1994)
Henzinger, T., Prabhu, V.: Timed alternating-time temporal logic. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 1–17. Springer, Heidelberg (2006)
Holzmann, G.: The model checker spin. IEEE Trans. Software Engineering 23(5), 279–295 (1997)
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)
McMillan, K.: Symbolic Model Checking — An Approach to the State Explosion Problem. PhD thesis, CMU, Pittsburgh, Pennsylvania, USA (1993)
Pnueli, A.: The temporal logic of programs. In: FOCS 1977, pp. 46–57. IEEE Computer Society Press, Los Alamitos (1977)
Puri, A.: Dynamical properties of timed automata. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 210–227. Springer, Heidelberg (1998)
Ramadge, P., Wonham, W.: The control of discrete event systems. Proc. IEEE 77(1), 81–98 (1989)
Schobbens, P.-Y., Bontemps, Y.: Real-time concurrent game structures. Personnal communication (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brihaye, T., Laroussinie, F., Markey, N., Oreiby, G. (2007). Timed Concurrent Game Structures. In: Caires, L., Vasconcelos, V.T. (eds) CONCUR 2007 – Concurrency Theory. CONCUR 2007. Lecture Notes in Computer Science, vol 4703. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74407-8_30
Download citation
DOI: https://doi.org/10.1007/978-3-540-74407-8_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-74406-1
Online ISBN: 978-3-540-74407-8
eBook Packages: Computer ScienceComputer Science (R0)