Catálogo de publicaciones - libros

The theory of graph games with ω -regular winning conditions is the foundation for modeling and synthesizing reactive processes. In the case of stochastic reactive processes, the corresponding stochastic graph games have three players, two of them (System and Environment) behaving adversarially, and the third (Uncertainty) behaving probabilistically. We consider two problems for stochastic graph games: the qualitative problem asks for the set of states from which a player can win with probability 1 ( almost-sure winning ); and the quantitative problem asks for the maximal probability of winning ( optimal winning ) from each state. We consider ω -regular winning conditions formalized as Müller winning conditions. We present optimal memory bounds for pure almost-sure winning and optimal winning strategies in stochastic graph games with Müller winning conditions. We also present improved memory bounds for randomized almost-sure winning and optimal strategies.

We consider games where the winning conditions are disjunctions (or dually, conjunctions) of parity conditions; we call them generalized parity games. These winning conditions, while ω -regular, arise naturally when considering fair simulation between parity automata, secure equilibria for parity conditions, and determinization of Rabin automata. We show that these games retain the computational complexity of Rabin and Streett conditions; i.e., they are NP-complete and co-NP-complete, respectively. The (co-)NP-hardness is proved for the special case of a conjunction/disjunction of two parity conditions, which is the case that arises in fair simulation and secure equilibria. However, considering these games as Rabin or Streett games is not optimal. We give an exposition of Zielonka’s algorithm when specialized to this kind of games. The complexity of solving these games for k parity objectives with d priorities, n states, and m edges is $O(n^{2 k d} \cdot m) \cdot \frac{(k\cdot d)!}{d!^k}$ , as compared to O ( n ^2 k d · m ) ·( k · d )! when these games are solved as Rabin/Streett games. We also extend the subexponential algorithm for solving parity games recently introduced by Jurdziński, Paterson, and Zwick to generalized parity games. The resulting complexity of solving generalized parity games is $n^{O(\sqrt{n})} \cdot \frac{(k\cdot d)!}{d!^k}$ . As a corollary we obtain an improved algorithm for Rabin and Streett games with d pairs, with time complexity $n^{O(\sqrt{n})} \cdot d!$ .

Tree automata with one memory have been introduced in 2001. They generalize both pushdown (word) automata and the tree automata with constraints of equality between brothers of Bogaert and Tison. Though it has a decidable emptiness problem, the main weakness of this model is its lack of good closure properties. We propose a generalization of the visibly pushdown automata of Alur and Madhusudan to a family of tree recognizers which carry along their (bottom-up) computation an auxiliary unbounded memory with a tree structure (instead of a symbol stack). In other words, these recognizers, called visibly Tree Automata with Memory (VTAM) define a subclass of tree automata with one memory enjoying Boolean closure properties. We show in particular that they can be determinized and the problems like emptiness, inclusion and universality are decidable for VTAM. Moreover, we propose an extension of VTAM whose transitions may be constrained by structural equality and disequality tests between memories, and show that this extension preserves the good closure and decidability properties.

The model checking problem for open finite-state systems (called module checking ) has been intensively studied in the literature with respect to CTL and CTL ^*. In this paper, we focus on module checking with respect to the fully enriched μ -calculus and some of its fragments. Fully enriched μ -calculus is the extension of the propositional μ -calculus with inverse programs , graded modalities , and nominals . The fragments we consider here are obtained by dropping at least one of the additional constructs. For the full calculus, we show that module checking is undecidable by using a reduction from the domino problem. For its fragments, instead, we show that module checking is decidable and ExpTime -complete. This result is obtained by using, for the upper bound, a classical automata-theoretic approach via Forest Enriched Automata and, for the lower bound, a reduction from the module checking problem for CTL , known to be ExpTime -hard.

We study the complexity of satisfiability in the expressive extension ICPDL of PDL (Propositional Dynamic Logic), which admits intersection and converse as program operations. Our main result is containment in 2 EXP , which improves the previously known non-elementary upper bound and implies 2 EXP -completeness due to an existing lower bound for PDL with intersection. The proof proceeds by showing that every satisfiable ICPDL formula has a model of tree-width at most two and then giving a reduction to the (non)-emptiness problem for alternating two-way automata on infinite trees. In this way, we also reprove in an elegant way Danecki’s difficult result that satisfiability for PDL with intersection is in 2 EXP .

Higher-order pushdown systems (PDSs) generalise pushdown systems through the use of higher-order stacks, that is, a nested “stack of stacks” structure. We further generalise higher-order PDSs to higher-order Alternating PDSs (APDSs) and consider the backwards reachability problem over these systems. We prove that given an order- n APDS, the set of configurations from which a given regular set of configurations is reachable is itself regular and computable in n -EXPTIME. We show that the result has several useful applications in the verification of higher-order PDSs such as LTL model checking, alternation-free μ -calculus model checking, and the computation of winning regions of reachability games.

We give an axiomatisation of strong bisimilarity on a small fragment of CCS that does not feature the sum operator. This axiomatisation is then used to derive congruence of strong bisimilarity in the finite π -calculus in absence of sum. To our knowledge, this is the only nontrivial subcalculus of the π -calculus that includes the full output prefix and for which strong bisimilarity is a congruence.

ATL is a temporal logic geared towards the specification and verification of properties in multi-agents systems. It allows to reason on the existence of strategies for coalitions of agents in order to enforce a given property. We prove that the standard definition of ATL (built on modalities “Next”, “Always” and “Until”) has to be completed in order to express the duals of its modalities: it is necessary to add the modality “Release”. We then precisely characterize the complexity of ATL model-checking when the number of agents is not fixed. We prove that it is $\bf \Delta_{\rm 2}^{\sf P}$ - and $\bf \Delta_{\rm 3}^{\sf P}$ -complete, depending on the underlying multi-agent model ( ATS and CGS resp.). We also prove that ATL + model-checking is $\bf \Delta_{\rm 3}^{\sf P}$ -complete over both models, even with a fixed number of agents.

Logics that can reason about sets and their cardinality bounds are useful in program analysis, program verification, databases, and knowledge bases. This paper presents a class of constraints on sets and their cardinalities for which the satisfiability and the entailment problems are computable in polynomial time. Our class of constraints, based on tree-shaped formulas, is unique in being simultaneously tractable and able to express 1) that a set is a union of other sets, 2) that sets are disjoint, and 3) that a set has cardinality within a given range. As the main result we present a polynomial-time algorithm for checking entailment of our constraints.

A web service is modeled here as a finite state machine. A composition problem for web services is to decide if a given web service can be constructed from a given set of web services; where the construction is understood as a simulation of the specification by a fully asynchronous product of the given services. We show an EXPTIME-lower bound for this problem, thus matching the known upper bound. Our result also applies to richer models of web services, such as the Roman model. Keywords: Automata simulation, complexity, web services composition.