{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:10:07Z","timestamp":1760202607799,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540407539"},{"type":"electronic","value":"9783540451877"}],"license":[{"start":{"date-parts":[[2003,1,1]],"date-time":"2003-01-01T00:00:00Z","timestamp":1041379200000},"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":[[2003]]},"DOI":"10.1007\/978-3-540-45187-7_8","type":"book-chapter","created":{"date-parts":[[2010,6,25]],"date-time":"2010-06-25T22:38:49Z","timestamp":1277505529000},"page":"128-143","source":"Crossref","is-referenced-by-count":10,"title":["Playing Games with Boxes and Diamonds"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[]},{"given":"Salvatore","family":"La Torre","sequence":"additional","affiliation":[]},{"given":"P.","family":"Madhusudan","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0035748","volume-title":"Automata, Languages and Programming","author":"M. Abadi","year":"1989","unstructured":"Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: Ronchi Della Rocca, S., Ausiello, G., Dezani-Ciancaglini, M. (eds.) ICALP 1989. LNCS, vol.\u00a0372, pp. 1\u201317. Springer, Heidelberg (1989)"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/3-540-48320-9_8","volume-title":"CONCUR\u201999. Concurrency Theory","author":"R. Alur","year":"1999","unstructured":"Alur, R., de Alfaro, L., Henzinger, T., Mang, F.: Automating modular verification. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 82\u201397. Springer, Heidelberg (1999)"},{"issue":"5","key":"8_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/585265.585270","volume":"49","author":"R. Alur","year":"2002","unstructured":"Alur, R., Henzinger, T., Kupferman, O.: Alternating-time temporal logic. Journal of the ACM\u00a049(5), 1\u201342 (2002)","journal-title":"Journal of the ACM"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R., La Torre, S.: Deterministic generators and games for LTL fragments. In: Proc. of LICS 2001, pp. 291\u2013302 (2001)","DOI":"10.1109\/LICS.2001.932505"},{"issue":"1","key":"8_CR5","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"A. Chandra","year":"1981","unstructured":"Chandra, A., Kozen, D., Stockmeyer, L.: Alternation. Journal of the ACM\u00a028(1), 114\u2013133 (1981)","journal-title":"Journal of the ACM"},{"key":"8_CR6","series-title":"Distinguished Dissertation Series.","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/6874.001.0001","volume-title":"Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits","author":"D. Dill","year":"1989","unstructured":"Dill, D.: Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits. Distinguished Dissertation Series. MIT Press, Cambridge (1989)"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Emerson, E., Jutla, C.: The complexity of tree automata and logics of programs. In: Proc. of FOCS 1988, pp. 328\u2013337 (1988)","DOI":"10.1109\/SFCS.1988.21949"},{"issue":"5","key":"8_CR8","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"Holzmann, G.: The model checker SPIN. IEEE Transactions on Software Engineeri ng\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineeri ng"},{"key":"8_CR9","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J. Hopcroft","year":"1979","unstructured":"Hopcroft, J., Ullman, J.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)"},{"key":"8_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1007\/3-540-61474-5_59","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"1996","unstructured":"Kupferman, O., Vardi, M.: Module checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 75\u201386. Springer, Heidelberg (1996)"},{"key":"8_CR11","volume-title":"The temporal logic of reactive and concurrent systems: Specification","author":"Z. Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems: Specification. Springer, Heidelberg (1991)"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/3-540-45793-3_18","volume-title":"Computer Science Logic","author":"J. Marcinkowski","year":"2002","unstructured":"Marcinkowski, J., Truderung, T.: Optimal complexity bounds for positive ltl games. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, pp. 262\u2013275. Springer, Heidelberg (2002)"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. of FOCS 1977, pp. 46\u201377 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. of POPL 1989, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"8_CR15","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A. Sistla","year":"1985","unstructured":"Sistla, A., Clarke, E.: The complexity of propositional linear temporal logics. The Journal of the ACM\u00a032, 733\u2013749 (1985)","journal-title":"The Journal of the ACM"},{"key":"8_CR16","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y., Stockmeyer, L.: Improved upper and lower bounds for modal logics of programs. In: Proc. 17th Symp. on Theory of Computing, pp. 240\u2013251 (1985)","DOI":"10.1145\/22145.22173"},{"key":"8_CR17","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1016\/S0304-3975(98)00009-7","volume":"200","author":"W. Zielonka","year":"1998","unstructured":"Zielonka, W.: Infinite games on finitely coloured graphs with applications to automata on infinite trees. Theoretical Computer Science\u00a0200, 135\u2013183 (1998)","journal-title":"Theoretical Computer Science"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2003 - Concurrency Theory"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-45187-7_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,22]],"date-time":"2025-02-22T07:57:21Z","timestamp":1740211041000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-45187-7_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540407539","9783540451877"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-45187-7_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}