Catálogo de publicaciones - libros

We consider the minimum-time reachability problem in concurrent two-player timed automaton game structures. We show how to compute the minimum time needed by a player to reach a target location against all possible choices of the opponent. We do not put any syntactic restriction on the game structure, nor do we require any player to guarantee time divergence. We only require players to use receptive strategies which do not block time. The minimal time is computed in part using a fixpoint expression, which we show can be evaluated on equivalence classes of a non-trivial extension of the clock-region equivalence relation for timed automata.

In a reachability-time game, players Min and Max choose moves so that the time to reach a final state in a timed automaton is minimised or maximised, respectively. Asarin and Maler showed decidability of reachability-time games on strongly non-Zeno timed automata using a value iteration algorithm. This paper complements their work by providing a strategy improvement algorithm for the problem. It also generalizes their decidability result because the proposed strategy improvement algorithm solves reachability-time games on all timed automata. The exact computational complexity of solving reachability-time games is also established: the problem is EXPTIME-complete for timed automata with at least two clocks.

We introduce stochastic priority games — a new class of perfect information stochastic games. These games can take two different, but equivalent, forms. In stopping priority games a play can be stopped by the environment after a finite number of stages, however, infinite plays are also possible. In discounted priority games only infinite plays are possible and the payoff is a linear combination of the classical discount payoff and of a limit payoff evaluating the performance at infinity. Shapley games [1] and parity games [2] are special extreme cases of priority games.

A data tree is a tree where each node has a label from a finite set, and a data value from a possibly infinite set. We consider data trees whose depth is bounded beforehand. By developing an appropriate automaton model, we show that under this assumption various formalisms, including a two variable first-order logic and a subset of XPath, have decidable emptiness problems.

We propose an extension of the tree automata with constraints between direct subtrees (Bogaert and Tison, 1992) to unranked trees. Our approach uses MSO-formulas to capture the possibility of comparing unboundedly many direct subtrees. Our main result is that the nonemptiness problem for the deterministic automata, as in the ranked setting, is decidable. Furthermore, we show that the nondeterministic automata are more expressive than the deterministic ones.

Nested words are a restriction of the class of visibly pushdown languages that provide a natural model of runs of programs with recursive procedure calls. The usual connection between monadic second-order logic (MSO) and automata extends from words to nested words and gives us a natural notion of regular languages of nested words.

In this paper we look at some well-known aspects of regular languages – their characterization via fixed points, deterministic and alternating automata for them, and synchronization for defining regular relations – and extend them to nested words. We show that mu-calculus is as expressive as MSO over finite and infinite nested words, and the equivalence holds, more generally, for mu-calculus with past modalities evaluated in arbitrary positions in a word, not only in the first position. We introduce the notion of alternating automata for nested words, show that they are as expressive as the usual automata, and also prove that Muller automata can be determinized (unlike in the case of visibly pushdown languages). Finally we look at synchronization over nested words. We show that the usual letter-to-letter synchronization is completely incompatible with nested words (in the sense that even the weakest form of it leads to an undecidable formalism) and present an alternative form of synchronization that gives us decidable notions of regular relations.

Following the idea developed by I. Simon in his theorem of Ramseyan factorisation forests, we develop a result of ‘deterministic factorisations’. This extra determinism property makes it usable on trees (finite or infinite).

We apply our result for proving that, , every monadic interpretation is equivalent to the composition of a first-order interpretation (with access to the ancestor relation) and a monadic marking. Using this remark, we give new characterisations for prefix-recognisable structures and for the Caucal hierarchy.

Furthermore, we believe that this approach has other potential applications.

Gaifman’s locality theorem states that every first-order sentence is equivalent to a local sentence. We show that there is no elementary bound on the length of the local sentence in terms of the original.

The classical Łoś-Tarski theorem states that every first-order sentence preserved under extensions is equivalent to an existential sentence. We show that there is no elementary bound on the length of the existential sentence in terms of the original. Recently, variants of the Łoś-Tarski theorem have been proved for certain classes of finite structures, among them the class of finite acyclic structures and more generally classes of structures of bounded tree width. Our lower bound also applies to these variants.

We further prove that a version of the Feferman-Vaught theorem based on a restriction by formula length necessarily entails a non-elementary blow-up in formula size.

All these results are based on a similar technique of encoding large numbers by trees of small height in such a way that small formulas can speak about these numbers. Notably, our lower bounds do not apply to restrictions of the results to structures of bounded degree. For such structures, we obtain elementary upper bounds in all cases. However, even there we can prove at least doubly exponential lower bounds.

We investigate a class of parametric timed automata, called lower bound/upper bound (L/U) automata, where each parameter occurs in the timing constraints either as a lower bound or as un upper bound. For such automata, we show that checking if for a parameter valuation (resp., all parameter valuations) there is an infinite accepting run is -complete. We extend these results by allowing the specification of constraints on parameters as a linear system. We show that the considered decision problems are still -complete, if the lower bound parameters are not compared to the upper bound parameters in the linear system, and are undecidable in general. Finally, we consider a parametric extension of , and prove that the related satisfiability and model checking (w.r.t. L/U automata) problems are -complete.

Recursive state machines (s) are models for programs with recursive procedural calls. While model-checking is -complete on such models, on finite-state machines, it is -complete in general and becomes -complete for interesting fragments. In this paper, we systematically study the computational complexity of model-checking s against several syntactic fragments of . Our main result shows that if in the specification we disallow and , and retain only the and operators, model-checking is in . Thus, differently from the full logic, for this fragment the abstract complexity of model-checking does not change moving from finite-state machines to s. Our results on the other studied fragments confirm this trend, in the sense that, moving from finite-state machines to s, the complexity of model-checking either rises from -complete to -complete, or stays within .