{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,3]],"date-time":"2026-07-03T11:21:23Z","timestamp":1783077683652,"version":"3.54.6"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319251493","type":"print"},{"value":"9783319251509","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-25150-9_34","type":"book-chapter","created":{"date-parts":[[2015,9,25]],"date-time":"2015-09-25T07:42:36Z","timestamp":1443166956000},"page":"583-594","source":"Crossref","is-referenced-by-count":13,"title":["A Tool for the Automated Verification of Nash Equilibria in Concurrent Games"],"prefix":"10.1007","author":[{"given":"Alexis","family":"Toumi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Julian","family":"Gutierrez","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Wooldridge","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,12,25]]},"reference":[{"key":"34_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"Computer Aided Verification","author":"R Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Mang, F., Qadeer, S., Rajamani, S., Tasiran, S.: MOCHA: modularity in model checking. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 521\u2013525. Springer, Heidelberg (1998)"},{"issue":"1","key":"34_CR2","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. Form. Meth. Syst. Des. 15(1), 7\u201348 (1999)","journal-title":"Form. Meth. Syst. Des."},{"key":"34_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/978-3-642-00768-2_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Berwanger","year":"2009","unstructured":"Berwanger, D., Chatterjee, K., De Wulf, M., Doyen, L., Henzinger, T.A.: Alpaga: a tool for solving parity games with imperfect information. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 58\u201361. Springer, Heidelberg (2009)"},{"key":"34_CR4","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"890","DOI":"10.1007\/978-3-642-39799-8_63","volume-title":"Computer Aided Verification","author":"R Brenguier","year":"2013","unstructured":"Brenguier, R.: PRALINE: a tool for computing nash equilibria in concurrent games. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 890\u2013895. Springer, Heidelberg (2013)"},{"key":"34_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"525","DOI":"10.1007\/978-3-319-08867-9_34","volume-title":"Computer Aided Verification","author":"P Cerm\u00e1k","year":"2014","unstructured":"Cerm\u00e1k, P., Lomuscio, A., Mogavero, F., Murano, A.: MCMAS-SLK: a model checker for the verification of strategy logic specifications. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 525\u2013532. Springer, Heidelberg (2014)"},{"key":"34_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"206","DOI":"10.1007\/978-3-662-46681-0_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A David","year":"2015","unstructured":"David, A., Jensen, P.G., Larsen, K.G., Mikucionis, M., Taankvist, J.H.: Uppaal Stratego. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 206\u2013211. Springer, Heidelberg (2015)"},{"key":"34_CR7","first-page":"996","volume-title":"Handbook of Theoretical Computer Science Volume B: Formal Models and Semantics","author":"EA Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science Volume B: Formal Models and Semantics, pp. 996\u20131072. Elsevier, Amsterdam (1990)"},{"key":"34_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1007\/978-3-642-12002-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Fisman","year":"2010","unstructured":"Fisman, D., Kupferman, O., Lustig, Y.: Rational synthesis. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 190\u2013204. Springer, Heidelberg (2010)"},{"key":"34_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-642-04761-9_15","volume-title":"Automated Technology for Verification and Analysis","author":"O Friedmann","year":"2009","unstructured":"Friedmann, O., Lange, M.: Solving parity games in practice. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 182\u2013196. Springer, Heidelberg (2009)"},{"key":"34_CR10","unstructured":"Gutierrez, J., Harrenstein, P., Wooldridge, M.: Iterated boolean games. In: IJCAI, IJCAI\/AAAI (2013)"},{"key":"34_CR11","unstructured":"Gutierrez, J., Harrenstein, P., Wooldridge, M.: Verification of temporal equilibrium properties of games on Reactive Modules. Technical report, University of Oxford (2015)"},{"issue":"2","key":"34_CR12","doi-asserted-by":"publisher","first-page":"322","DOI":"10.1006\/inco.2000.2893","volume":"164","author":"O Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M., Wolper, P.: Module checking. Inf. Comput. 164(2), 322\u2013344 (2001)","journal-title":"Inf. Comput."},{"key":"34_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"34_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"682","DOI":"10.1007\/978-3-642-02658-4_55","volume-title":"Computer Aided Verification","author":"A Lomuscio","year":"2009","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: a model checker for the verification of multi-agent systems. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 682\u2013688. Springer, Heidelberg (2009)"},{"key":"34_CR15","volume-title":"A Course in Game Theory","author":"MJ Osborne","year":"1994","unstructured":"Osborne, M.J., Rubinstein, A.: A Course in Game Theory. MIT Press, Cambridge (1994)"},{"key":"34_CR16","unstructured":"Prezza, N.: CTLSAT (2015). \n                      https:\/\/github.com\/nicolaprezza\/CTLSAT"},{"key":"34_CR17","unstructured":"Reynaud, D., Mr. Waffles: (2015). \n                      http:\/\/mrwaffles.gforge.inria.fr"},{"key":"34_CR18","unstructured":"Toumi, A.: Equilibrium checking in Reactive Modules games. Technical report, Department of Computer Science, University of Oxford (2015)"},{"key":"34_CR19","doi-asserted-by":"crossref","unstructured":"van der Hoek, W., Lomuscio, A., Wooldridge, M.: On the complexity of practical ATL model checking. In: AAMAS, pp. 201\u2013208. ACM (2006)","DOI":"10.1145\/1160633.1160665"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing - ICTAC 2015"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-25150-9_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T21:50:44Z","timestamp":1559253044000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-25150-9_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319251493","9783319251509"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-25150-9_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}