Catálogo de publicaciones - libros

Recently, a new approach to the symbolic model checking of timed automata based on a partial order semantics was introduced, which relies on event zones that use vectors of event occurrences instead of clock zones that use vectors of clock values grouped in polyhedral clock constraints. Symbolic state exploration with event zones rather than clock zones can result in significant reductions in the number of symbolic states explored. In this work, we show how to extend the event zone approach to networks of automata with local state invariants, an important feature for modeling complex timed systems. To avoid formalizing local states, we attach to each transition an urgency constraint, that allows to code local state invariants. We have integrated the extension into a prototype tool with event zones and reported very promising experimental results.

Polygonal hybrid systems (SPDI) are a subclass of planar hybrid automata which can be represented by piecewise constant differential inclusions. The reachability problem as well as the computation of certain objects of the phase portrait, namely the viability, controllability and invariance kernels, for such systems is decidable. In this paper we show how to compute another object of an SPDI phase portrait, namely semi-separatrix curves and show how the phase portrait can be used for reducing the state-space for optimizing the reachability analysis.

We compare the expressiveness of variants of Metric Temporal Logic (MTL) obtained by adding the past operators ‘ S ’ and ‘ S _ I ’. We consider these variants under the “pointwise” and “continuous” interpretations over both finite and infinite models. Among other results, we show that for each of these variants the continuous version is strictly more expressive than the pointwise version. We also prove a counter-freeness result for MTL which helps to carry over some results from [3] for the case of infinite models to the case of finite models.

We describe a concept and design of a simulator of Real-Time Abstract State Machines. Time can be continuous or discrete. Time constraints are defined by linear inequalities. Two semantics are considered: with and without non-deterministic bounded delays between actions. The simulator is easily configurable. Simulation tasks can be generated according to descriptions in a special language. The simulator will be used for on-the-fly verification of formulas in an expressible timed predicate logic. Several features that facilitate the simulation are described: external functions definition, delays settings, constraints specification, and others.

Continuous-time Markov decision process are an important variant of labelled transition systems having nondeterminism through labels and stochasticity through exponential fire-time distributions. Nondeterministic choices are resolved using the notion of a scheduler . In this paper we characterize the class of measurable schedulers, which is the most general one, and show how a measurable scheduler induces a unique probability measure on the sigma-algebra of infinite paths. We then give evidence that for particular reachability properties it is sufficient to consider a subset of measurable schedulers. Having analyzed schedulers and their induced probability measures we finally show that each probability measure on the sigma-algebra of infinite paths is indeed induced by a measurable scheduler which proves that this class is complete.