A simple algorithm for solving qualitative probabilistic parity games

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

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

5 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 nonprobabilistic 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
Title of host publicationComputer Aided Verification
Subtitle of host publication28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings
EditorsSwarat Chaudhuri, Azadeh Farzan
Place of PublicationCham
Number of pages21
VolumePart II
ISBN (Electronic)978-3-319-41540-6
ISBN (Print)978-3-319-41539-0
Publication statusPublished - 2016
Externally publishedYes
Event28th International Conference on Computer Aided Verification, CAV 2016 - Toronto, Canada
Duration: 17 Jul 201623 Jul 2016
Conference number: 26

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference28th International Conference on Computer Aided Verification, CAV 2016
Abbreviated titleCAV


  • Recursive call
  • Winning strategy
  • Weak attractor
  • Winning region
  • Winning condition

Fingerprint Dive into the research topics of 'A simple algorithm for solving qualitative probabilistic parity games'. Together they form a unique fingerprint.

Cite this