A Simple Algorithm for Solving Qualitative Probabilistic Parity Games

Ernst Moritz Hahn, Sven Schewe, Andrea Turrini, Lijun Zhang

Research output: Contribution to conferencePaperpeer-review

6 Citations (Scopus)


In this paper, we develop an approach to find strategies that guarantee a property in systems that contain controllable, uncontrollable, and random vertices, resulting in probabilistic games. Such games are a reasonable abstraction of systems that comprise partial control over the system (reflected by controllable transitions), hostile nondeterminism (abstraction of the unknown, such as the behaviour of an attacker or a potentially hostile environment), and probabilistic transitions for the abstraction of unknown behaviour neutral to our goals. We exploit a simple and only mildly adjusted algorithm from the analysis of non-probabilistic systems, and use it to show that the qualitative analysis of probabilistic games inherits the much celebrated sub-exponential complexity from 2-player games. The simple structure of the exploited algorithm allows us to offer tool support for finding the desired strategy, if it exists, for the given systems and properties. Our experimental evaluation shows that our technique is powerful enough to construct simple strategies that guarantee the specified probabilistic temporal properties.
Original languageEnglish
Number of pages311
Publication statusPublished - 2016
Externally publishedYes
EventComputer Aided Verification - Toronto, Canada
Duration: 17 Jul 201623 Jul 2016
Conference number: 28


ConferenceComputer Aided Verification
Abbreviated titleCAV
Internet address


  • Recursive call
  • Winning Strategy
  • Weak Attractor
  • Merseyside
  • Winning Condition


Dive into the research topics of 'A Simple Algorithm for Solving Qualitative Probabilistic Parity Games'. Together they form a unique fingerprint.

Cite this