10 Search Results for "Ohlmann, Pierre"


Document
Track B: Automata, Logic, Semantics, and Theory of Programming
Characterising Memory in Infinite Games

Authors: Antonio Casares and Pierre Ohlmann

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


Abstract
This paper is concerned with games of infinite duration played over potentially infinite graphs. Recently, Ohlmann (TheoretiCS 2023) presented a characterisation of objectives admitting optimal positional strategies, by means of universal graphs: an objective is positional if and only if it admits well-ordered monotone universal graphs. We extend Ohlmann’s characterisation to encompass (finite or infinite) memory upper bounds. We prove that objectives admitting optimal strategies with ε-memory less than m (a memory that cannot be updated when reading an ε-edge) are exactly those which admit well-founded monotone universal graphs whose antichains have size bounded by m. We also give a characterisation of chromatic memory by means of appropriate universal structures. Our results apply to finite as well as infinite memory bounds (for instance, to objectives with finite but unbounded memory, or with countable memory strategies). We illustrate the applicability of our framework by carrying out a few case studies, we provide examples witnessing limitations of our approach, and we discuss general closure properties which follow from our results.

Cite as

Antonio Casares and Pierre Ohlmann. Characterising Memory in Infinite Games. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 122:1-122:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{casares_et_al:LIPIcs.ICALP.2023.122,
  author =	{Casares, Antonio and Ohlmann, Pierre},
  title =	{{Characterising Memory in Infinite Games}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{122:1--122: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.122},
  URN =		{urn:nbn:de:0030-drops-181740},
  doi =		{10.4230/LIPIcs.ICALP.2023.122},
  annote =	{Keywords: Infinite duration games, Memory, Universal graphs}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
Flipper Games for Monadically Stable Graph Classes

Authors: Jakub Gajarský, Nikolas Mählmann, Rose McCarty, Pierre Ohlmann, Michał Pilipczuk, Wojciech Przybyszewski, Sebastian Siebertz, Marek Sokołowski, and Szymon Toruńczyk

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


Abstract
A class of graphs C is monadically stable if for every unary expansion Ĉ of C, one cannot encode - using first-order transductions - arbitrarily long linear orders in graphs from C. It is known that nowhere dense graph classes are monadically stable; these include classes of bounded maximum degree and classes that exclude a fixed topological minor. On the other hand, monadic stability is a property expressed in purely model-theoretic terms that is also suited for capturing structure in dense graphs. In this work we provide a characterization of monadic stability in terms of the Flipper game: a game on a graph played by Flipper, who in each round can complement the edge relation between any pair of vertex subsets, and Localizer, who in each round is forced to restrict the game to a ball of bounded radius. This is an analog of the Splitter game, which characterizes nowhere dense classes of graphs (Grohe, Kreutzer, and Siebertz, J. ACM '17). We give two different proofs of our main result. The first proof is based on tools borrowed from model theory, and it exposes an additional property of monadically stable graph classes that is close in spirit to definability of types. Also, as a byproduct, we show that monadic stability for graph classes coincides with monadic stability of existential formulas with two free variables, and we provide another combinatorial characterization of monadic stability via forbidden patterns. The second proof relies on the recently introduced notion of flip-flatness (Dreier, Mählmann, Siebertz, and Toruńczyk, arXiv 2206.13765) and provides an efficient algorithm to compute Flipper’s moves in a winning strategy.

Cite as

Jakub Gajarský, Nikolas Mählmann, Rose McCarty, Pierre Ohlmann, Michał Pilipczuk, Wojciech Przybyszewski, Sebastian Siebertz, Marek Sokołowski, and Szymon Toruńczyk. Flipper Games for Monadically Stable Graph Classes. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 128:1-128:16, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{gajarsky_et_al:LIPIcs.ICALP.2023.128,
  author =	{Gajarsk\'{y}, Jakub and M\"{a}hlmann, Nikolas and McCarty, Rose and Ohlmann, Pierre and Pilipczuk, Micha{\l} and Przybyszewski, Wojciech and Siebertz, Sebastian and Soko{\l}owski, Marek and Toru\'{n}czyk, Szymon},
  title =	{{Flipper Games for Monadically Stable Graph Classes}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{128:1--128:16},
  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.128},
  URN =		{urn:nbn:de:0030-drops-181804},
  doi =		{10.4230/LIPIcs.ICALP.2023.128},
  annote =	{Keywords: Stability theory, structural graph theory, games}
}
Document
Track B: Automata, Logic, Semantics, and Theory of Programming
Canonical Decompositions in Monadically Stable and Bounded Shrubdepth Graph Classes

Authors: Pierre Ohlmann, Michał Pilipczuk, Wojciech Przybyszewski, and Szymon Toruńczyk

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


Abstract
We use model-theoretic tools originating from stability theory to derive a result we call the Finitary Substitute Lemma, which intuitively says the following. Suppose we work in a stable graph class 𝒞, and using a first-order formula φ with parameters we are able to define, in every graph G ∈ 𝒞, a relation R that satisfies some hereditary first-order assertion ψ. Then we are able to find a first-order formula φ' that has the same property, but additionally is finitary: there is finite bound k ∈ ℕ such that in every graph G ∈ 𝒞, different choices of parameters give only at most k different relations R that can be defined using φ'. We use the Finitary Substitute Lemma to derive two corollaries about the existence of certain canonical decompositions in classes of well-structured graphs. - We prove that in the Splitter game, which characterizes nowhere dense graph classes, and in the Flipper game, which characterizes monadically stable graph classes, there is a winning strategy for Splitter, respectively Flipper, that can be defined in first-order logic from the game history. Thus, the strategy is canonical. - We show that for any fixed graph class 𝒞 of bounded shrubdepth, there is an 𝒪(n²)-time algorithm that given an n-vertex graph G ∈ 𝒞, computes in an isomorphism-invariant way a structure H of bounded treedepth in which G can be interpreted. A corollary of this result is an 𝒪(n²)-time isomorphism test and canonization algorithm for any fixed class of bounded shrubdepth.

Cite as

Pierre Ohlmann, Michał Pilipczuk, Wojciech Przybyszewski, and Szymon Toruńczyk. Canonical Decompositions in Monadically Stable and Bounded Shrubdepth Graph Classes. In 50th International Colloquium on Automata, Languages, and Programming (ICALP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 261, pp. 135:1-135:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{ohlmann_et_al:LIPIcs.ICALP.2023.135,
  author =	{Ohlmann, Pierre and Pilipczuk, Micha{\l} and Przybyszewski, Wojciech and Toru\'{n}czyk, Szymon},
  title =	{{Canonical Decompositions in Monadically Stable and Bounded Shrubdepth Graph Classes}},
  booktitle =	{50th International Colloquium on Automata, Languages, and Programming (ICALP 2023)},
  pages =	{135:1--135:17},
  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.135},
  URN =		{urn:nbn:de:0030-drops-181874},
  doi =		{10.4230/LIPIcs.ICALP.2023.135},
  annote =	{Keywords: Model Theory, Stability Theory, Shrubdepth, Nowhere Dense, Monadically Stable}
}
Document
A Technique to Speed up Symmetric Attractor-Based Algorithms for Parity Games

Authors: K. S. Thejaswini, Pierre Ohlmann, and Marcin Jurdziński

Published in: LIPIcs, Volume 250, 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)


Abstract
The classic McNaughton-Zielonka algorithm for solving parity games has excellent performance in practice, but its worst-case asymptotic complexity is worse than that of the state-of-the-art algorithms. This work pinpoints the mechanism that is responsible for this relative underperformance and proposes a new technique that eliminates it. The culprit is the wasteful manner in which the results obtained from recursive calls are indiscriminately discarded by the algorithm whenever subgames on which the algorithm is run change. Our new technique is based on firstly enhancing the algorithm to compute attractor decompositions of subgames instead of just winning strategies on them, and then on making it carefully use attractor decompositions computed in prior recursive calls to reduce the size of subgames on which further recursive calls are made. We illustrate the new technique on the classic example of the recursive McNaughton-Zielonka algorithm, but it can be applied to other symmetric attractor-based algorithms that were inspired by it, such as the quasi-polynomial versions of the McNaughton-Zielonka algorithm based on universal trees.

Cite as

K. S. Thejaswini, Pierre Ohlmann, and Marcin Jurdziński. A Technique to Speed up Symmetric Attractor-Based Algorithms for Parity Games. In 42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 250, pp. 44:1-44:20, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{thejaswini_et_al:LIPIcs.FSTTCS.2022.44,
  author =	{Thejaswini, K. S. and Ohlmann, Pierre and Jurdzi\'{n}ski, Marcin},
  title =	{{A Technique to Speed up Symmetric Attractor-Based Algorithms for Parity Games}},
  booktitle =	{42nd IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2022)},
  pages =	{44:1--44:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-261-7},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{250},
  editor =	{Dawar, Anuj and Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2022.44},
  URN =		{urn:nbn:de:0030-drops-174365},
  doi =		{10.4230/LIPIcs.FSTTCS.2022.44},
  annote =	{Keywords: Parity games, Attractor decomposition, Quasipolynomial Algorithms, Universal trees}
}
Document
Half-Positional Objectives Recognized by Deterministic Büchi Automata

Authors: Patricia Bouyer, Antonio Casares, Mickael Randour, and Pierre Vandenhove

Published in: LIPIcs, Volume 243, 33rd International Conference on Concurrency Theory (CONCUR 2022)


Abstract
A central question in the theory of two-player games over graphs is to understand which objectives are half-positional, that is, which are the objectives for which the protagonist does not need memory to implement winning strategies. Objectives for which both players do not need memory have already been characterized (both in finite and infinite graphs); however, less is known about half-positional objectives. In particular, no characterization of half-positionality is known for the central class of ω-regular objectives. In this paper, we characterize objectives recognizable by deterministic Büchi automata (a class of ω-regular objectives) that are half-positional, in both finite and infinite graphs. Our characterization consists of three natural conditions linked to the language-theoretic notion of right congruence. Furthermore, this characterization yields a polynomial-time algorithm to decide half-positionality of an objective recognized by a given deterministic Büchi automaton.

Cite as

Patricia Bouyer, Antonio Casares, Mickael Randour, and Pierre Vandenhove. Half-Positional Objectives Recognized by Deterministic Büchi Automata. In 33rd International Conference on Concurrency Theory (CONCUR 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 243, pp. 20:1-20:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{bouyer_et_al:LIPIcs.CONCUR.2022.20,
  author =	{Bouyer, Patricia and Casares, Antonio and Randour, Mickael and Vandenhove, Pierre},
  title =	{{Half-Positional Objectives Recognized by Deterministic B\"{u}chi Automata}},
  booktitle =	{33rd International Conference on Concurrency Theory (CONCUR 2022)},
  pages =	{20:1--20:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-246-4},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{243},
  editor =	{Klin, Bartek and Lasota, S{\l}awomir 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.CONCUR.2022.20},
  URN =		{urn:nbn:de:0030-drops-170833},
  doi =		{10.4230/LIPIcs.CONCUR.2022.20},
  annote =	{Keywords: two-player games on graphs, half-positionality, memoryless optimal strategies, B\"{u}chi automata, \omega-regularity}
}
Document
Track A: Algorithms, Complexity and Games
Algorithms and Data Structures for First-Order Logic with Connectivity Under Vertex Failures

Authors: Michał Pilipczuk, Nicole Schirrmacher, Sebastian Siebertz, Szymon Toruńczyk, and Alexandre Vigny

Published in: LIPIcs, Volume 229, 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)


Abstract
We introduce a new data structure for answering connectivity queries in undirected graphs subject to batched vertex failures. Precisely, given any graph G and integer parameter k, we can in fixed-parameter time construct a data structure that can later be used to answer queries of the form: "are vertices s and t connected via a path that avoids vertices u₁,…, u_k?" in time 2^𝒪(k). In the terminology of the literature on data structures, this gives the first deterministic data structure for connectivity under vertex failures where for every fixed number of failures, all operations can be performed in constant time. With the aim to understand the power and the limitations of our new techniques, we prove an algorithmic meta theorem for the recently introduced separator logic, which extends first-order logic with atoms for connectivity under vertex failures. We prove that the model-checking problem for separator logic is fixed-parameter tractable on every class of graphs that exclude a fixed topological minor. We also show a weak converse. This implies that from the point of view of parameterized complexity, under standard complexity theoretical assumptions, the frontier of tractability of separator logic is almost exactly delimited by classes excluding a fixed topological minor. The backbone of our proof relies on a decomposition theorem of Cygan, Lokshtanov, Pilipczuk, Pilipczuk, and Saurabh [SICOMP '19], which provides a tree decomposition of a given graph into bags that are unbreakable. Crucially, unbreakability allows to reduce separator logic to plain first-order logic within each bag individually. Guided by this observation, we design our model-checking algorithm using dynamic programming over the tree decomposition, where the transition at each bag amounts to running a suitable model-checking subprocedure for plain first-order logic. This approach is robust enough to provide also an extension to efficient enumeration of answers to a query expressed in separator logic.

Cite as

Michał Pilipczuk, Nicole Schirrmacher, Sebastian Siebertz, Szymon Toruńczyk, and Alexandre Vigny. Algorithms and Data Structures for First-Order Logic with Connectivity Under Vertex Failures. In 49th International Colloquium on Automata, Languages, and Programming (ICALP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 229, pp. 102:1-102:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{pilipczuk_et_al:LIPIcs.ICALP.2022.102,
  author =	{Pilipczuk, Micha{\l} and Schirrmacher, Nicole and Siebertz, Sebastian and Toru\'{n}czyk, Szymon and Vigny, Alexandre},
  title =	{{Algorithms and Data Structures for First-Order Logic with Connectivity Under Vertex Failures}},
  booktitle =	{49th International Colloquium on Automata, Languages, and Programming (ICALP 2022)},
  pages =	{102:1--102:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-235-8},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{229},
  editor =	{Boja\'{n}czyk, Miko{\l}aj and Merelli, Emanuela and Woodruff, David P.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2022.102},
  URN =		{urn:nbn:de:0030-drops-164432},
  doi =		{10.4230/LIPIcs.ICALP.2022.102},
  annote =	{Keywords: Combinatorics and graph theory, Computational applications of logic, Data structures, Fixed-parameter algorithms and complexity, Graph algorithms}
}
Document
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
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
Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives

Authors: Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, and Mickael Randour

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)


Abstract
The window mechanism was introduced by Chatterjee et al. [Krishnendu Chatterjee et al., 2015] to strengthen classical game objectives with time bounds. It permits to synthesize system controllers that exhibit acceptable behaviors within a configurable time frame, all along their infinite execution, in contrast to the traditional objectives that only require correctness of behaviors in the limit. The window concept has proved its interest in a variety of two-player zero-sum games, thanks to the ability to reason about such time bounds in system specifications, but also the increased tractability that it usually yields. In this work, we extend the window framework to stochastic environments by considering the fundamental threshold probability problem in Markov decision processes for window objectives. That is, given such an objective, we want to synthesize strategies that guarantee satisfying runs with a given probability. We solve this problem for the usual variants of window objectives, where either the time frame is set as a parameter, or we ask if such a time frame exists. We develop a generic approach for window-based objectives and instantiate it for the classical mean-payoff and parity objectives, already considered in games. Our work paves the way to a wide use of the window mechanism in stochastic models.

Cite as

Thomas Brihaye, Florent Delgrange, Youssouf Oualhadj, and Mickael Randour. Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)


Copy BibTex To Clipboard

@InProceedings{brihaye_et_al:LIPIcs.CONCUR.2019.8,
  author =	{Brihaye, Thomas and Delgrange, Florent and Oualhadj, Youssouf and Randour, Mickael},
  title =	{{Life Is Random, Time Is Not: Markov Decision Processes with Window Objectives}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.8},
  URN =		{urn:nbn:de:0030-drops-109103},
  doi =		{10.4230/LIPIcs.CONCUR.2019.8},
  annote =	{Keywords: Markov decision processes, window mean-payoff, window parity}
}
Document
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}
}
  • Refine by Author
  • 7 Ohlmann, Pierre
  • 3 Fijalkow, Nathanaël
  • 3 Pilipczuk, Michał
  • 3 Toruńczyk, Szymon
  • 2 Casares, Antonio
  • Show More...

  • Refine by Classification
  • 3 Theory of computation → Finite Model Theory
  • 2 Theory of computation → Formal languages and automata theory
  • 2 Theory of computation → Logic and verification
  • 1 Mathematics of computing → Graph algorithms
  • 1 Mathematics of computing → Graph theory
  • Show More...

  • Refine by Keyword
  • 2 Universal graphs
  • 1 Arithmetic Circuit Complexity
  • 1 Attractor decomposition
  • 1 Büchi automata
  • 1 Combinatorics and graph theory
  • Show More...

  • Refine by Type
  • 10 document

  • Refine by Publication Year
  • 3 2022
  • 3 2023
  • 2 2020
  • 1 2017
  • 1 2019

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