An ω-regular language is Eve-positional if, in all games with this language as objective, the existential player can play optimally without keeping any information from the previous moves. This notion plays a crucial role in verification, automata theory and synthesis. Casares and Ohlmann recently gave several characterisations of Eve-positionality of ω-regular languages. For this, they introduce the notion of ε-complete parity automaton and show (among other results) that an ω-regular language is Eve-positional if and only if it can be recognised by some ε-completion of a deterministic parity automaton. Colcombet and Idir built on their work, and obtained a more direct algebraic characterisation of Eve-positionality. We introduce a new formalism that characterises the Eve-positional languages, consisting of a restriction of non-deterministic Büchi automata. This allows us to complete a missing implication in Casares and Ohlmann’s work. We then use this formalism to describe a determinization procedure for non-deterministic Büchi automata recognising such languages, with size blow-up at most factorial. We also show that this construction is state-wise optimal for languages over sufficiently complete alphabets.

International audience

The parity index problem of tree automata asks, given a regular tree language $L$ and a set of priorities $J$, is $L$ $J$-feasible, that is, recognised by a nondeterministic parity automaton with priorities $J$? This is a long-standing open problem, of which only a few sub-cases and variations are known to be decidable. In a significant but technically difficult step, Colcombet and Löding reduced the problem to the uniform universality of distance-parity automata. In this article, we revisit the index problem using tools from the parity game literature. We add some counters to Lehtinen's register game, originally used to solve parity games in quasipolynomial time, and use this novel game to characterise $J$-feasibility. This provides a alternative proof to Colcombet and Löding's reduction. We then provide a second characterisation, based on the notion of attractor decompositions and the complexity of their structure, as measured by a parameterised version of their Strahler number, which we call $n$-Strahler number. Finally, we rephrase this result using the notion of universal tree extended to automata: a guidable automaton recognises a $[1,2j]$-feasible language if and only if it admits a universal tree with $n$-Strahler number $j$, for some $n$. In particular, a language recognised by a guidable automaton $A$ is Büchi-feasible if and only if there is a uniform bound $n\in \mathbb{N}$ such that all trees in the language admit an accepting run with an attractor decomposition of width bounded by $n$, or, equivalently, if and only $A$ admits a \textit{finite} universal tree. While we do not solve the decidability of the index problem, our work makes the state-of-the-art more accessible and brings to light the deep relationships between the $J$-feasibility of a language and attractor decompositions, universal trees and Lehtinen's register game.

Covering a given area with a team of mobile robots in a minimum time is a well-studied problem with many real-world applications. A rarely studied subject, however, is the case of a weighted plane: due to the necessity of taking time-consuming measurements or having to traverse different kinds of terrains, the coverage time may vary over the environment and the path planning needs to be adapted accordingly. In this paper, we present an adapted version of a state-of-the-art mCPP (multi-robot coverage path planning) approach, the DARP algorithm, to make it suitable to deal with weighted environments. In particular, we propose several modifications to DARP that allow overcoming some of its limitations and, as a result, obtain an increased convergence rate and decreased convergence time with respect to the original version. Furthermore, as proved by extensive simulations, these improvements are also noticed in the unweighted version of the problem.