Parity Games and Automata for Game Logic

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

Differential Game Logic

ACM Transactions on Computational Logic ◽

10.1145/2817824 ◽

2015 ◽

Vol 17 (1) ◽

pp. 1-51 ◽

Cited By ~ 13

Author(s):

André Platzer

Keyword(s):

Differential Game ◽

Game Logic

Download Full-text

Some model theory for game logics

Journal of Symbolic Logic ◽

10.2307/2273724 ◽

1979 ◽

Vol 44 (2) ◽

pp. 147-152

Author(s):

Judy Green

Keyword(s):

Model Theory ◽

Existence Theorems ◽

Semantic Interpretation ◽

Rule Based ◽

Game Logic ◽

Important Method ◽

Consistency Property ◽

Consistency Properties ◽

Model Existence

Consistency properties and their model existence theorems have provided an important method of constructing models for fragments of L∞ω. In [E] Ellentuck extended this construction to Suslin logic. One of his extensions, the Borel consistency property, has its extra rule based not on the semantic interpretation of the extra symbols but rather on a theorem of Sierpinski about the classical operation . In this paper we extend that consistency property to the game logic LG and use it to show how one can extend results about and its countable fragments to LG and certain of its countable fragments. The particular formation of LG which we use will allow in the game quantifier infinite alternation of countable conjunctions and disjunctions as well as infinite alternation of quantifiers. In this way LG can be viewed as an extension of Suslin logic.

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