A Simple Algorithm for Solving Qualitative Probabilistic Parity Games

Hahn, Ernst Moritz, Schewe, Sven ORCID: 0000-0002-9093-9518, Turrini, Andrea and Zhang, Lijun (2016) A Simple Algorithm for Solving Qualitative Probabilistic Parity Games. In: Computer Aided Verification: 28th International Conference, CAV 2016, 2016-7-17 - 2016-7-23, Toronto, ON, Canada.

Text 156.pdf - Author Accepted Manuscript Download (397kB)

Abstract

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.

Item Type:	Conference or Workshop Item (Unspecified)
Depositing User:	Symplectic Admin
Date Deposited:	22 Feb 2017 10:39
Last Modified:	19 Jan 2023 07:19
DOI:	10.1007/978-3-319-41540-6_16
Related URLs:	Author Publisher
URI:	https://livrepository.liverpool.ac.uk/id/eprint/3005466