2018/11/17 by Marta Kwiatkowska, Gethin Norman, Kwiatkowska, Marta +5 · 1 citation
Computer Science · #Advanced Software Engineering Methodologies #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Multi-Agent Systems and Negotiation
paper · pdf · doi:10.48550/arxiv.1811.07145
openalex publication_date 2018/11/17 · openalex created_date 2022/08/02 · openalex updated_date 2026/07/28
Probabilistic model checking for stochastic games enables formal verification\nof systems that comprise competing or collaborating entities operating in a\nstochastic environment. Despite good progress in the area, existing approaches\nfocus on zero-sum goals and cannot reason about scenarios where entities are\nendowed with different objectives. In this paper, we propose probabilistic\nmodel checking techniques for concurrent stochastic games based on Nash\nequilibria. We extend the temporal logic rPATL (probabilistic alternating-time\ntemporal logic with rewards) to allow reasoning about players with distinct\nquantitative goals, which capture either the probability of an event occurring\nor a reward measure. We present algorithms to synthesise strategies that are\nsubgame perfect social welfare optimal Nash equilibria, i.e., where there is no\nincentive for any players to unilaterally change their strategy in any state of\nthe game, whilst the combined probabilities or rewards are maximised. We\nimplement our techniques in the PRISM-games tool and apply them to several case\nstudies, including network protocols and robot navigation, showing the benefits\ncompared to existing approaches.\n