{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T01:02:53Z","timestamp":1743123773800,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031757747"},{"type":"electronic","value":"9783031757754"}],"license":[{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,11,13]],"date-time":"2024-11-13T00:00:00Z","timestamp":1731456000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"DOI":"10.1007\/978-3-031-75775-4_8","type":"book-chapter","created":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T07:26:35Z","timestamp":1731396395000},"page":"166-191","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Expectation vs. Reality: Towards Verification of\u00a0Psychological Games"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9022-7599","authenticated-orcid":false,"given":"Marta","family":"Kwiatkowska","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9326-4344","authenticated-orcid":false,"given":"Gethin","family":"Norman","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4137-8862","authenticated-orcid":false,"given":"David","family":"Parker","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6570-9737","authenticated-orcid":false,"given":"Gabriel","family":"Santos","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,11,13]]},"reference":[{"unstructured":"Andr\u00e9s, P.: From decision theory to game theory: reasoning about decisions of others (2024). Manuscript in Preparation, Cambridge University Press","key":"8_CR1"},{"doi-asserted-by":"crossref","unstructured":"Aslanyan, Z., Nielson, F., Parker, D.: Quantitative verification and synthesis of attack-defence scenarios. In: Proceedings of CSF 2016, pp. 105\u2013119. IEEE (2016)","key":"8_CR2","DOI":"10.1109\/CSF.2016.15"},{"unstructured":"Attanasi, G., Nagel, R.: A survey of psychological games: theoretical findings and experimental evidence. In: Innocenti, A., Sbriglia, P. (eds.) Games, Rationality and Behavior. Essays on Behavioral Game Theory and Experiments, pp. 204\u2013232 (2008)","key":"8_CR3"},{"key":"8_CR4","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1016\/j.jebo.2019.04.009","volume":"167","author":"P Battigalli","year":"2019","unstructured":"Battigalli, P., Corrao, R., Dufwenberg, M.: Incorporating belief-dependent motivation in games. J. Econ. Behav. Organ. 167, 185\u2013218 (2019)","journal-title":"J. Econ. Behav. Organ."},{"issue":"1","key":"8_CR5","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.jet.2008.01.004","volume":"144","author":"P Battigalli","year":"2009","unstructured":"Battigalli, P., Dufwenberg, M.: Dynamic psychological games. J. Econ. Theory 144(1), 1\u201335 (2009)","journal-title":"J. Econ. Theory"},{"issue":"3","key":"8_CR6","doi-asserted-by":"publisher","first-page":"833","DOI":"10.1257\/jel.20201378","volume":"60","author":"P Battigalli","year":"2022","unstructured":"Battigalli, P., Dufwenberg, M.: Belief-dependent motivations and psychological game theory. J. Econ. Lit. 60(3), 833\u201382 (2022)","journal-title":"J. Econ. Lit."},{"doi-asserted-by":"crossref","unstructured":"Bj\u00f8rnskau, T.: The zebra crossing game - using game theory to explain a discrepancy between road user behaviour and traffic rules. Saf. Sci. 92 (2015)","key":"8_CR7","DOI":"10.1016\/j.ssci.2015.10.007"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","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). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_63"},{"key":"8_CR9","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1007\/978-1-4757-2281-9_7","volume-title":"Economic and Financial Modeling with Mathematica","author":"J Dickhaut","year":"1993","unstructured":"Dickhaut, J., Kaplan, T.: A program for finding nash equilibria. In: Varian, H.R. (ed.) Economic and Financial Modeling with Mathematica, pp. 148\u2013166. Springer, New York (1993). https:\/\/doi.org\/10.1007\/978-1-4757-2281-9_7"},{"key":"8_CR10","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1016\/j.aap.2013.06.016","volume":"62","author":"R Elvik","year":"2014","unstructured":"Elvik, R.: A review of game-theoretic models of road user behaviour. Accid. Anal. Prev. 62, 388\u2013396 (2014)","journal-title":"Accid. Anal. Prev."},{"key":"8_CR11","doi-asserted-by":"publisher","DOI":"10.1016\/j.aap.2024.107604","volume":"203","author":"R Ezzati Amini","year":"2024","unstructured":"Ezzati Amini, R., Abouelela, M., Dhamaniya, A., Friedrich, B., Antoniou, C.: A game-theoretic approach for modelling pedestrian-vehicle conflict resolutions in uncontrolled traffic environments. Accid. Anal. Prev. 203, 107604 (2024)","journal-title":"Accid. Anal. Prev."},{"issue":"2","key":"8_CR12","doi-asserted-by":"publisher","first-page":"450","DOI":"10.1109\/TASE.2016.2530623","volume":"13","author":"L Feng","year":"2016","unstructured":"Feng, L., Wiltsche, C., Humphrey, L., Topcu, U.: Synthesis of human-in-the-loop control protocols for autonomous systems. IEEE Trans. Autom. Sci. Eng. 13(2), 450\u2013462 (2016)","journal-title":"IEEE Trans. Autom. Sci. Eng."},{"issue":"1","key":"8_CR13","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1016\/0899-8256(89)90005-5","volume":"1","author":"J Geanakoplos","year":"1989","unstructured":"Geanakoplos, J., Pearce, D., Stacchetti, E.: Psychological games and sequential rationality. Games Econom. Behav. 1(1), 60\u201379 (1989)","journal-title":"Games Econom. Behav."},{"issue":"1","key":"8_CR14","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1016\/S0022-0531(03)00005-X","volume":"110","author":"S Govindan","year":"2003","unstructured":"Govindan, S., Wilson, R.: A global Newton method to compute Nash equilibria. J. Econ. Theory 110(1), 65\u201386 (2003)","journal-title":"J. Econ. Theory"},{"unstructured":"Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2021). http:\/\/gurobi.com\/","key":"8_CR15"},{"issue":"4","key":"8_CR16","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/s10009-021-00633-z","volume":"24","author":"C Hensel","year":"2022","unstructured":"Hensel, C., Junges, S., Katoen, J.P., Quatmann, T., Volk, M.: The probabilistic model checker Storm. Int. J. Softw. Tools Technol. Transfer 24(4), 589\u2013610 (2022)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/978-3-030-01090-4_35","volume-title":"Automated Technology for Verification and Analysis","author":"J Gutierrez","year":"2018","unstructured":"Gutierrez, J., Najib, M., Perelli, G., Wooldridge, M.: EVE: a tool for temporal equilibrium analysis. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 551\u2013557. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_35"},{"key":"8_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"207","DOI":"10.1007\/978-3-319-99154-2_13","volume-title":"Quantitative Evaluation of Systems","author":"S Junges","year":"2018","unstructured":"Junges, S., Jansen, N., Katoen, J.-P., Topcu, U., Zhang, R., Hayhoe, M.: Model checking for safe navigation among humans. In: McIver, A., Horvath, A. (eds.) QEST 2018. LNCS, vol. 11024, pp. 207\u2013222. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-99154-2_13"},{"doi-asserted-by":"crossref","unstructured":"Karabag, M.O., Smith, S., Fridovich-Keil, D., Topcu, U.: Encouraging inferable behavior for autonomy: repeated bimatrix stackelberg games with observations (2023)","key":"8_CR19","DOI":"10.23919\/ACC60939.2024.10644936"},{"key":"8_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable Markov Chains","author":"J Kemeny","year":"1976","unstructured":"Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Springer, New York (1976). https:\/\/doi.org\/10.1007\/978-1-4684-9455-6"},{"issue":"2","key":"8_CR21","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1016\/0899-8256(92)90016-L","volume":"4","author":"V Kolpin","year":"1992","unstructured":"Kolpin, V.: Equilibrium refinement in psychological games. Games Econom. Behav. 4(2), 218\u2013231 (1992)","journal-title":"Games Econom. Behav."},{"key":"8_CR22","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). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-030-53291-8_25","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2020","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: PRISM-games 3.0: stochastic game verification with concurrency, equilibria and time. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 475\u2013487. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_25"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"74","DOI":"10.1007\/978-3-030-59854-9_7","volume-title":"Quantitative Evaluation of Systems","author":"M Kwiatkowska","year":"2020","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Multi-player equilibria verification for\u00a0concurrent stochastic games. In: Gribaudo, M., Jansen, D.N., Remke, A. (eds.) QEST 2020. LNCS, vol. 12289, pp. 74\u201395. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-59854-9_7"},{"key":"8_CR25","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/s10703-020-00356-y","volume":"58","author":"M Kwiatkowska","year":"2021","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Automatic verification of concurrent stochastic systems. Formal Methods Syst. Des. 58, 188\u2013250 (2021)","journal-title":"Formal Methods Syst. Des."},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-030-99527-0_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Kwiatkowska","year":"2022","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Santos, G.: Correlated equilibria and fairness in concurrent stochastic games. In: TACAS 2022. LNCS, vol. 13244, pp. 60\u201378. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_4"},{"issue":"3","key":"8_CR27","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1287\/moor.12.3.377","volume":"12","author":"GVD Laan","year":"1987","unstructured":"Laan, G.V.D., Talman, A.J.J., Heyden, L.V.D.: Simplicial variable dimension algorithms for solving the nonlinear complementarity problem on a product of unit simplices using a general labelling. Math. Oper. Res. 12(3), 377\u2013397 (1987)","journal-title":"Math. Oper. Res."},{"issue":"2","key":"8_CR28","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1137\/0112033","volume":"12","author":"C Lemke","year":"1964","unstructured":"Lemke, C., Howson, J.: Equilibrium points of bimatrix games. J. Soc. Ind. Appl. Math. 12(2), 413\u2013423 (1964)","journal-title":"J. Soc. Ind. Appl. Math."},{"doi-asserted-by":"crossref","unstructured":"Michieli, U., Badia, L.: Game theoretic analysis of road user safety scenarios involving autonomous vehicles. In: Proceedings of PIMRC 2018, pp. 1377\u20131381 (2018)","key":"8_CR29","DOI":"10.1109\/PIMRC.2018.8580679"},{"unstructured":"Porter, R., Nudelman, E., Shoham, Y.: Simple search methods for finding a Nash equilibrium. In: Proceedings of AAAI 2004, pp. 664\u2013669. AAAI Press (2004)","key":"8_CR30"},{"unstructured":"Rabin, M.: Incorporating fairness into game theory and economics. Am. Econ. Rev. 1281\u20131302 (1993)","key":"8_CR31"},{"unstructured":"Sandholm, T., Gilpin, A., Conitzer, V.: Mixed-integer programming methods for finding Nash equilibria. In: Proceedings of AAAI 2005, pp. 495\u2013501. AAAI Press (2005)","key":"8_CR32"},{"key":"8_CR33","doi-asserted-by":"publisher","first-page":"1095","DOI":"10.1073\/pnas.39.10.1095","volume":"39","author":"L Shapley","year":"1953","unstructured":"Shapley, L.: Stochastic games. Proc. Natl. Acad. Sci. 39, 1095\u20131100 (1953)","journal-title":"Proc. Natl. Acad. Sci."},{"doi-asserted-by":"crossref","unstructured":"Shirado, H., Kasahara, S., Christakis, N.A.: Emergence and collapse of reciprocity in semiautomatic driving coordination experiments with humans. Proc. Natl. Acad. Sci. 120(51) (2023)","key":"8_CR34","DOI":"10.1073\/pnas.2307804120"},{"key":"8_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"583","DOI":"10.1007\/978-3-319-25150-9_34","volume-title":"Theoretical Aspects of Computing - ICTAC 2015","author":"A Toumi","year":"2015","unstructured":"Toumi, A., Gutierrez, J., Wooldridge, M.: A tool for the automated verification of nash equilibria in concurrent games. In: Leucker, M., Rueda, C., Valencia, F.D. (eds.) ICTAC 2015. LNCS, vol. 9399, pp. 583\u2013594. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-25150-9_34"}],"container-title":["Lecture Notes in Computer Science","Principles of Verification: Cycling the Probabilistic Landscape"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-75775-4_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,12]],"date-time":"2024-11-12T08:03:13Z","timestamp":1731398593000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-75775-4_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,11,13]]},"ISBN":["9783031757747","9783031757754"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-75775-4_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024,11,13]]},"assertion":[{"value":"13 November 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}