Chatterjee, Krishnendu ;
Dvorák, Wolfgang ;
Henzinger, Monika ;
Loitzenbauer, Veronika
Improved SetBased Symbolic Algorithms for Parity Games
Abstract
Graph games with omegaregular winning conditions provide a mathematical framework to analyze a wide range of problems in the analysis of reactive systems and programs (such as the synthesis of reactive systems, program repair, and the verification of branching time properties). Parity conditions are canonical forms to specify omegaregular winning conditions. Graph games with parity conditions are equivalent to mucalculus model checking, and thus a very important algorithmic problem. Symbolic algorithms are of great significance because they provide scalable algorithms for the analysis of large finitestate systems, as well as algorithms for the analysis of infinitestate systems with finite quotient. A setbased symbolic algorithm uses the basic set operations and the onestep predecessor operators.
We consider graph games with n vertices and parity conditions with c priorities (equivalently, a mucalculus formula with c alternations of least and greatest fixed points). While many explicit algorithms exist for graph games with parity conditions, for setbased symbolic algorithms there are only two algorithms (notice that we use space to refer to the number of sets stored by a symbolic algorithm): (a) the basic algorithm that requires O(n^c) symbolic operations and linear space; and (b) an improved algorithm that requires O(n^{c/2+1}) symbolic operations but also O(n^{c/2+1}) space (i.e., exponential space).
In this work we present two setbased symbolic algorithms for parity games: (a) our first algorithm requires O(n^{c/2+1}) symbolic operations and only requires linear space; and (b) developing on our first algorithm, we present an algorithm that requires O(n^{c/3+1}) symbolic operations and only linear space. We also present the first linear space setbased symbolic algorithm for parity games that requires at most a subexponential number of symbolic operations.
BibTeX  Entry
@InProceedings{chatterjee_et_al:LIPIcs:2017:7683,
author = {Krishnendu Chatterjee and Wolfgang Dvor{\'a}k and Monika Henzinger and Veronika Loitzenbauer},
title = {{Improved SetBased Symbolic Algorithms for Parity Games}},
booktitle = {26th EACSL Annual Conference on Computer Science Logic (CSL 2017)},
pages = {18:118:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770453},
ISSN = {18688969},
year = {2017},
volume = {82},
editor = {Valentin Goranko and Mads Dam},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2017/7683},
URN = {urn:nbn:de:0030drops76830},
doi = {10.4230/LIPIcs.CSL.2017.18},
annote = {Keywords: model checking, graph games, parity games, symbolic computation, progress measure}
}
16.08.2017
Keywords: 

model checking, graph games, parity games, symbolic computation, progress measure 
Seminar: 

26th EACSL Annual Conference on Computer Science Logic (CSL 2017)

Issue date: 

2017 
Date of publication: 

16.08.2017 