A Simple Algorithm for Solving Qualitative Probabilistic Parity Games

In this talk, 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. The talk is based on the CAV 2016 paper with the same title. It is joint work with Ernst Moritz Hahn, Andrea Turrini, and Lijun Zhang. The amazing thing about this approach is its simplicity and beauty. Instead of having a gadget based reduction to involved techniques, we use a straight-forward adaptation of a simple technique — and it turns out that 2. 5 player games are not that hard to solve.

Authors

• Sven Schewe

Keywords

No keywords are indexed for this paper.