arXiv subjects

Olivier Serre

Publications and source records attributed to Olivier Serre.

14 recordsLinked to original sources

arXiv2025

Games on Graphs: From Logic and Automata to Algorithms

The objective of this book is to give a comprehensive presentation of the research field concerned with infinite duration games on graphs. Historically, these game models appeared in the study of automata and logic, and they later became important for program verification and synthesis. They have many more applications, in particular some of the models investigated in this book were introduced and studied in neighbouring research communities such as optimisation, reinforcement learning, model theory, and set theory.

cs.GT↗

arXiv2021

Higher-Order Recursion Schemes and Collapsible Pushdown Automata: Logical Properties

This paper studies the logical properties of a very general class of infinite ranked trees, namely those generated by higher-order recursion schemes. We consider, for both monadic second-order logic and modal mu-calculus, three main problems: model-checking, logical reflection (aka global model-checking, that asks for a finite description of the set of elements for which a formula holds) and selection (that asks, if exists, for some finite description of a set of elements for which an MSO formula with a second-order free variable holds). For each of these problems we provide an effective solution. This is obtained thanks to a known connection between higher-order recursion schemes and collapsible pushdown automata and on previous work regarding parity games played on transition graphs of collapsible pushdown automata.

cs.LO↗

arXiv2020

Alternating Tree Automata with Qualitative Semantics

We study alternating automata with qualitative semantics over infinite binary trees: alternation means that two opposing players construct a decoration of the input tree called a run, and the qualitative semantics says that a run of the automaton is accepting if almost all branches of the run are accepting. In this paper we prove a positive and a negative result for the emptiness problem of alternating automata with qualitative semantics. The positive result is the decidability of the emptiness problem for the case of Büchi acceptance condition. An interesting aspect of our approach is that we do not extend the classical solution for solving the emptiness problem of alternating automata, which first constructs an equivalent non-deterministic automaton. Instead, we directly construct an emptiness game making use of imperfect information. The negative result is the undecidability of the emptiness problem for the case of co-Büchi acceptance condition. This result has two direct consequences: the undecidability of monadic second-order logic extended with the qualitative path-measure quantifier, and the undecidability of the emptiness problem for alternating tree automata with non-zero semantics, a recently introduced probabilistic model of alternating tree automata.

cs.FL↗

arXiv2020

Collapsible Pushdown Parity Games

This paper studies a large class of two-player perfect-information turn-based parity games on infinite graphs, namely those generated by collapsible pushdown automata. The main motivation for studying these games comes from the connections from collapsible pushdown automata and higher-order recursion schemes, both models being equi-expressive for generating infinite trees. Our main result is to establish the decidability of such games and to provide an effective representation of the winning region as well as of a winning strategy. Thus, the results obtained here provide all necessary tools for an in-depth study of logical properties of trees generated by collapsible pushdown automata/recursion schemes.

cs.FL↗

arXiv2020

Reasoning about strategies on collapsible pushdown arenas with imperfect information

Strategy Logic with imperfect information (SLiR) is a very expressive logic designed to express complex properties of strategic abilities in distributed systems. Previous work on SLiR focused on finite systems, and showed that the model-checking problem is decidable when information on the control states of the system is hierarchical among the players or components of the system, meaning that the players or components can be totally ordered according to their respective knowledge of the state. We show that moving from finite to infinite systems generated by collapsible (higher-order) pushdown systems preserves decidability, under the natural restriction that the stack content is visible. The proof follows the same lines as in the case of finite systems, but requires to use (collapsible) alternating pushdown tree automata. Such automata are undecidable, but semi-alternating pushdown tree automata were introduced and proved decidable, to study a strategic problem on pushdown systems with two players. In order to tackle multiple players with hierarchical information, we refine further these automata: we define direction-guided (collapsible) pushdown tree automata, and show that they are stable under projection, nondeterminisation and narrowing. For the latter operation, used to deal with imperfect information, stability holds under some assumption that is satisfied when used for systems with visible stack. We then use these automata to prove our main result.

cs.LO↗

arXiv2020

How Good Is a Strategy in a Game With Nature?

We consider games with two antagonistic players --- Éloïse (modelling a program) and Abélard (modelling a byzantine environment) --- and a third, unpredictable and uncontrollable player, that we call Nature. Motivated by the fact that the usual probabilistic semantics very quickly leads to undecidability when considering either infinite game graphs or imperfect-information, we propose two alternative semantics that leads to decidability where the probabilistic one fails: one based on counting and one based on topology.

cs.FL↗

arXiv2018

C-SHORe: Higher-Order Verification via Collapsible Pushdown System Saturation

Higher-order recursion schemes (HORS) have received much attention as a useful abstraction of higher-order functional programs with a number of new verification techniques employing HORS model-checking as their centrepiece. We give an account of the C-SHORe tool, which contributed to the ongoing quest for a truly scalable model-checker for HORS by offering a different, automata theoretic perspective. C-SHORe implements the first practical model-checking algorithm that acts on a generalisation of pushdown automata equi-expressive with HORS called collapsible pushdown systems (CPDS). At its core is a backwards saturation algorithm for CPDS. Additionally, it is able to use information gathered from an approximate forward reachability analysis to guide its backward search. Moreover, it uses an algorithm that prunes the CPDS prior to model-checking and a method for extracting counter-examples in negative instances. We provide an up-to-date comparison of C-SHORe with the state-of-the-art verification tools for HORS. The tool and additional material are available from http://cshore.cs.rhul.ac.uk.

cs.LO↗

arXiv2018

Emptiness of Stack Automata is NEXPTIME-complete: A Correction

A saturation algorithm for collapsible pushdown systems was published in ICALP 2012. This work introduced a class of stack automata used to recognised regular sets of collapsible pushdown configurations. It was shown that these automata form an effective boolean algebra, have a linear time membership problem, and are equivalent to an alternative automata representation appearing in LICS 2010. It was also claimed that the emptiness problem for stack automata is PSPACE-complete. Unfortunately, this claim is not true. We show that the problem is in fact NEXPTIME-complete when the stacks being accepted are collapsible pushdown stacks, rather than the annotated stacks used in ICALP 2012.

cs.FL↗

arXiv2018

Pure Strategies in Imperfect Information Stochastic Games

We consider imperfect information stochastic games where we require the players to use pure (i.e. non randomised) strategies. We consider reachability, safety, Büchi and co-Büchi objectives, and investigate the existence of almost-sure/positively winning strategies for the first player when the second player is perfectly informed or more informed than the first player. We obtain decidability results for positive reachability and almost-sure Büchi with optimal algorithms to decide existence of a pure winning strategy and to compute one if exists. We complete the picture by showing that positive safety is undecidable when restricting to pure strategies even if the second player is perfectly informed.

cs.FL↗

arXiv2017

Two-way Two-tape Automata

In this article we consider two-way two-tape (alternating) automata accepting pairs of words and we study some closure properties of this model. Our main result is that such alternating automata are not closed under complementation for non-unary alphabets. This improves a similar result of Kari and Moore for picture languages. We also show that these deterministic, non-deterministic and alternating automata are not closed under composition.

cs.FL↗

arXiv2016

Marking Shortest Paths On Pushdown Graphs Does Not Preserve MSO Decidability

In this paper we consider pushdown graphs, i.e. infinite graphs that can be described as transition graphs of deterministic real-time pushdown automata. We consider the case where some vertices are designated as being final and we built, in a breadth-first manner, a marking of edges that lead to such vertices (i.e., for every vertex that can reach a final one, we mark all out-going edges laying on some shortest path to a final vertex). Our main result is that the edge-marked version of a pushdown graph may itself no longer be a pushdown graph, as we prove that this enrich graph may have an undecidable MSO theory. In this paper we consider pushdown graphs, i.e. infinite graphs that can be described as transition graphs of deterministic real-time pushdown automata. We consider the case where some vertices are designated as being final and we build, in a breadth-first manner, a marking of edges that lead to such vertices (i.e., for every vertex that can reach a final one, we mark all out-going edges laying on some shortest path to a final vertex). Our main result is that the edge-marked version of a pushdown graph may itself no longer be a pushdown graph, as we prove that the MSO theory of this enriched graph may be undecidable.

cs.FL↗

arXiv2015

Streaming Property Testing of Visibly Pushdown Languages

In the context of language recognition, we demonstrate the superiority of streaming property testers against streaming algorithms and property testers, when they are not combined. Initiated by Feigenbaum et al., a streaming property tester is a streaming algorithm recognizing a language under the property testing approximation: it must distinguish inputs of the language from those that are $\varepsilon$-far from it, while using the smallest possible memory (rather than limiting its number of input queries). Our main result is a streaming $\varepsilon$-property tester for visibly pushdown languages (VPL) with one-sided error using memory space $\mathrm{poly}((\log n) / \varepsilon)$. This constructions relies on a (non-streaming) property tester for weighted regular languages based on a previous tester by Alon et al. We provide a simple application of this tester for streaming testing special cases of instances of VPL that are already hard for both streaming algorithms and property testers. Our main algorithm is a combination of an original simulation of visibly pushdown automata using a stack with small height but possible items of linear size. In a second step, those items are replaced by small sketches. Those sketches relies on a notion of suffix-sampling we introduce. This sampling is the key idea connecting our streaming tester algorithm to property testers.

cs.DS↗

arXiv2015

Counting Branches in Trees Using Games

We study finite automata running over infinite binary trees. A run of such an automaton is usually said to be accepting if all its branches are accepting. In this article, we relax the notion of accepting run by allowing a certain quantity of rejecting branches. More precisely we study the following criteria for a run to be accepting: - it contains at most finitely (resp countably) many rejecting branches; - it contains infinitely (resp uncountably) many accepting branches; - the set of accepting branches is topologically "big". In all situations we provide a simple acceptance game that later permits to prove that the languages accepted by automata with cardinality constraints are always $ω$-regular. In the case (ii) where one counts accepting branches it leads to new proofs (without appealing to logic) of an old result of Beauquier and Niwinski.

cs.FL↗

arXiv2011

Qualitative Concurrent Stochastic Games with Imperfect Information

We study a model of games that combines concurrency, imperfect information and stochastic aspects. Those are finite states games in which, at each round, the two players choose, simultaneously and independently, an action. Then a successor state is chosen accordingly to some fixed probability distribution depending on the previous state and on the pair of actions chosen by the players. Imperfect information is modeled as follows: both players have an equivalence relation over states and, instead of observing the exact state, they only know to which equivalence class it belongs. Therefore, if two partial plays are indistinguishable by some player, he should behave the same in both of them. We consider reachability (does the play eventually visit a final state?) and Büchi objective (does the play visit infinitely often a final state?). Our main contribution is to prove that the following problem is complete for 2-ExpTime: decide whether the first player has a strategy that ensures her to almost-surely win against any possible strategy of her oponent. We also characterise those strategies needed by the first player to almost-surely win.

cs.FL↗