TY - GEN
T1 - Parity games and automata for game logic
AU - Hansen, Helle Hvid
AU - Kupke, Clemens
AU - Marti, Johannes
AU - Venema, Yde
PY - 2018
Y1 - 2018
N2 - Parikh’s game logic is a PDL-like fixpoint logic interpreted on monotone neighbourhood frames that represent the strategic power of players in determined two-player games. Game logic translates into a fragment of the monotone μ -calculus, which in turn is expressively equivalent to monotone modal automata. Parity games and automata are important tools for dealing with the combinatorial complexity of nested fixpoints in modal fixpoint logics, such as the modal μ -calculus. In this paper, we (1) discuss the semantics a of game logic over neighbourhood structures in terms of parity games, and (2) use these games to obtain an automata-theoretic characterisation of the fragment of the monotone μ -calculus that corresponds to game logic. Our proof makes extensive use of structures that we call syntax graphs that combine the ease-of-use of syntax trees of formulas with the flexibility and succinctness of automata. They are essentially a graph-based view of the alternating tree automata that were introduced by Wilke in the study of modal μ -calculus.
AB - Parikh’s game logic is a PDL-like fixpoint logic interpreted on monotone neighbourhood frames that represent the strategic power of players in determined two-player games. Game logic translates into a fragment of the monotone μ -calculus, which in turn is expressively equivalent to monotone modal automata. Parity games and automata are important tools for dealing with the combinatorial complexity of nested fixpoints in modal fixpoint logics, such as the modal μ -calculus. In this paper, we (1) discuss the semantics a of game logic over neighbourhood structures in terms of parity games, and (2) use these games to obtain an automata-theoretic characterisation of the fragment of the monotone μ -calculus that corresponds to game logic. Our proof makes extensive use of structures that we call syntax graphs that combine the ease-of-use of syntax trees of formulas with the flexibility and succinctness of automata. They are essentially a graph-based view of the alternating tree automata that were introduced by Wilke in the study of modal μ -calculus.
UR - http://resolver.tudelft.nl/uuid:caac78d7-d837-4327-bf6e-d8ff5e69499c
UR - http://www.scopus.com/inward/record.url?scp=85041131521&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-73579-5_8
DO - 10.1007/978-3-319-73579-5_8
M3 - Conference contribution
AN - SCOPUS:85041131521
SN - 9783319735788
VL - 10669 LNCS
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 115
EP - 132
BT - Dynamic Logic. New Trends and Applications - 1st International Workshop, DALI 2017, Proceedings
PB - Springer
T2 - 1st International Workshop on Dynamic Logic, DALI 2017
Y2 - 23 September 2017 through 24 September 2017
ER -