{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,25]],"date-time":"2025-10-25T12:42:18Z","timestamp":1761396138385},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021,9]]},"abstract":"<jats:p>Rational verification is the problem of determining which temporal logic properties will hold in a multi-agent system, under the assumption that agents in the system  act rationally, by choosing strategies that collectively form a game-theoretic equilibrium. Previous work in this area has largely focussed on deterministic systems. In this paper, we develop the theory and algorithms for rational verification in probabilistic systems. We focus on concurrent stochastic games (CSGs), which can be used to model uncertainty and randomness in complex multi-agent environments. We study the rational verification problem for both non-cooperative games and cooperative games in the qualitative probabilistic setting. In the former case, we consider LTL properties satisfied by the Nash equilibria of the game and in the latter case LTL properties satisfied by the core. In both cases, we show that the problem is 2EXPTIME-complete, thus not harder than the much simpler verification problem of model checking LTL properties of systems modelled as Markov decision processes (MDPs).<\/jats:p>","DOI":"10.24963\/kr.2021\/30","type":"proceedings-article","created":{"date-parts":[[2021,10,11]],"date-time":"2021-10-11T16:45:56Z","timestamp":1633970756000},"page":"312-322","source":"Crossref","is-referenced-by-count":2,"title":["Rational Verification for Probabilistic Systems"],"prefix":"10.24963","author":[{"given":"Julian","family":"Gutierrez","sequence":"first","affiliation":[{"name":"Monash University"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lewis","family":"Hammond","sequence":"additional","affiliation":[{"name":"University of Oxford"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anthony W.","family":"Lin","sequence":"additional","affiliation":[{"name":"University of Kaiserslautern"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Muhammad","family":"Najib","sequence":"additional","affiliation":[{"name":"University of Kaiserslautern"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Wooldridge","sequence":"additional","affiliation":[{"name":"University of Oxford"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"10584","event":{"number":"18","sponsor":["Artificial Intelligence Journal","Principles of Knowledge Representation and Reasoning Inc.","Sea AI Lab","Potassco Solutions","European Association for Artificial Intelligence"],"acronym":"KR-2021","name":"18th International Conference on Principles of Knowledge Representation and Reasoning {KR-2021}","start":{"date-parts":[[2020,11,12]]},"theme":"Artificial Intelligence","location":"Hanoii, Vietnam","end":{"date-parts":[[2021,11,18]]}},"container-title":["Proceedings of the Eighteenth International Conference on Principles of Knowledge Representation and Reasoning"],"original-title":[],"deposited":{"date-parts":[[2021,10,11]],"date-time":"2021-10-11T16:46:14Z","timestamp":1633970774000},"score":1,"resource":{"primary":{"URL":"https:\/\/proceedings.kr.org\/2021\/30"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2021,9]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/kr.2021\/30","relation":{},"subject":[],"published":{"date-parts":[[2021,9]]}}}