Prefix-independent objectives over finite colors are positionally determined on vertex-colored one- and two-player games iff they are generalized parity objectives on ordered pairs of colors.
Infinite Games on Finitely Coloured Graphs with Applications to Automata on Infinite Trees
4 Pith papers cite this work, alongside 486 external citations. Polarity classification is still indexing.
representative citing papers
Fair parity/parity games with fairness constraints on both players are solvable via a polynomial gadget reduction to ordinary parity games or a direct symbolic fixpoint algorithm.
A neuro-symbolic system using large reasoning models and model checkers outperforms dedicated reactive synthesis tools on benchmarks and handles parameterized systems.
Obligation properties in LTLf+ admit a direct symbolic translation to deterministic weak automata, enabling linear-time synthesis via DWA games with effectiveness comparable to LTLf.
citing papers explorer
-
Positional Determinacy with Colored Vertices: a 1-to-2-Player Lift
Prefix-independent objectives over finite colors are positionally determined on vertex-colored one- and two-player games iff they are generalized parity objectives on ordered pairs of colors.
-
Doubly Fair Parity Games
Fair parity/parity games with fairness constraints on both players are solvable via a polynomial gadget reduction to ordinary parity games or a direct symbolic fixpoint algorithm.
-
Natural Synthesis: Outperforming Reactive Synthesis Tools with Large Reasoning Models
A neuro-symbolic system using large reasoning models and model checkers outperforms dedicated reactive synthesis tools on benchmarks and handles parameterized systems.
-
Symbolic Synthesis for LTLf+ Obligations
Obligation properties in LTLf+ admit a direct symbolic translation to deterministic weak automata, enabling linear-time synthesis via DWA games with effectiveness comparable to LTLf.