Search Results

Documents authored by Fijalkow, Nathanael

Found 2 Possible Name Variants:

Fijalkow, Nathanael

Document
DOI: 10.4230/DagRep.13.9.166
The Futures of Reactive Synthesis (Dagstuhl Seminar 23391)

Authors: Nathanaël Fijalkow, Bernd Finkbeiner, Guillermo A. Pérez, Elizabeth Polgreen, and Rémi Morvan

Published in: Dagstuhl Reports, Volume 13, Issue 9 (2024)

Abstract
The Dagstuhl Seminar 23391 "The Futures of Reactive Synthesis" held in September 2023 was meant to gather neighbouring communities on a joint goal: Reactive Synthesis. We identified five trends: neural-symbolic computation, template-based solving for constraint programming, symbolic algorithms, syntax-guided synthesis, and model learning; and the objective was to discuss the potential futures of the field.
Cite as

Nathanaël Fijalkow, Bernd Finkbeiner, Guillermo A. Pérez, Elizabeth Polgreen, and Rémi Morvan. The Futures of Reactive Synthesis (Dagstuhl Seminar 23391). In Dagstuhl Reports, Volume 13, Issue 9, pp. 166-184, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{fijalkow_et_al:DagRep.13.9.166,
  author =	{Fijalkow, Nathana\"{e}l and Finkbeiner, Bernd and P\'{e}rez, Guillermo A. and Polgreen, Elizabeth and Morvan, R\'{e}mi},
  title =	{{The Futures of Reactive Synthesis (Dagstuhl Seminar 23391)}},
  pages =	{166--184},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{13},
  number =	{9},
  editor =	{Fijalkow, Nathana\"{e}l and Finkbeiner, Bernd and P\'{e}rez, Guillermo A. and Polgreen, Elizabeth and Morvan, R\'{e}mi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.9.166},
  URN =		{urn:nbn:de:0030-drops-198259},
  doi =		{10.4230/DagRep.13.9.166},
  annote =	{Keywords: program synthesis, program verification, reactive synthesis, temporal synthesis}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.118
How to Play Optimally for Regular Objectives?

Authors: Patricia Bouyer, Nathanaël Fijalkow, Mickael Randour, and Pierre Vandenhove

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
This paper studies two-player zero-sum games played on graphs and makes contributions toward the following question: given an objective, how much memory is required to play optimally for that objective? We study regular objectives, where the goal of one of the two players is that eventually the sequence of colors along the play belongs to some regular language of finite words. We obtain different characterizations of the chromatic memory requirements for such objectives for both players, from which we derive complexity-theoretic statements: deciding whether there exist small memory structures sufficient to play optimally is NP-complete for both players. Some of our characterization results apply to a more general class of objectives: topologically closed and topologically open sets.
Cite as

Patricia Bouyer, Nathanaël Fijalkow, Mickael Randour, and Pierre Vandenhove. How to Play Optimally for Regular Objectives?. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 118:1-118:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.ICALP.2023.118,
  author =	{Bouyer, Patricia and Fijalkow, Nathana\"{e}l and Randour, Mickael and Vandenhove, Pierre},
  title =	{{How to Play Optimally for Regular Objectives?}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{118:1--118:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.118},
  URN =		{urn:nbn:de:0030-drops-181700},
  doi =		{10.4230/LIPIcs.ICALP.2023.118},
  annote =	{Keywords: two-player games on graphs, strategy complexity, regular languages, finite-memory strategies, NP-completeness}
}
Document
DOI: 10.4230/LIPIcs.CP.2021.43
Statistical Comparison of Algorithm Performance Through Instance Selection

Authors: Théo Matricon, Marie Anastacio, Nathanaël Fijalkow, Laurent Simon, and Holger H. Hoos

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract
Empirical performance evaluations, in competitions and scientific publications, play a major role in improving the state of the art in solving many automated reasoning problems, including SAT, CSP and Bayesian network structure learning (BNSL). To empirically demonstrate the merit of a new solver usually requires extensive experiments, with computational costs of CPU years. This not only makes it difficult for researchers with limited access to computational resources to test their ideas and publish their work, but also consumes large amounts of energy. We propose an approach for comparing the performance of two algorithms: by performing runs on carefully chosen instances, we obtain a probabilistic statement on which algorithm performs best, trading off between the computational cost of running algorithms and the confidence in the result. We describe a set of methods for this purpose and evaluate their efficacy on diverse datasets from SAT, CSP and BNSL. On all these datasets, most of our approaches were able to choose the correct algorithm with about 95% accuracy, while using less than a third of the CPU time required for a full comparison; the best methods reach this level of accuracy within less than 15% of the CPU time for a full comparison.
Cite as

Théo Matricon, Marie Anastacio, Nathanaël Fijalkow, Laurent Simon, and Holger H. Hoos. Statistical Comparison of Algorithm Performance Through Instance Selection. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 43:1-43:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{matricon_et_al:LIPIcs.CP.2021.43,
  author =	{Matricon, Th\'{e}o and Anastacio, Marie and Fijalkow, Nathana\"{e}l and Simon, Laurent and Hoos, Holger H.},
  title =	{{Statistical Comparison of Algorithm Performance Through Instance Selection}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{43:1--43:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.43},
  URN =		{urn:nbn:de:0030-drops-153346},
  doi =		{10.4230/LIPIcs.CP.2021.43},
  annote =	{Keywords: Performance assessment, early stopping, automated reasoning solvers}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.123
Optimal Transformations of Games and Automata Using Muller Conditions

Authors: Antonio Casares, Thomas Colcombet, and Nathanaël Fijalkow

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
We consider the following question: given an automaton or a game with a Muller condition, how can we efficiently construct an equivalent one with a parity condition? There are several examples of such transformations in the literature, including in the determinisation of Büchi automata. We define a new transformation called the alternating cycle decomposition, inspired and extending Zielonka’s construction. Our transformation operates on transition systems, encompassing both automata and games, and preserves semantic properties through the existence of a locally bijective morphism. We show a strong optimality result: the obtained parity transition system is minimal both in number of states and number of priorities with respect to locally bijective morphisms. We give two applications: the first is related to the determinisation of Büchi automata, and the second is to give crisp characterisations on the possibility of relabelling automata with different acceptance conditions.
Cite as

Antonio Casares, Thomas Colcombet, and Nathanaël Fijalkow. Optimal Transformations of Games and Automata Using Muller Conditions. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 123:1-123:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{casares_et_al:LIPIcs.ICALP.2021.123,
  author =	{Casares, Antonio and Colcombet, Thomas and Fijalkow, Nathana\"{e}l},
  title =	{{Optimal Transformations of Games and Automata Using Muller Conditions}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{123:1--123:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.123},
  URN =		{urn:nbn:de:0030-drops-141928},
  doi =		{10.4230/LIPIcs.ICALP.2021.123},
  annote =	{Keywords: Automata over infinite words, Omega regular languages, Determinisation of automata}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2020.34
Value Iteration Using Universal Graphs and the Complexity of Mean Payoff Games

Authors: Nathanaël Fijalkow, Paweł Gawrychowski, and Pierre Ohlmann

Published in: LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

Abstract
We study the computational complexity of solving mean payoff games. This class of games can be seen as an extension of parity games, and they have similar complexity status: in both cases solving them is in NP ∩ coNP and not known to be in P. In a breakthrough result Calude, Jain, Khoussainov, Li, and Stephan constructed in 2017 a quasipolynomial time algorithm for solving parity games, which was quickly followed by a few other algorithms with the same complexity. Our objective is to investigate how these techniques can be extended to mean payoff games. The starting point is the combinatorial notion of universal trees: all quasipolynomial time algorithms for parity games have been shown to exploit universal trees. Universal graphs extend universal trees to arbitrary (positionally determined) objectives. We show that they yield a family of value iteration algorithms for solving mean payoff games which includes the value iteration algorithm due to Brim, Chaloupka, Doyen, Gentilini, and Raskin. The contribution of this paper is to prove tight bounds on the complexity of algorithms for mean payoff games using universal graphs. We consider two parameters: the largest weight N in absolute value and the number k of weights. The dependence in N in the existing value iteration algorithm is linear, we show that this can be improved to N^{1 - 1/n} and obtain a matching lower bound. However, we show that we cannot break the linear dependence in the exponent in the number k of weights implying that universal graphs do not yield a quasipolynomial time algorithm for solving mean payoff games.
Cite as

Nathanaël Fijalkow, Paweł Gawrychowski, and Pierre Ohlmann. Value Iteration Using Universal Graphs and the Complexity of Mean Payoff Games. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 34:1-34:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.MFCS.2020.34,
  author =	{Fijalkow, Nathana\"{e}l and Gawrychowski, Pawe{\l} and Ohlmann, Pierre},
  title =	{{Value Iteration Using Universal Graphs and the Complexity of Mean Payoff Games}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{34:1--34:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Esparza, Javier and Kr\'{a}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.34},
  URN =		{urn:nbn:de:0030-drops-127011},
  doi =		{10.4230/LIPIcs.MFCS.2020.34},
  annote =	{Keywords: Mean payoff games, Universal graphs, Value iteration}
}
Document
DOI: 10.4230/LIPIcs.STACS.2020.24
Lower Bounds for Arithmetic Circuits via the Hankel Matrix

Authors: Nathanaël Fijalkow, Guillaume Lagarde, Pierre Ohlmann, and Olivier Serre

Published in: LIPIcs, Volume 154, 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)

Abstract
We study the complexity of representing polynomials by arithmetic circuits in both the commutative and the non-commutative settings. To analyse circuits we count their number of parse trees, which describe the non-associative computations realised by the circuit. In the non-commutative setting a circuit computing a polynomial of degree d has at most 2^{O(d)} parse trees. Previous superpolynomial lower bounds were known for circuits with up to 2^{d^{1/3-ε}} parse trees, for any ε > 0. Our main result is to reduce the gap by showing a superpolynomial lower bound for circuits with just a small defect in the exponent for the total number of parse trees, that is 2^{d^{1 - ε}}, for any ε > 0. In the commutative setting a circuit computing a polynomial of degree d has at most 2^{O(d log d)} parse trees. We show a superpolynomial lower bound for circuits with up to 2^{d^{1/3 - ε}} parse trees, for any ε > 0. When d is polylogarithmic in n, we push this further to up to 2^{d^{1 - ε}} parse trees. While these two main results hold in the associative setting, our approach goes through a precise understanding of the more restricted setting where multiplication is not associative, meaning that we distinguish the polynomials (xy)z and x(yz). Our first and main conceptual result is a characterization result: we show that the size of the smallest circuit computing a given non-associative polynomial is exactly the rank of a matrix constructed from the polynomial and called the Hankel matrix. This result applies to the class of all circuits in both commutative and non-commutative settings, and can be seen as an extension of the seminal result of Nisan giving a similar characterization for non-commutative algebraic branching programs. Our key technical contribution is to provide generic lower bound theorems based on analyzing and decomposing the Hankel matrix, from which we derive the results mentioned above. The study of the Hankel matrix also provides a unifying approach for proving lower bounds for polynomials in the (classical) associative setting. We demonstrate this by giving alternative proofs of recent lower bounds as corollaries of our generic lower bound results.
Cite as

Nathanaël Fijalkow, Guillaume Lagarde, Pierre Ohlmann, and Olivier Serre. Lower Bounds for Arithmetic Circuits via the Hankel Matrix. In 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 154, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.STACS.2020.24,
  author =	{Fijalkow, Nathana\"{e}l and Lagarde, Guillaume and Ohlmann, Pierre and Serre, Olivier},
  title =	{{Lower Bounds for Arithmetic Circuits via the Hankel Matrix}},
  booktitle =	{37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)},
  pages =	{24:1--24:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-140-5},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{154},
  editor =	{Paul, Christophe and Bl\"{a}ser, Markus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2020.24},
  URN =		{urn:nbn:de:0030-drops-118859},
  doi =		{10.4230/LIPIcs.STACS.2020.24},
  annote =	{Keywords: Arithmetic Circuit Complexity, Lower Bounds, Parse Trees, Hankel Matrix}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.9
A Robust Class of Linear Recurrence Sequences

Authors: Corentin Barloy, Nathanaël Fijalkow, Nathan Lhote, and Filip Mazowiecki

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
We introduce a subclass of linear recurrence sequences which we call poly-rational sequences because they are denoted by rational expressions closed under sum and product. We show that this class is robust by giving several characterisations: polynomially ambiguous weighted automata, copyless cost-register automata, rational formal series, and linear recurrence sequences whose eigenvalues are roots of rational numbers.
Cite as

Corentin Barloy, Nathanaël Fijalkow, Nathan Lhote, and Filip Mazowiecki. A Robust Class of Linear Recurrence Sequences. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{barloy_et_al:LIPIcs.CSL.2020.9,
  author =	{Barloy, Corentin and Fijalkow, Nathana\"{e}l and Lhote, Nathan and Mazowiecki, Filip},
  title =	{{A Robust Class of Linear Recurrence Sequences}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{9:1--9:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.9},
  URN =		{urn:nbn:de:0030-drops-116521},
  doi =		{10.4230/LIPIcs.CSL.2020.9},
  annote =	{Keywords: linear recurrence sequences, weighted automata, cost-register automata}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.23
Quantifying Bounds in Strategy Logic

Authors: Nathanaël Fijalkow, Bastien Maubert, Aniello Murano, and Sasha Rubin

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
Program synthesis constructs programs from specifications in an automated way. Strategy Logic (SL) is a powerful and versatile specification language whose goal is to give theoretical foundations for program synthesis in a multi-agent setting. One limitation of Strategy Logic is that it is purely qualitative. For instance it cannot specify quantitative properties of executions such as "every request is quickly granted", or quantitative properties of trees such as "most executions of the system terminate". In this work, we extend Strategy Logic to include quantitative aspects in a way that can express bounds on "how quickly" and "how many". We define Prompt Strategy Logic, which encompasses Prompt LTL (itself an extension of LTL with a prompt eventuality temporal operator), and we define Bounded-Outcome Strategy Logic which has a bounded quantifier on paths. We supply a general technique, based on the study of automata with counters, that solves the model-checking problems for both these logics.
Cite as

Nathanaël Fijalkow, Bastien Maubert, Aniello Murano, and Sasha Rubin. Quantifying Bounds in Strategy Logic. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 23:1-23:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.CSL.2018.23,
  author =	{Fijalkow, Nathana\"{e}l and Maubert, Bastien and Murano, Aniello and Rubin, Sasha},
  title =	{{Quantifying Bounds in Strategy Logic}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{23:1--23:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.23},
  URN =		{urn:nbn:de:0030-drops-96901},
  doi =		{10.4230/LIPIcs.CSL.2018.23},
  annote =	{Keywords: Prompt LTL, Strategy Logic, Model checking, Automata with counters}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.19
Probabilistic Automata of Bounded Ambiguity

Authors: Nathanaël Fijalkow, Cristian Riveros, and James Worrell

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
Probabilistic automata are a computational model introduced by Michael Rabin, extending nondeterministic finite automata with probabilistic transitions. Despite its simplicity, this model is very expressive and many of the associated algorithmic questions are undecidable. In this work we focus on the emptiness problem, which asks whether a given probabilistic automaton accepts some word with probability higher than a given threshold. We consider a natural and well-studied structural restriction on automata, namely the degree of ambiguity, which is defined as the maximum number of accepting runs over all words. We observe that undecidability of the emptiness problem requires infinite ambiguity and so we focus on the case of finitely ambiguous probabilistic automata. Our main results are to construct efficient algorithms for analysing finitely ambiguous probabilistic automata through a reduction to a multi-objective optimisation problem, called the stochastic path problem. We obtain a polynomial time algorithm for approximating the value of finitely ambiguous probabilistic automata and a quasi-polynomial time algorithm for the emptiness problem for 2-ambiguous probabilistic automata.
Cite as

Nathanaël Fijalkow, Cristian Riveros, and James Worrell. Probabilistic Automata of Bounded Ambiguity. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 19:1-19:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.CONCUR.2017.19,
  author =	{Fijalkow, Nathana\"{e}l and Riveros, Cristian and Worrell, James},
  title =	{{Probabilistic Automata of Bounded Ambiguity}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{19:1--19:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.19},
  URN =		{urn:nbn:de:0030-drops-77716},
  doi =		{10.4230/LIPIcs.CONCUR.2017.19},
  annote =	{Keywords: Probabilistic Automata, Emptiness Problem, Stochastic Path Problem, Multi-Objective Optimisation Problems}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.105
Expressiveness of Probabilistic Modal Logics, Revisited

Authors: Nathanaël Fijalkow, Bartek Klin, and Prakash Panangaden

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
Labelled Markov processes are probabilistic versions of labelled transition systems. In general, the state space of a labelled Markov process may be a continuum. Logical characterizations of probabilistic bisimulation and simulation were given by Desharnais et al. These results hold for systems defined on analytic state spaces and assume that there are countably many labels in the case of bisimulation and finitely many labels in the case of simulation. In this paper, we first revisit these results by giving simpler and more streamlined proofs. In particular, our proof for simulation has the same structure as the one for bisimulation, relying on a new result of a topological nature. This departs from the known proof for this result, which uses domain theory techniques and falls out of a theory of approximation of Labelled Markov processes. Both our proofs assume the presence of countably many labels. We investigate the necessity of this assumption, and show that the logical characterization of bisimulation may fail when there are uncountably many labels. However, with a stronger assumption on the transition functions (continuity instead of just measurability), we can regain the logical characterization result, for arbitrarily many labels. These new results arose from a new game-theoretic way of understanding probabilistic simulation and bisimulation.
Cite as

Nathanaël Fijalkow, Bartek Klin, and Prakash Panangaden. Expressiveness of Probabilistic Modal Logics, Revisited. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 105:1-105:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.ICALP.2017.105,
  author =	{Fijalkow, Nathana\"{e}l and Klin, Bartek and Panangaden, Prakash},
  title =	{{Expressiveness of Probabilistic Modal Logics, Revisited}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{105:1--105:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.105},
  URN =		{urn:nbn:de:0030-drops-73683},
  doi =		{10.4230/LIPIcs.ICALP.2017.105},
  annote =	{Keywords: probabilistic modal logic, probabilistic bisimulation, probabilistic simulation}
}
Document
DOI: 10.4230/LIPIcs.STACS.2017.29
Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem

Authors: Nathanaël Fijalkow, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, and James Worrell

Published in: LIPIcs, Volume 66, 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)

Abstract
The Orbit Problem consists of determining, given a linear transformation A on d-dimensional rationals Q^d, together with vectors x and y, whether the orbit of x under repeated applications of A can ever reach y. This problem was famously shown to be decidable by Kannan and Lipton in the 1980s. In this paper, we are concerned with the problem of synthesising suitable invariants P which are subsets of R^d, i.e., sets that are stable under A and contain x and not y, thereby providing compact and versatile certificates of non-reachability. We show that whether a given instance of the Orbit Problem admits a semialgebraic invariant is decidable, and moreover in positive instances we provide an algorithm to synthesise suitable invariants of polynomial size. It is worth noting that the existence of semilinear invariants, on the other hand, is (to the best of our knowledge) not known to be decidable.
Cite as

Nathanaël Fijalkow, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, and James Worrell. Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 29:1-29:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.STACS.2017.29,
  author =	{Fijalkow, Nathana\"{e}l and Ohlmann, Pierre and Ouaknine, Jo\"{e}l and Pouly, Amaury and Worrell, James},
  title =	{{Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem}},
  booktitle =	{34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)},
  pages =	{29:1--29:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-028-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{66},
  editor =	{Vollmer, Heribert and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2017.29},
  URN =		{urn:nbn:de:0030-drops-70059},
  doi =		{10.4230/LIPIcs.STACS.2017.29},
  annote =	{Keywords: Verification,algebraic computation,Skolem Problem,Orbit Problem,invariants}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.126
The Bridge Between Regular Cost Functions and Omega-Regular Languages

Authors: Thomas Colcombet and Nathanaël Fijalkow

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
In this paper, we exhibit a one-to-one correspondence between omega-regular languages and a subclass of regular cost functions over finite words, called omega-regular like cost functions. This bridge between the two models allows one to readily import classical results such as the last appearance record or the McNaughton-Safra constructions to the realm of regular cost functions. In combination with game theoretic techniques, this also yields a simple description of an optimal procedure of history-determinisation for cost automata, a central result in the theory of regular cost functions.
Cite as

Thomas Colcombet and Nathanaël Fijalkow. The Bridge Between Regular Cost Functions and Omega-Regular Languages. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 126:1-126:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.ICALP.2016.126,
  author =	{Colcombet, Thomas and Fijalkow, Nathana\"{e}l},
  title =	{{The Bridge Between Regular Cost Functions and Omega-Regular Languages}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{126:1--126:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.126},
  URN =		{urn:nbn:de:0030-drops-62619},
  doi =		{10.4230/LIPIcs.ICALP.2016.126},
  annote =	{Keywords: Theory of Regular Cost Functions, Automata with Counters, Costautomata, Quantitative Extensions of Automata, Determinisation of Automata}
}
Document
DOI: 10.4230/LIPIcs.STACS.2016.34
Characterisation of an Algebraic Algorithm for Probabilistic Automata

Authors: Nathanaël Fijalkow

Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

Abstract
We consider the value 1 problem for probabilistic automata over finite words: it asks whether a given probabilistic automaton accepts words with probability arbitrarily close to 1. This problem is known to be undecidable. However, different algorithms have been proposed to partially solve it; it has been recently shown that the Markov Monoid algorithm, based on algebra, is the most correct algorithm so far. The first contribution of this paper is to give a characterisation of the Markov Monoid algorithm. The second contribution is to develop a profinite theory for probabilistic automata, called the prostochastic theory. This new framework gives a topological account of the value 1 problem, which in this context is cast as an emptiness problem. The above characterisation is reformulated using the prostochastic theory, allowing to give a modular proof.
Cite as

Nathanaël Fijalkow. Characterisation of an Algebraic Algorithm for Probabilistic Automata. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 34:1-34:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{fijalkow:LIPIcs.STACS.2016.34,
  author =	{Fijalkow, Nathana\"{e}l},
  title =	{{Characterisation of an Algebraic Algorithm for Probabilistic Automata}},
  booktitle =	{33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
  pages =	{34:1--34:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-001-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{47},
  editor =	{Ollinger, Nicolas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.34},
  URN =		{urn:nbn:de:0030-drops-57355},
  doi =		{10.4230/LIPIcs.STACS.2016.34},
  annote =	{Keywords: Probabilistic Automata, Value 1 Problem, Markov Monoid Algorithm, Algebraic Algorithm, Profinite Theory, Topology in Computer Science}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.379
Playing Safe

Authors: Thomas Colcombet, Nathanael Fijalkow, and Florian Horn

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
We consider two-player games over graphs and give tight bounds on the memory size of strategies ensuring safety conditions. More specifically, we show that the minimal number of memory states of a strategy ensuring a safety condition is given by the size of the maximal antichain of left quotients with respect to language inclusion. This result holds for all safety conditions without any regularity assumptions, and for all (finite or infinite) graphs of finite degree. We give several applications of this general principle. In particular, we characterize the exact memory requirements for the opponent in generalized reachability games, and we prove the existence of positional strategies in games with counters.
Cite as

Thomas Colcombet, Nathanael Fijalkow, and Florian Horn. Playing Safe. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 379-390, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.FSTTCS.2014.379,
  author =	{Colcombet, Thomas and Fijalkow, Nathanael and Horn, Florian},
  title =	{{Playing Safe}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{379--390},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.379},
  URN =		{urn:nbn:de:0030-drops-48571},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.379},
  annote =	{Keywords: Game Theory, Synthesis, Safety Specifications, Program Verification}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2013.299
Emptiness Of Alternating Tree Automata Using Games With Imperfect Information

Authors: Nathanaël Fijalkow, Sophie Pinchinat, and Olivier Serre

Published in: LIPIcs, Volume 24, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)

Abstract
We consider the emptiness problem for alternating tree automata, with two acceptance semantics: classical (all branches are accepted) and qualitative (almost all branches are accepted). For the classical semantics, the usual technique to tackle this problem relies on a Simulation Theorem which constructs an equivalent non-deterministic automaton from the original alternating one, and then checks emptiness by a reduction to a two-player perfect information game. However, for the qualitative semantics, no simulation of alternation by means of non-determinism is known. We give an alternative technique to decide the emptiness problem of alternating tree automata, that does not rely on a Simulation Theorem. Indeed, we directly reduce the emptiness problem to solving an imperfect information two-player parity game. Our new approach can successfully be applied to both semantics, and yields decidability results with optimal complexity; for the qualitative semantics, the key ingredient in the proof is a positionality result for stochastic games played over infinite graphs.
Cite as

Nathanaël Fijalkow, Sophie Pinchinat, and Olivier Serre. Emptiness Of Alternating Tree Automata Using Games With Imperfect Information. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 299-311, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.FSTTCS.2013.299,
  author =	{Fijalkow, Nathana\"{e}l and Pinchinat, Sophie and Serre, Olivier},
  title =	{{Emptiness Of Alternating Tree Automata Using Games With Imperfect Information}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)},
  pages =	{299--311},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-64-4},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{24},
  editor =	{Seth, Anil and Vishnoi, Nisheeth K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.299},
  URN =		{urn:nbn:de:0030-drops-43812},
  doi =		{10.4230/LIPIcs.FSTTCS.2013.299},
  annote =	{Keywords: Alternating Automata, Emptiness checking, Two-player games, Imperfect Information Games}
}
Document
DOI: 10.4230/LIPIcs.CSL.2013.181
Infinite-state games with finitary conditions

Authors: Krishnendu Chatterjee and Nathanaël Fijalkow

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
We study two-player zero-sum games over infinite-state graphs equipped with omega-B and finitary conditions. Our first contribution is about the strategy complexity, i.e the memory required for winning strategies: we prove that over general infinite-state graphs, memoryless strategies are sufficient for finitary Büchi, and finite-memory suffices for finitary parity games. We then study pushdown games with boundedness conditions, with two contributions. First we prove a collapse result for pushdown games with omega-B-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.
Cite as

Krishnendu Chatterjee and Nathanaël Fijalkow. Infinite-state games with finitary conditions. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 181-196, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.CSL.2013.181,
  author =	{Chatterjee, Krishnendu and Fijalkow, Nathana\"{e}l},
  title =	{{Infinite-state games with finitary conditions}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{181--196},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.181},
  URN =		{urn:nbn:de:0030-drops-41970},
  doi =		{10.4230/LIPIcs.CSL.2013.181},
  annote =	{Keywords: Two-player games, Infinite-state systems, Pushdown games, Bounds in omega-regularity, Synthesis}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.124
Cost-Parity and Cost-Streett Games

Authors: Nathanael Fijalkow and Martin Zimmermann

Published in: LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)

Abstract
We consider two-player games played on finite 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 intersection 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.
Cite as

Nathanael Fijalkow and Martin Zimmermann. Cost-Parity and Cost-Streett Games. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 124-135, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.FSTTCS.2012.124,
  author =	{Fijalkow, Nathanael and Zimmermann, Martin},
  title =	{{Cost-Parity and Cost-Streett Games}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{124--135},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.124},
  URN =		{urn:nbn:de:0030-drops-38538},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.124},
  annote =	{Keywords: Parity Games, Streett Games, Costs, Scoring Functions}
}

Fijalkow, Nathanaël

Document
DOI: 10.4230/DagRep.13.9.166
The Futures of Reactive Synthesis (Dagstuhl Seminar 23391)

Authors: Nathanaël Fijalkow, Bernd Finkbeiner, Guillermo A. Pérez, Elizabeth Polgreen, and Rémi Morvan

Published in: Dagstuhl Reports, Volume 13, Issue 9 (2024)

Abstract
The Dagstuhl Seminar 23391 "The Futures of Reactive Synthesis" held in September 2023 was meant to gather neighbouring communities on a joint goal: Reactive Synthesis. We identified five trends: neural-symbolic computation, template-based solving for constraint programming, symbolic algorithms, syntax-guided synthesis, and model learning; and the objective was to discuss the potential futures of the field.
Cite as

Nathanaël Fijalkow, Bernd Finkbeiner, Guillermo A. Pérez, Elizabeth Polgreen, and Rémi Morvan. The Futures of Reactive Synthesis (Dagstuhl Seminar 23391). In Dagstuhl Reports, Volume 13, Issue 9, pp. 166-184, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{fijalkow_et_al:DagRep.13.9.166,
  author =	{Fijalkow, Nathana\"{e}l and Finkbeiner, Bernd and P\'{e}rez, Guillermo A. and Polgreen, Elizabeth and Morvan, R\'{e}mi},
  title =	{{The Futures of Reactive Synthesis (Dagstuhl Seminar 23391)}},
  pages =	{166--184},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{13},
  number =	{9},
  editor =	{Fijalkow, Nathana\"{e}l and Finkbeiner, Bernd and P\'{e}rez, Guillermo A. and Polgreen, Elizabeth and Morvan, R\'{e}mi},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.9.166},
  URN =		{urn:nbn:de:0030-drops-198259},
  doi =		{10.4230/DagRep.13.9.166},
  annote =	{Keywords: program synthesis, program verification, reactive synthesis, temporal synthesis}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2023.118
How to Play Optimally for Regular Objectives?

Authors: Patricia Bouyer, Nathanaël Fijalkow, Mickael Randour, and Pierre Vandenhove

Published in: LIPIcs, Volume 261, 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)

Abstract
This paper studies two-player zero-sum games played on graphs and makes contributions toward the following question: given an objective, how much memory is required to play optimally for that objective? We study regular objectives, where the goal of one of the two players is that eventually the sequence of colors along the play belongs to some regular language of finite words. We obtain different characterizations of the chromatic memory requirements for such objectives for both players, from which we derive complexity-theoretic statements: deciding whether there exist small memory structures sufficient to play optimally is NP-complete for both players. Some of our characterization results apply to a more general class of objectives: topologically closed and topologically open sets.
Cite as

Patricia Bouyer, Nathanaël Fijalkow, Mickael Randour, and Pierre Vandenhove. How to Play Optimally for Regular Objectives?. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 118:1-118:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.ICALP.2023.118,
  author =	{Bouyer, Patricia and Fijalkow, Nathana\"{e}l and Randour, Mickael and Vandenhove, Pierre},
  title =	{{How to Play Optimally for Regular Objectives?}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{118:1--118:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-278-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{261},
  editor =	{Etessami, Kousha and Feige, Uriel and Puppis, Gabriele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2023.118},
  URN =		{urn:nbn:de:0030-drops-181700},
  doi =		{10.4230/LIPIcs.ICALP.2023.118},
  annote =	{Keywords: two-player games on graphs, strategy complexity, regular languages, finite-memory strategies, NP-completeness}
}
Document
DOI: 10.4230/LIPIcs.CP.2021.43
Statistical Comparison of Algorithm Performance Through Instance Selection

Authors: Théo Matricon, Marie Anastacio, Nathanaël Fijalkow, Laurent Simon, and Holger H. Hoos

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract
Empirical performance evaluations, in competitions and scientific publications, play a major role in improving the state of the art in solving many automated reasoning problems, including SAT, CSP and Bayesian network structure learning (BNSL). To empirically demonstrate the merit of a new solver usually requires extensive experiments, with computational costs of CPU years. This not only makes it difficult for researchers with limited access to computational resources to test their ideas and publish their work, but also consumes large amounts of energy. We propose an approach for comparing the performance of two algorithms: by performing runs on carefully chosen instances, we obtain a probabilistic statement on which algorithm performs best, trading off between the computational cost of running algorithms and the confidence in the result. We describe a set of methods for this purpose and evaluate their efficacy on diverse datasets from SAT, CSP and BNSL. On all these datasets, most of our approaches were able to choose the correct algorithm with about 95% accuracy, while using less than a third of the CPU time required for a full comparison; the best methods reach this level of accuracy within less than 15% of the CPU time for a full comparison.
Cite as

Théo Matricon, Marie Anastacio, Nathanaël Fijalkow, Laurent Simon, and Holger H. Hoos. Statistical Comparison of Algorithm Performance Through Instance Selection. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 43:1-43:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{matricon_et_al:LIPIcs.CP.2021.43,
  author =	{Matricon, Th\'{e}o and Anastacio, Marie and Fijalkow, Nathana\"{e}l and Simon, Laurent and Hoos, Holger H.},
  title =	{{Statistical Comparison of Algorithm Performance Through Instance Selection}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{43:1--43:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.43},
  URN =		{urn:nbn:de:0030-drops-153346},
  doi =		{10.4230/LIPIcs.CP.2021.43},
  annote =	{Keywords: Performance assessment, early stopping, automated reasoning solvers}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
DOI: 10.4230/LIPIcs.ICALP.2021.123
Optimal Transformations of Games and Automata Using Muller Conditions

Authors: Antonio Casares, Thomas Colcombet, and Nathanaël Fijalkow

Published in: LIPIcs, Volume 198, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)

Abstract
We consider the following question: given an automaton or a game with a Muller condition, how can we efficiently construct an equivalent one with a parity condition? There are several examples of such transformations in the literature, including in the determinisation of Büchi automata. We define a new transformation called the alternating cycle decomposition, inspired and extending Zielonka’s construction. Our transformation operates on transition systems, encompassing both automata and games, and preserves semantic properties through the existence of a locally bijective morphism. We show a strong optimality result: the obtained parity transition system is minimal both in number of states and number of priorities with respect to locally bijective morphisms. We give two applications: the first is related to the determinisation of Büchi automata, and the second is to give crisp characterisations on the possibility of relabelling automata with different acceptance conditions.
Cite as

Antonio Casares, Thomas Colcombet, and Nathanaël Fijalkow. Optimal Transformations of Games and Automata Using Muller Conditions. In 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 198, pp. 123:1-123:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{casares_et_al:LIPIcs.ICALP.2021.123,
  author =	{Casares, Antonio and Colcombet, Thomas and Fijalkow, Nathana\"{e}l},
  title =	{{Optimal Transformations of Games and Automata Using Muller Conditions}},
  booktitle =	{48th International Colloquium on Automata, Languages, and Programming (ICALP 2021)},
  pages =	{123:1--123:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-195-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{198},
  editor =	{Bansal, Nikhil and Merelli, Emanuela and Worrell, James},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2021.123},
  URN =		{urn:nbn:de:0030-drops-141928},
  doi =		{10.4230/LIPIcs.ICALP.2021.123},
  annote =	{Keywords: Automata over infinite words, Omega regular languages, Determinisation of automata}
}
Document
DOI: 10.4230/LIPIcs.MFCS.2020.34
Value Iteration Using Universal Graphs and the Complexity of Mean Payoff Games

Authors: Nathanaël Fijalkow, Paweł Gawrychowski, and Pierre Ohlmann

Published in: LIPIcs, Volume 170, 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)

Abstract
We study the computational complexity of solving mean payoff games. This class of games can be seen as an extension of parity games, and they have similar complexity status: in both cases solving them is in NP ∩ coNP and not known to be in P. In a breakthrough result Calude, Jain, Khoussainov, Li, and Stephan constructed in 2017 a quasipolynomial time algorithm for solving parity games, which was quickly followed by a few other algorithms with the same complexity. Our objective is to investigate how these techniques can be extended to mean payoff games. The starting point is the combinatorial notion of universal trees: all quasipolynomial time algorithms for parity games have been shown to exploit universal trees. Universal graphs extend universal trees to arbitrary (positionally determined) objectives. We show that they yield a family of value iteration algorithms for solving mean payoff games which includes the value iteration algorithm due to Brim, Chaloupka, Doyen, Gentilini, and Raskin. The contribution of this paper is to prove tight bounds on the complexity of algorithms for mean payoff games using universal graphs. We consider two parameters: the largest weight N in absolute value and the number k of weights. The dependence in N in the existing value iteration algorithm is linear, we show that this can be improved to N^{1 - 1/n} and obtain a matching lower bound. However, we show that we cannot break the linear dependence in the exponent in the number k of weights implying that universal graphs do not yield a quasipolynomial time algorithm for solving mean payoff games.
Cite as

Nathanaël Fijalkow, Paweł Gawrychowski, and Pierre Ohlmann. Value Iteration Using Universal Graphs and the Complexity of Mean Payoff Games. In 45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 170, pp. 34:1-34:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.MFCS.2020.34,
  author =	{Fijalkow, Nathana\"{e}l and Gawrychowski, Pawe{\l} and Ohlmann, Pierre},
  title =	{{Value Iteration Using Universal Graphs and the Complexity of Mean Payoff Games}},
  booktitle =	{45th International Symposium on Mathematical Foundations of Computer Science (MFCS 2020)},
  pages =	{34:1--34:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-159-7},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{170},
  editor =	{Esparza, Javier and Kr\'{a}l', Daniel},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.MFCS.2020.34},
  URN =		{urn:nbn:de:0030-drops-127011},
  doi =		{10.4230/LIPIcs.MFCS.2020.34},
  annote =	{Keywords: Mean payoff games, Universal graphs, Value iteration}
}
Document
DOI: 10.4230/LIPIcs.STACS.2020.24
Lower Bounds for Arithmetic Circuits via the Hankel Matrix

Authors: Nathanaël Fijalkow, Guillaume Lagarde, Pierre Ohlmann, and Olivier Serre

Published in: LIPIcs, Volume 154, 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)

Abstract
We study the complexity of representing polynomials by arithmetic circuits in both the commutative and the non-commutative settings. To analyse circuits we count their number of parse trees, which describe the non-associative computations realised by the circuit. In the non-commutative setting a circuit computing a polynomial of degree d has at most 2^{O(d)} parse trees. Previous superpolynomial lower bounds were known for circuits with up to 2^{d^{1/3-ε}} parse trees, for any ε > 0. Our main result is to reduce the gap by showing a superpolynomial lower bound for circuits with just a small defect in the exponent for the total number of parse trees, that is 2^{d^{1 - ε}}, for any ε > 0. In the commutative setting a circuit computing a polynomial of degree d has at most 2^{O(d log d)} parse trees. We show a superpolynomial lower bound for circuits with up to 2^{d^{1/3 - ε}} parse trees, for any ε > 0. When d is polylogarithmic in n, we push this further to up to 2^{d^{1 - ε}} parse trees. While these two main results hold in the associative setting, our approach goes through a precise understanding of the more restricted setting where multiplication is not associative, meaning that we distinguish the polynomials (xy)z and x(yz). Our first and main conceptual result is a characterization result: we show that the size of the smallest circuit computing a given non-associative polynomial is exactly the rank of a matrix constructed from the polynomial and called the Hankel matrix. This result applies to the class of all circuits in both commutative and non-commutative settings, and can be seen as an extension of the seminal result of Nisan giving a similar characterization for non-commutative algebraic branching programs. Our key technical contribution is to provide generic lower bound theorems based on analyzing and decomposing the Hankel matrix, from which we derive the results mentioned above. The study of the Hankel matrix also provides a unifying approach for proving lower bounds for polynomials in the (classical) associative setting. We demonstrate this by giving alternative proofs of recent lower bounds as corollaries of our generic lower bound results.
Cite as

Nathanaël Fijalkow, Guillaume Lagarde, Pierre Ohlmann, and Olivier Serre. Lower Bounds for Arithmetic Circuits via the Hankel Matrix. In 37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 154, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.STACS.2020.24,
  author =	{Fijalkow, Nathana\"{e}l and Lagarde, Guillaume and Ohlmann, Pierre and Serre, Olivier},
  title =	{{Lower Bounds for Arithmetic Circuits via the Hankel Matrix}},
  booktitle =	{37th International Symposium on Theoretical Aspects of Computer Science (STACS 2020)},
  pages =	{24:1--24:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-140-5},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{154},
  editor =	{Paul, Christophe and Bl\"{a}ser, Markus},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2020.24},
  URN =		{urn:nbn:de:0030-drops-118859},
  doi =		{10.4230/LIPIcs.STACS.2020.24},
  annote =	{Keywords: Arithmetic Circuit Complexity, Lower Bounds, Parse Trees, Hankel Matrix}
}
Document
DOI: 10.4230/LIPIcs.CSL.2020.9
A Robust Class of Linear Recurrence Sequences

Authors: Corentin Barloy, Nathanaël Fijalkow, Nathan Lhote, and Filip Mazowiecki

Published in: LIPIcs, Volume 152, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020)

Abstract
We introduce a subclass of linear recurrence sequences which we call poly-rational sequences because they are denoted by rational expressions closed under sum and product. We show that this class is robust by giving several characterisations: polynomially ambiguous weighted automata, copyless cost-register automata, rational formal series, and linear recurrence sequences whose eigenvalues are roots of rational numbers.
Cite as

Corentin Barloy, Nathanaël Fijalkow, Nathan Lhote, and Filip Mazowiecki. A Robust Class of Linear Recurrence Sequences. In 28th EACSL Annual Conference on Computer Science Logic (CSL 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 152, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{barloy_et_al:LIPIcs.CSL.2020.9,
  author =	{Barloy, Corentin and Fijalkow, Nathana\"{e}l and Lhote, Nathan and Mazowiecki, Filip},
  title =	{{A Robust Class of Linear Recurrence Sequences}},
  booktitle =	{28th EACSL Annual Conference on Computer Science Logic (CSL 2020)},
  pages =	{9:1--9:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-132-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{152},
  editor =	{Fern\'{a}ndez, Maribel and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.9},
  URN =		{urn:nbn:de:0030-drops-116521},
  doi =		{10.4230/LIPIcs.CSL.2020.9},
  annote =	{Keywords: linear recurrence sequences, weighted automata, cost-register automata}
}
Document
DOI: 10.4230/LIPIcs.CSL.2018.23
Quantifying Bounds in Strategy Logic

Authors: Nathanaël Fijalkow, Bastien Maubert, Aniello Murano, and Sasha Rubin

Published in: LIPIcs, Volume 119, 27th EACSL Annual Conference on Computer Science Logic (CSL 2018)

Abstract
Program synthesis constructs programs from specifications in an automated way. Strategy Logic (SL) is a powerful and versatile specification language whose goal is to give theoretical foundations for program synthesis in a multi-agent setting. One limitation of Strategy Logic is that it is purely qualitative. For instance it cannot specify quantitative properties of executions such as "every request is quickly granted", or quantitative properties of trees such as "most executions of the system terminate". In this work, we extend Strategy Logic to include quantitative aspects in a way that can express bounds on "how quickly" and "how many". We define Prompt Strategy Logic, which encompasses Prompt LTL (itself an extension of LTL with a prompt eventuality temporal operator), and we define Bounded-Outcome Strategy Logic which has a bounded quantifier on paths. We supply a general technique, based on the study of automata with counters, that solves the model-checking problems for both these logics.
Cite as

Nathanaël Fijalkow, Bastien Maubert, Aniello Murano, and Sasha Rubin. Quantifying Bounds in Strategy Logic. In 27th EACSL Annual Conference on Computer Science Logic (CSL 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 119, pp. 23:1-23:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.CSL.2018.23,
  author =	{Fijalkow, Nathana\"{e}l and Maubert, Bastien and Murano, Aniello and Rubin, Sasha},
  title =	{{Quantifying Bounds in Strategy Logic}},
  booktitle =	{27th EACSL Annual Conference on Computer Science Logic (CSL 2018)},
  pages =	{23:1--23:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-088-0},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{119},
  editor =	{Ghica, Dan R. and Jung, Achim},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2018.23},
  URN =		{urn:nbn:de:0030-drops-96901},
  doi =		{10.4230/LIPIcs.CSL.2018.23},
  annote =	{Keywords: Prompt LTL, Strategy Logic, Model checking, Automata with counters}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.19
Probabilistic Automata of Bounded Ambiguity

Authors: Nathanaël Fijalkow, Cristian Riveros, and James Worrell

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
Probabilistic automata are a computational model introduced by Michael Rabin, extending nondeterministic finite automata with probabilistic transitions. Despite its simplicity, this model is very expressive and many of the associated algorithmic questions are undecidable. In this work we focus on the emptiness problem, which asks whether a given probabilistic automaton accepts some word with probability higher than a given threshold. We consider a natural and well-studied structural restriction on automata, namely the degree of ambiguity, which is defined as the maximum number of accepting runs over all words. We observe that undecidability of the emptiness problem requires infinite ambiguity and so we focus on the case of finitely ambiguous probabilistic automata. Our main results are to construct efficient algorithms for analysing finitely ambiguous probabilistic automata through a reduction to a multi-objective optimisation problem, called the stochastic path problem. We obtain a polynomial time algorithm for approximating the value of finitely ambiguous probabilistic automata and a quasi-polynomial time algorithm for the emptiness problem for 2-ambiguous probabilistic automata.
Cite as

Nathanaël Fijalkow, Cristian Riveros, and James Worrell. Probabilistic Automata of Bounded Ambiguity. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 19:1-19:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.CONCUR.2017.19,
  author =	{Fijalkow, Nathana\"{e}l and Riveros, Cristian and Worrell, James},
  title =	{{Probabilistic Automata of Bounded Ambiguity}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{19:1--19:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.19},
  URN =		{urn:nbn:de:0030-drops-77716},
  doi =		{10.4230/LIPIcs.CONCUR.2017.19},
  annote =	{Keywords: Probabilistic Automata, Emptiness Problem, Stochastic Path Problem, Multi-Objective Optimisation Problems}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.105
Expressiveness of Probabilistic Modal Logics, Revisited

Authors: Nathanaël Fijalkow, Bartek Klin, and Prakash Panangaden

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
Labelled Markov processes are probabilistic versions of labelled transition systems. In general, the state space of a labelled Markov process may be a continuum. Logical characterizations of probabilistic bisimulation and simulation were given by Desharnais et al. These results hold for systems defined on analytic state spaces and assume that there are countably many labels in the case of bisimulation and finitely many labels in the case of simulation. In this paper, we first revisit these results by giving simpler and more streamlined proofs. In particular, our proof for simulation has the same structure as the one for bisimulation, relying on a new result of a topological nature. This departs from the known proof for this result, which uses domain theory techniques and falls out of a theory of approximation of Labelled Markov processes. Both our proofs assume the presence of countably many labels. We investigate the necessity of this assumption, and show that the logical characterization of bisimulation may fail when there are uncountably many labels. However, with a stronger assumption on the transition functions (continuity instead of just measurability), we can regain the logical characterization result, for arbitrarily many labels. These new results arose from a new game-theoretic way of understanding probabilistic simulation and bisimulation.
Cite as

Nathanaël Fijalkow, Bartek Klin, and Prakash Panangaden. Expressiveness of Probabilistic Modal Logics, Revisited. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 105:1-105:12, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.ICALP.2017.105,
  author =	{Fijalkow, Nathana\"{e}l and Klin, Bartek and Panangaden, Prakash},
  title =	{{Expressiveness of Probabilistic Modal Logics, Revisited}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{105:1--105:12},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.105},
  URN =		{urn:nbn:de:0030-drops-73683},
  doi =		{10.4230/LIPIcs.ICALP.2017.105},
  annote =	{Keywords: probabilistic modal logic, probabilistic bisimulation, probabilistic simulation}
}
Document
DOI: 10.4230/LIPIcs.STACS.2017.29
Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem

Authors: Nathanaël Fijalkow, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, and James Worrell

Published in: LIPIcs, Volume 66, 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)

Abstract
The Orbit Problem consists of determining, given a linear transformation A on d-dimensional rationals Q^d, together with vectors x and y, whether the orbit of x under repeated applications of A can ever reach y. This problem was famously shown to be decidable by Kannan and Lipton in the 1980s. In this paper, we are concerned with the problem of synthesising suitable invariants P which are subsets of R^d, i.e., sets that are stable under A and contain x and not y, thereby providing compact and versatile certificates of non-reachability. We show that whether a given instance of the Orbit Problem admits a semialgebraic invariant is decidable, and moreover in positive instances we provide an algorithm to synthesise suitable invariants of polynomial size. It is worth noting that the existence of semilinear invariants, on the other hand, is (to the best of our knowledge) not known to be decidable.
Cite as

Nathanaël Fijalkow, Pierre Ohlmann, Joël Ouaknine, Amaury Pouly, and James Worrell. Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem. In 34th Symposium on Theoretical Aspects of Computer Science (STACS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 66, pp. 29:1-29:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.STACS.2017.29,
  author =	{Fijalkow, Nathana\"{e}l and Ohlmann, Pierre and Ouaknine, Jo\"{e}l and Pouly, Amaury and Worrell, James},
  title =	{{Semialgebraic Invariant Synthesis for the Kannan-Lipton Orbit Problem}},
  booktitle =	{34th Symposium on Theoretical Aspects of Computer Science (STACS 2017)},
  pages =	{29:1--29:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-028-6},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{66},
  editor =	{Vollmer, Heribert and Vall\'{e}e, Brigitte},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2017.29},
  URN =		{urn:nbn:de:0030-drops-70059},
  doi =		{10.4230/LIPIcs.STACS.2017.29},
  annote =	{Keywords: Verification,algebraic computation,Skolem Problem,Orbit Problem,invariants}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2016.126
The Bridge Between Regular Cost Functions and Omega-Regular Languages

Authors: Thomas Colcombet and Nathanaël Fijalkow

Published in: LIPIcs, Volume 55, 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)

Abstract
In this paper, we exhibit a one-to-one correspondence between omega-regular languages and a subclass of regular cost functions over finite words, called omega-regular like cost functions. This bridge between the two models allows one to readily import classical results such as the last appearance record or the McNaughton-Safra constructions to the realm of regular cost functions. In combination with game theoretic techniques, this also yields a simple description of an optimal procedure of history-determinisation for cost automata, a central result in the theory of regular cost functions.
Cite as

Thomas Colcombet and Nathanaël Fijalkow. The Bridge Between Regular Cost Functions and Omega-Regular Languages. In 43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 55, pp. 126:1-126:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.ICALP.2016.126,
  author =	{Colcombet, Thomas and Fijalkow, Nathana\"{e}l},
  title =	{{The Bridge Between Regular Cost Functions and Omega-Regular Languages}},
  booktitle =	{43rd International Colloquium on Automata, Languages, and Programming (ICALP 2016)},
  pages =	{126:1--126:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-013-2},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{55},
  editor =	{Chatzigiannakis, Ioannis and Mitzenmacher, Michael and Rabani, Yuval and Sangiorgi, Davide},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2016.126},
  URN =		{urn:nbn:de:0030-drops-62619},
  doi =		{10.4230/LIPIcs.ICALP.2016.126},
  annote =	{Keywords: Theory of Regular Cost Functions, Automata with Counters, Costautomata, Quantitative Extensions of Automata, Determinisation of Automata}
}
Document
DOI: 10.4230/LIPIcs.STACS.2016.34
Characterisation of an Algebraic Algorithm for Probabilistic Automata

Authors: Nathanaël Fijalkow

Published in: LIPIcs, Volume 47, 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)

Abstract
We consider the value 1 problem for probabilistic automata over finite words: it asks whether a given probabilistic automaton accepts words with probability arbitrarily close to 1. This problem is known to be undecidable. However, different algorithms have been proposed to partially solve it; it has been recently shown that the Markov Monoid algorithm, based on algebra, is the most correct algorithm so far. The first contribution of this paper is to give a characterisation of the Markov Monoid algorithm. The second contribution is to develop a profinite theory for probabilistic automata, called the prostochastic theory. This new framework gives a topological account of the value 1 problem, which in this context is cast as an emptiness problem. The above characterisation is reformulated using the prostochastic theory, allowing to give a modular proof.
Cite as

Nathanaël Fijalkow. Characterisation of an Algebraic Algorithm for Probabilistic Automata. In 33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 47, pp. 34:1-34:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{fijalkow:LIPIcs.STACS.2016.34,
  author =	{Fijalkow, Nathana\"{e}l},
  title =	{{Characterisation of an Algebraic Algorithm for Probabilistic Automata}},
  booktitle =	{33rd Symposium on Theoretical Aspects of Computer Science (STACS 2016)},
  pages =	{34:1--34:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-001-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{47},
  editor =	{Ollinger, Nicolas and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2016.34},
  URN =		{urn:nbn:de:0030-drops-57355},
  doi =		{10.4230/LIPIcs.STACS.2016.34},
  annote =	{Keywords: Probabilistic Automata, Value 1 Problem, Markov Monoid Algorithm, Algebraic Algorithm, Profinite Theory, Topology in Computer Science}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2014.379
Playing Safe

Authors: Thomas Colcombet, Nathanael Fijalkow, and Florian Horn

Published in: LIPIcs, Volume 29, 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)

Abstract
We consider two-player games over graphs and give tight bounds on the memory size of strategies ensuring safety conditions. More specifically, we show that the minimal number of memory states of a strategy ensuring a safety condition is given by the size of the maximal antichain of left quotients with respect to language inclusion. This result holds for all safety conditions without any regularity assumptions, and for all (finite or infinite) graphs of finite degree. We give several applications of this general principle. In particular, we characterize the exact memory requirements for the opponent in generalized reachability games, and we prove the existence of positional strategies in games with counters.
Cite as

Thomas Colcombet, Nathanael Fijalkow, and Florian Horn. Playing Safe. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 379-390, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@InProceedings{colcombet_et_al:LIPIcs.FSTTCS.2014.379,
  author =	{Colcombet, Thomas and Fijalkow, Nathanael and Horn, Florian},
  title =	{{Playing Safe}},
  booktitle =	{34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)},
  pages =	{379--390},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-77-4},
  ISSN =	{1868-8969},
  year =	{2014},
  volume =	{29},
  editor =	{Raman, Venkatesh and Suresh, S. P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2014.379},
  URN =		{urn:nbn:de:0030-drops-48571},
  doi =		{10.4230/LIPIcs.FSTTCS.2014.379},
  annote =	{Keywords: Game Theory, Synthesis, Safety Specifications, Program Verification}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2013.299
Emptiness Of Alternating Tree Automata Using Games With Imperfect Information

Authors: Nathanaël Fijalkow, Sophie Pinchinat, and Olivier Serre

Published in: LIPIcs, Volume 24, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)

Abstract
We consider the emptiness problem for alternating tree automata, with two acceptance semantics: classical (all branches are accepted) and qualitative (almost all branches are accepted). For the classical semantics, the usual technique to tackle this problem relies on a Simulation Theorem which constructs an equivalent non-deterministic automaton from the original alternating one, and then checks emptiness by a reduction to a two-player perfect information game. However, for the qualitative semantics, no simulation of alternation by means of non-determinism is known. We give an alternative technique to decide the emptiness problem of alternating tree automata, that does not rely on a Simulation Theorem. Indeed, we directly reduce the emptiness problem to solving an imperfect information two-player parity game. Our new approach can successfully be applied to both semantics, and yields decidability results with optimal complexity; for the qualitative semantics, the key ingredient in the proof is a positionality result for stochastic games played over infinite graphs.
Cite as

Nathanaël Fijalkow, Sophie Pinchinat, and Olivier Serre. Emptiness Of Alternating Tree Automata Using Games With Imperfect Information. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 24, pp. 299-311, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.FSTTCS.2013.299,
  author =	{Fijalkow, Nathana\"{e}l and Pinchinat, Sophie and Serre, Olivier},
  title =	{{Emptiness Of Alternating Tree Automata Using Games With Imperfect Information}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2013)},
  pages =	{299--311},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-64-4},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{24},
  editor =	{Seth, Anil and Vishnoi, Nisheeth K.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2013.299},
  URN =		{urn:nbn:de:0030-drops-43812},
  doi =		{10.4230/LIPIcs.FSTTCS.2013.299},
  annote =	{Keywords: Alternating Automata, Emptiness checking, Two-player games, Imperfect Information Games}
}
Document
DOI: 10.4230/LIPIcs.CSL.2013.181
Infinite-state games with finitary conditions

Authors: Krishnendu Chatterjee and Nathanaël Fijalkow

Published in: LIPIcs, Volume 23, Computer Science Logic 2013 (CSL 2013)

Abstract
We study two-player zero-sum games over infinite-state graphs equipped with omega-B and finitary conditions. Our first contribution is about the strategy complexity, i.e the memory required for winning strategies: we prove that over general infinite-state graphs, memoryless strategies are sufficient for finitary Büchi, and finite-memory suffices for finitary parity games. We then study pushdown games with boundedness conditions, with two contributions. First we prove a collapse result for pushdown games with omega-B-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.
Cite as

Krishnendu Chatterjee and Nathanaël Fijalkow. Infinite-state games with finitary conditions. In Computer Science Logic 2013 (CSL 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 23, pp. 181-196, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@InProceedings{chatterjee_et_al:LIPIcs.CSL.2013.181,
  author =	{Chatterjee, Krishnendu and Fijalkow, Nathana\"{e}l},
  title =	{{Infinite-state games with finitary conditions}},
  booktitle =	{Computer Science Logic 2013 (CSL 2013)},
  pages =	{181--196},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-60-6},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{23},
  editor =	{Ronchi Della Rocca, Simona},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2013.181},
  URN =		{urn:nbn:de:0030-drops-41970},
  doi =		{10.4230/LIPIcs.CSL.2013.181},
  annote =	{Keywords: Two-player games, Infinite-state systems, Pushdown games, Bounds in omega-regularity, Synthesis}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.124
Cost-Parity and Cost-Streett Games

Authors: Nathanael Fijalkow and Martin Zimmermann

Published in: LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)

Abstract
We consider two-player games played on finite 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 intersection 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.
Cite as

Nathanael Fijalkow and Martin Zimmermann. Cost-Parity and Cost-Streett Games. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 124-135, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{fijalkow_et_al:LIPIcs.FSTTCS.2012.124,
  author =	{Fijalkow, Nathanael and Zimmermann, Martin},
  title =	{{Cost-Parity and Cost-Streett Games}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{124--135},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.124},
  URN =		{urn:nbn:de:0030-drops-38538},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.124},
  annote =	{Keywords: Parity Games, Streett Games, Costs, Scoring Functions}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact