Searcharxiv⌕ Search

arXiv subjects

Laurent Doyen

Publications and source records attributed to Laurent Doyen.

40 records · Page 3Linked to original sources

Expressiveness and Closure Properties for Quantitative Languages

Weighted automata are nondeterministic automata with numerical weights on transitions. They can define quantitative languages $L$ that assign to each word $w$ a real number $L(w)$. In the case of infinite words, the value of a run is naturally computed as the maximum, limsup, liminf, limit average, or discounted sum of the transition weights. We study expressiveness and closure questions about these quantitative languages. We first show that the set of words with value greater than a threshold can be non-$ω$-regular for deterministic limit-average and discounted-sum automata, while this set is always $ω$-regular when the threshold is isolated (i.e., some neighborhood around the threshold contains no word). In the latter case, we prove that the $ω$-regular language is robust against small perturbations of the transition weights. We next consider automata with transition weights 0 or 1 and show that they are as expressive as general weighted automata in the limit-average case, but not in the discounted-sum case. Third, for quantitative languages $L_1$ and $L_2$, we consider the operations $\max(L_1,L_2)$, $\min(L_1,L_2)$, and $1-L_1$, which generalize the boolean operations on languages, as well as the sum $L_1 + L_2$. We establish the closure properties of all classes of quantitative languages with respect to these four operations.

cs.LO↗

Antichains for the Automata-Based Approach to Model-Checking

We propose and evaluate antichain algorithms to solve the universality and language inclusion problems for nondeterministic Buechi automata, and the emptiness problem for alternating Buechi automata. To obtain those algorithms, we establish the existence of simulation pre-orders that can be exploited to efficiently evaluate fixed points on the automata defined during the complementation step (that we keep implicit in our approach). We evaluate the performance of the algorithm to check the universality of Buechi automata using the random automaton model recently proposed by Tabakov and Vardi. We show that on the difficult instances of this probabilistic model, our algorithm outperforms the standard ones by several orders of magnitude.

cs.LO↗

Alpaga: A Tool for Solving Parity Games with Imperfect Information

Alpaga is a solver for two-player parity games with imperfect information. Given the description of a game, it determines whether the first player can ensure to win and, if so, it constructs a winning strategy. The tool provides a symbolic implementation of a recent algorithm based on antichains.

cs.GT↗

Algorithms for Omega-Regular Games with Imperfect Information

We study observation-based strategies for two-player turn-based games on graphs with omega-regular objectives. An observation-based strategy relies on imperfect information about the history of a play, namely, on the past sequence of observations. Such games occur in the synthesis of a controller that does not see the private state of the plant. Our main results are twofold. First, we give a fixed-point algorithm for computing the set of states from which a player can win with a deterministic observation-based strategy for any omega-regular objective. The fixed point is computed in the lattice of antichains of state sets. This algorithm has the advantages of being directed by the objective and of avoiding an explicit subset construction on the game graph. Second, we give an algorithm for computing the set of states from which a player can win with probability 1 with a randomized observation-based strategy for a Buechi objective. This set is of interest because in the absence of perfect information, randomized strategies are more powerful than deterministic ones. We show that our algorithms are optimal by proving matching lower bounds.

cs.LO↗