Author name cluster

Olivier Serre

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

4 papers

1 author row

I&C Journal 2017 Journal Article

Counting branches in trees using games

Arnaud Carayol
Olivier Serre

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: (i) it contains at most finitely (resp. countably) many rejecting branches; (ii) it contains infinitely (resp. uncountably) many accepting branches; (iii) 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 a result of Beauquier and Niwiński.

Details DOI

I&C Journal 2013 Journal Article

Pushdown module checking with imperfect information

Benjamin Aminof
Axel Legay
Aniello Murano
Olivier Serre
Moshe Y. Vardi

The model checking problem for finite-state open systems (module checking) has been extensively studied in the literature, both in the context of environments with perfect and imperfect information about the system. Recently, the perfect information case has been extended to infinite-state systems (pushdown module checking). In this paper, we extend pushdown module checking to the imperfect information setting; i. e. , to the case where the environment has only a partial view of the systemʼs control states and pushdown store content. We study the complexity of this problem with respect to the branching-time temporal logics CTL, CTL ⁎ and the propositional μ-calculus. We show that pushdown module checking, which is by itself harder than pushdown model checking, becomes undecidable when the environment has imperfect information. We also show that undecidability relies on hiding information about the pushdown store. Indeed, we prove that with imperfect information about the control states, but a visible pushdown store, the problem is decidable and its complexity is 2Exptime-complete for CTL and the propositional μ-calculus, and 3Exptime-complete for CTL ⁎.

Details DOI

TCS Journal 2006 Journal Article

Games with winning conditions of high Borel complexity

Olivier Serre

We first consider infinite two-player games on pushdown graphs. In previous work, Cachat et al. [Solving pushdown games with a Σ 3 -winning condition, in: Proc. 11th Annu. Conf. of the European Association for Computer Science Logic, CSL 2002, Lecture Notes in Computer Science, Vol. 2471, Springer, Berlin, 2002, pp. 322–336] have presented a winning decidable condition that is Σ 3 -complete in the Borel hierarchy. This was the first example of a decidable winning condition of such Borel complexity. We extend this result by giving a family of decidable winning conditions of arbitrary finite Borel complexity. From this family, we deduce a family of decidable winning conditions of arbitrary finite Borel complexity for games played on finite graphs. The problem of deciding the winner for these conditions is shown to be non-elementary.

Details DOI

TCS Journal 2004 Journal Article

Vectorial languages and linear temporal logic

Olivier Serre

Determining for a given deterministic complete automaton the sequence of visited states while reading a given word is the core of important problems with automata-based solutions, such as approximate string matching. The main difficulty is to do this computation efficiently. Considering words as vectors and working on them using vectorial operations allows to solve the problem faster than using local operations. In this paper, we show first that the set of vectorial operations needed by an algorithm representing a given automaton depends on the language accepted by the automaton. We give precise characterizations for star-free, solvable and regular languages using vectorial algorithms. We also study classes of languages associated with restricted sets of vectorial operations and relate them with languages defined by fragments of linear temporal logic. Finally, we consider the converse problem of constructing an automaton from a given vectorial algorithm. As a byproduct, we show that the satisfiability problem for some extensions of LTL characterizing solvable and regular languages is PSPACE-complete.

Details DOI