{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T06:09:16Z","timestamp":1770703756546,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540450269","type":"print"},{"value":"9783540450313","type":"electronic"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11867340_18","type":"book-chapter","created":{"date-parts":[[2006,9,25]],"date-time":"2006-09-25T09:06:53Z","timestamp":1159175213000},"page":"245-259","source":"Crossref","is-referenced-by-count":13,"title":["Model-Checking Timed ATL for Durational Concurrent Game Structures"],"prefix":"10.1007","author":[{"given":"Fran\u00e7ois","family":"Laroussinie","sequence":"first","affiliation":[]},{"given":"Nicolas","family":"Markey","sequence":"additional","affiliation":[]},{"given":"Ghassan","family":"Oreiby","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"1","key":"18_CR1","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1006\/inco.1993.1024","volume":"104","author":"R. Alur","year":"1993","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: Model-checking in dense real-time. Information & Computation\u00a0104(1), 2\u201334 (1993)","journal-title":"Information & Computation"},{"issue":"2","key":"18_CR2","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theoretical Computer Science"},{"key":"18_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"74","DOI":"10.1007\/3-540-63141-0_6","volume-title":"CONCUR\u201997: Concurrency Theory","author":"R. Alur","year":"1997","unstructured":"Alur, R., Henzinger, T.A.: Modularity for timed and hybrid systems. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, pp. 74\u201388. Springer, Heidelberg (1997)"},{"key":"18_CR4","doi-asserted-by":"publisher","first-page":"100","DOI":"10.1109\/SFCS.1997.646098","volume-title":"Proc 38th Annual Symp. on Foundations of Computer Science (FOCS 1997)","author":"R. Alur","year":"1997","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. In: Proc 38th Annual Symp. on Foundations of Computer Science (FOCS 1997), pp. 100\u2013109. IEEE Comp. Soc. Press, Los Alamitos (1997)"},{"issue":"5","key":"18_CR5","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R. Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM\u00a049(5), 672\u2013713 (2002)","journal-title":"Journal of the ACM"},{"key":"18_CR6","volume-title":"Proc IFAC Symp. on System Structure and Control","author":"E. Asarin","year":"1998","unstructured":"Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. In: Proc IFAC Symp. on System Structure and Control. Elsevier, Amsterdam (1998)"},{"key":"18_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-04558-9","volume-title":"Systems and Software Verification. Model-Checking Techniques and Tools","author":"B. B\u00e9rard","year":"2001","unstructured":"B\u00e9rard, B., Bidoit, M., Finkel, A., Laroussinie, F., Petit, A., Petrucci, L., Schnoebelen, P.: Systems and Software Verification. Model-Checking Techniques and Tools. Springer, Heidelberg (2001)"},{"issue":"3","key":"18_CR8","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R.E. Bryant","year":"1992","unstructured":"Bryant, R.E.: Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys\u00a024(3), 293\u2013318 (1992)","journal-title":"ACM Computing Surveys"},{"key":"18_CR9","series-title":"AMAST Series in Computing","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1142\/9789812831583_0005","volume-title":"Theories and Experiences for Real-Time System Development","author":"S. Campos","year":"1995","unstructured":"Campos, S., Clarke, E.M.: Real-time symbolic model checking for discrete time models. In: Theories and Experiences for Real-Time System Development. AMAST Series in Computing, vol.\u00a02, pp. 129\u2013145. World Scientific, Singapore (1995)"},{"key":"18_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/11539452_9","volume-title":"CONCUR 2005 \u2013 Concurrency Theory","author":"F. Cassez","year":"2005","unstructured":"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.\u00a03653, pp. 66\u201380. Springer, Heidelberg (2005)"},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Logics of Programs","author":"E.M. Clarke","year":"1982","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Kozen, D. (ed.) Logic of Programs 1981. LNCS, vol.\u00a0131, pp. 52\u201371. Springer, Heidelberg (1982)"},{"key":"18_CR12","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"18_CR13","series-title":"Lecture Notes in Computer Science","first-page":"142","volume-title":"CONCUR 2003 - Concurrency Theory","author":"L. Alfaro de","year":"2003","unstructured":"de Alfaro, L., Faella, M., Henzinger, T.A., Majumdar, R., Stoelinga, M.: The element of surprise in timed games. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol.\u00a02761, pp. 142\u2013156. Springer, Heidelberg (2003)"},{"key":"18_CR14","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/BF00355298","volume":"4","author":"E.A. Emerson","year":"1992","unstructured":"Emerson, E.A., Mok, A.K.-L., Sistla, A.P., Srinivasan, J.: Quantitative temporal reasoning. Real-Time Systems\u00a04, 331\u2013352 (1992)","journal-title":"Real-Time Systems"},{"key":"18_CR15","unstructured":"Jurdzi\u0144ski, M.: Countdown games. Personal communication (March 2006)"},{"key":"18_CR16","unstructured":"Laroussinie, F., Markey, N., Oreiby, G.: Expressiveness and complexity of\u00a0ATL. Research Report LSV-06-03, Laboratoire Sp\u00e9cification et V\u00e9rification, ENS Cachan, France (February 2006)"},{"issue":"1-3","key":"18_CR17","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/j.tcs.2005.11.020","volume":"353","author":"F. Laroussinie","year":"2006","unstructured":"Laroussinie, F., Markey, N., Schnoebelen, P.: Efficient timed model checking for discrete-time systems. Theoretical Computer Science\u00a0353(1-3), 249\u2013271 (2006)","journal-title":"Theoretical Computer Science"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"229","DOI":"10.1007\/3-540-59042-0_76","volume-title":"STACS 95","author":"O. Maler","year":"1995","unstructured":"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.\u00a0900, pp. 229\u2013242. Springer, Heidelberg (1995)"},{"key":"18_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-540-30206-3_9","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"N. Markey","year":"2004","unstructured":"Markey, N., Schnoebelen, P.: Symbolic model checking of simply-timed systems. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol.\u00a03253, pp. 102\u2013117. Springer, Heidelberg (2004)"},{"key":"18_CR20","unstructured":"McMillan, K.L.: Symbolic Model Checking: An Approach to the State Explosion Problem. PhD thesis, Carnegie Mellon University, Pittsburgh, PA, USA (1992)"},{"key":"18_CR21","first-page":"46","volume-title":"Proc. 18th IEEE Symp. Foundations of Computer Science (FOCS 1977)","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. Foundations of Computer Science (FOCS 1977), pp. 46\u201357. IEEE Comp. Soc. Press, Los Alamitos (1977)"},{"key":"18_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"International Symposium on Programming","author":"J.-P. Queille","year":"1982","unstructured":"Queille, J.-P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Dezani-Ciancaglini, M., Montanari, U. (eds.) Programming 1982. LNCS, vol.\u00a0137, pp. 337\u2013351. Springer, Heidelberg (1982)"},{"issue":"1","key":"18_CR23","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1109\/5.21072","volume":"77","author":"P.J. Ramadge","year":"1989","unstructured":"Ramadge, P.J., Wonham, W.M.: The control of discrete event systems. Proceedings of the IEEE\u00a077(1), 81\u201398 (1989)","journal-title":"Proceedings of the IEEE"},{"key":"18_CR24","unstructured":"Schobbens, P.-Y., Bontemps, Y.: Real-time concurrent game structures. Personal communication (December 2005)"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11867340_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T17:50:15Z","timestamp":1558288215000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11867340_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540450269","9783540450313"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/11867340_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}