Nathanaël Fijalkow and Martin Zimmermann.
Cost-parity and Cost-Streett Games,
Foundations of Software Technology and Theoretical Computer Science, FSTTCS'2012.
(HAL)
We consider games played on graphs equipped with costs on edges, and introduce two winning conditions, cost-parity and cost-Streett, which require bounds on the cost between requests and their responses. Both conditions generalize the corresponding classical omega-regular conditions as well as the corresponding finitary conditions. For cost-parity games we show that the first player has positional winning strategies and that determining the winner lies in NP and co-NP. For cost-Streett games we show that the first player has finite-state winning strategies and that determining the winner is EXPTIME-complete. This unifies the complexity results for the classical and finitary variants of these games. Both types of cost-games can be solved by solving linearly many instances of their classical variants.
[FGO12]
Nathanaël Fijalkow, Hugo Gimbert and Youssouf Oualhadj.
Deciding the Value 1 Problem for Probabilistic Leaktight Automata,
Logic in Computer Science, LICS'2012.
(HAL)
The value 1 problem is a decision problem for probabilistic automata over finite words: given a probabilistic automaton A, are there words accepted by A with probability arbitrarily close to 1? This problem was proved undecidable recently. We sharpen this result, showing that the undecidability result holds even if the probabilistic automata have only one probabilistic transition. Our main contribution is to introduce a new class of probabilistic automata, called leaktight automata, for which the value 1 problem is shown decidable (and PSPACE-complete). We construct an algorithm based on the computation of a monoid abstracting the behaviours of the automaton, and rely on algebraic techniques developed by Simon for the correctness proof. The class of leaktight automata is decidable in PSPACE, subsumes all subclasses of probabilistic automata whose value 1 problem is known to be decidable (in particular deterministic automata), and is closed under two natural composition operators.
2011
[CF11b]
Krishnendu Chatterjee and Nathanaël Fijalkow.
A reduction from parity games to simple stochastic games, In
Games, Automata, Logics and Formal Verification, GanDALF'2011.
(ArXiv)
Games on graphs provide a natural model for reactive non-terminating systems. In such games, the interaction of two players on an arena results in an infinite path that describes a run of the system. Different settings are used to model various open systems in computer science, as for instance turn-based or concurrent moves, and deterministic or stochastic transitions. In this paper, we are interested in turn-based games, and specifically in deterministic parity games and stochastic reachability games (also known as simple stochastic games). We present a simple, direct and efficient reduction from deterministic parity games to simple stochastic games: it yields an arena whose size is linear up to a logarithmic factor in size of the original arena.
[CF11a]
Krishnendu Chatterjee and Nathanaël Fijalkow.
Finitary languages, In
Language and Automata Theory and Applications, LATA'2011.
(HAL)
The class of omega-regular languages provides a robust specification language in verification. Every omega-regular condition can be decomposed into a safety part and a liveness part. The liveness part ensures that something good happens "eventually". Finitary liveness was proposed by Alur and Henzinger as a stronger formulation of liveness. It requires that there exists an unknown, fixed bound b such that something good happens within b transitions. In this work we consider automata with finitary acceptance conditions defined by finitary Buchi, parity and Streett languages. We study languages expressible by such automata: we give their topological complexity and present a regular-expression characterization. We compare the expressive power of finitary automata and give optimal algorithms for classical decisions questions. We show that the finitary languages are Sigma 2-complete; we present a complete picture of the expressive power of various classes of automata with finitary and infinitary acceptance conditions; we show that the languages defined by finitary parity automata exactly characterize the star-free fragment of omega B-regular languages; and we show that emptiness is NLOGSPACE-complete and universality as well as language inclusion are PSPACE-complete for finitary parity and Streett automata.
Unpublished (technical reports)
2013
[CF13]
Krishnendu Chatterjee and Nathanaël Fijalkow.
Infinite-state games with finitary conditions,
Technical report, 2013.
(HAL)
We study two-player zero-sum games over infinite-state graphs equipped with finitary conditions. Such conditions refine the classical omega-regular conditions: instead of requiring that good events occur infinitely often, they ensure the existence of a bound B such that in the limit good events occur within B steps. Our first contribution is to give (non-effective) characterizations of the winning regions for finitary games over countably infinite-state graphs. From these results we obtain the strategy complexity, i.e the memory required for winning strategies: we prove that memoryless strategies are sufficient for finitary Büchi, and finite memory suffices for finitary parity. We then study pushdown games with finitary conditions, with two contributions. First we prove a collapse result for pushdown games with finitary conditions, implying the decidability of solving these games. Second we consider pushdown games with finitary parity along with stack boundedness conditions, and show that solving these games is EXPTIME-complete.
2010
[FH10]
Nathanaël Fijalkow and Florian Horn.
The surprizing complexity of generalized reachability games,
Technical report, 2010.
(HAL)
Games on graphs provide a natural and powerful model for reactive systems. In this paper, we consider generalized reachability objectives, defined as conjunctions of reachability objectives. We first prove that deciding the winner in such games is PSPACE-complete, although it is fixed-parameter tractable with the number of reachability objectives as parameter. Moreover, we consider the memory requirements for both players and give matching upper and lower bounds on the size of winning strategies. In order to allow more efficient algorithms, we consider subclasses of generalized reachability games. We show that bounding the size of the reachability sets gives two natural subclasses where deciding the winner can be done efficiently.
Mathematics
[RMS-122-1]
Nathanaël Fijalkow.
Conjugation (conjugaison),
Revue des Mathématiques Spéciales, RMS 122-1.
(PDF, in French)
[RMS-118-4]
Nathanaël Fijalkow and Quentin Martin-Laval.
A Geometric Approach to 2*2 Matrices' Equivalence Classes (une étude géométrique des classes de similitude des matrices 2x2),
Revue des Mathématiques Spéciales, RMS 118-4.
(PDF, in French)
