English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Probabilistic model checking for stochastic games enables formal verificationof systems that comprise competing or collaborating entities operating in astochastic environment. Despite good progress in the area, existing approachesfocus on zero-sum goals and cannot reason about scenarios where entities areendowed with different objectives. In this paper, we propose probabilisticmodel checking techniques for concurrent stochastic games based on Nashequilibria. We extend the temporal logic rPATL (probabilistic alternating-timetemporal logic with rewards) to allow reasoning about players with distinctquantitative goals, which capture either the probability of an event occurringor a reward measure. We present algorithms to synthesise strategies that aresubgame perfect social welfare optimal Nash equilibria, i.e., where there is noincentive for any players to unilaterally change their strategy in any state ofthe game, whilst the combined probabilities or rewards are maximised. Weimplement our techniques in the PRISM-games tool and apply them to several casestudies, including network protocols and robot navigation, showing the benefitscompared to existing approaches.

Equilibria-based Probabilistic Model Checking for Concurrent Stochastic Games