Solving Parity Games Using an Automata-Based Algorithm

Higher-order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties

ACM Transactions on Computational Logic ◽

10.1145/3452917 ◽

2021 ◽

Vol 22 (2) ◽

pp. 1-37

Author(s):

Christopher H. Broadbent ◽

Arnaud Carayol ◽

C.-H. Luke Ong ◽

Olivier Serre

Keyword(s):

Model Checking ◽

Free Variable ◽

Higher Order ◽

Second Order ◽

Effective Solution ◽

Parity Games ◽

Transition Graphs ◽

Second Order Logic ◽

Pushdown Automata ◽

Monadic Second Order Logic

This article studies the logical properties of a very general class of infinite ranked trees, namely, those generated by higher-order recursion schemes. We consider, for both monadic second-order logic and modal -calculus, three main problems: model-checking, logical reflection (a.k.a. global model-checking, that asks for a finite description of the set of elements for which a formula holds), and selection (that asks, if exists, for some finite description of a set of elements for which an MSO formula with a second-order free variable holds). For each of these problems, we provide an effective solution. This is obtained, thanks to a known connection between higher-order recursion schemes and collapsible pushdown automata and on previous work regarding parity games played on transition graphs of collapsible pushdown automata.

Download Full-text

An Improved Recursive Algorithm for Parity Games

2014 Theoretical Aspects of Software Engineering Conference ◽

10.1109/tase.2014.24 ◽

2014 ◽

Cited By ~ 1

Author(s):

Yao Liu ◽

Zhenhua Duan ◽

Cong Tian

Keyword(s):

Recursive Algorithm ◽

Parity Games

Download Full-text

OBLIGATION BLACKWELL GAMES AND P-AUTOMATA

Journal of Symbolic Logic ◽

10.1017/jsl.2016.71 ◽

2017 ◽

Vol 82 (2) ◽

pp. 420-452

Author(s):

KRISHNENDU CHATTERJEE ◽

NIR PITERMAN

Keyword(s):

Markov Chains ◽

Decision Problem ◽

Value Function ◽

Acceptance Condition ◽

Parity Games ◽

The Value Function

AbstractWe generalize winning conditions in two-player games by adding a structural acceptance condition called obligations. Obligations are orthogonal to the linear winning conditions that define whether a play is winning. Obligations are a declaration that player 0 can achieve a certain value from a configuration. If the obligation is met, the value of that configuration for player 0 is 1.We define the value in such games and show that obligation games are determined. For Markov chains with Borel objectives and obligations, and finite turn-based stochastic parity games with obligations we give an alternative and simpler characterization of the value function. Based on this simpler definition we show that the decision problem of winning finite turn-based stochastic parity games with obligations is in NP∩co-NP. We also show that obligation games provide a game framework for reasoning about p-automata.

Download Full-text

Stochastic Parity Games on Lossy Channel Systems

Logical Methods in Computer Science ◽

10.2168/lmcs-10(4:21)2014 ◽

2015 ◽

Vol 10 (4) ◽

Author(s):

Parosh Abdulla ◽

Lorenzo Clemente ◽

Richard Mayr ◽

Sven Sandberg

Keyword(s):

Parity Games ◽

Lossy Channel ◽

Channel Systems

Download Full-text

A Discrete Stratety Improvement Algorithm for Solving Parity Games

BRICS Report Series ◽

10.7146/brics.v7i48.20215 ◽

2000 ◽

Vol 7 (48) ◽

Cited By ~ 1

Author(s):

Marcin Jurdzinski ◽

Jens Vöge

Keyword(s):

Linear Programming ◽

Conceptual Understanding ◽

Polynomial Time ◽

Stochastic Games ◽

Real Numbers ◽

Improvement Algorithm ◽

Winning Strategies ◽

Parity Games ◽

Present Algorithm ◽

Standing Problem

A discrete strategy improvement algorithm is given for constructing<br />winning strategies in parity games, thereby providing<br />also a new solution of the model-checking problem for the modal<br />-calculus. Known strategy improvement algorithms, as proposed<br />for stochastic games by Homan and Karp in 1966, and for discounted payoff games and parity games by Puri in 1995, work with real numbers and require solving linear programming instances involving high precision arithmetic. In the present algorithm for parity games these difficulties are avoided by the use of discrete vertex valuations in which information about the relevance of vertices and certain distances is coded. An efficient implementation is given for a strategy improvement step. Another advantage of the present approach is that it provides a better conceptual understanding and easier analysis of strategy improvement algorithms for parity games. However, so far it is not known whether the present algorithm works in polynomial time. The long standing problem whether parity games can be solved in polynomial time remains open.

Download Full-text