Catálogo de publicaciones - libros

We propose a symbolic algorithm for the analysis of the robustness of timed automata, that is the correctness of the model in presence of small drifts on the clocks or imprecision in testing guards. This problem is known to be decidable with an algorithm based on detecting strongly connected components on the region graph, which, for complexity reasons, is not effective in practice. Our symbolic algorithm is based on the standard algorithm for symbolic reachability analysis using zones to represent symbolic states and can then be easily integrated within tools for the verification of timed automata models. It relies on the computation of the stable zone of each cycle in a timed automaton. The stable zone is the largest set of states that can reach and be reached from itself through the cycle. To compute the robust reachable set, each stable zone that intersects the set of explored states has to be added to the set of states to be explored.

The Performance Evaluation Process Algebra (PEPA) language is a stochastic process algebra, generating Continuous Time Markov Chains (CTMC) to allow quantitative analysis. Protocols such as BitTorrent are highly parallel in nature, and represent one area where CTMC analysis is limited by the well-known state space problem. The number of unique states each client can exist in, and the number of clients required to accurately model a typical BitTorrent network preclude the use of CTMCs. Recent work has shown that PEPA models also allow the derivation of an activity matrix, from which ODE and stochastic simulation models, as alternative forms of analysis, are possible. Using this technique, a BitTorrent network is created, analysed, and the results compared against previous BitTorrent models.

In this paper, we consider a novel approach to the temporal logic verification problem of continuous dynamical systems. Our methodology has the distinctive feature that enables the verification of the temporal properties of a continuous system by verifying only a finite number of its (simulated) trajectories. The proposed framework comprises two main ideas. First, we take advantage of the fact that in metric spaces we can quantify how close are two different states. Based on that, we define robust, multi-valued semantics for MTL (and LTL) formulas. These capture not only the usual Boolean satisfiability of the formula, but also topological information regarding the distance from unsatisfiability. Second, we use the recently developed notion of bisimulation functions to infer the behavior of a set of trajectories that lie in the neighborhood of the simulated one. If the latter set of trajectories is bounded by the tube of robustness, then we can infer that all the trajectories in the neighborhood of the simulated one satisfy the same temporal specification as the simulated trajectory. The interesting and promising feature of our approach is that the more robust the system is with respect to the temporal logic specification, the less is the number of simulations that are required in order to verify the system.

We solve some decision problems for timed automata which were raised by S. Tripakis in [Tri04] and by E. Asarin in [Asa04]. In particular, we show that one cannot decide whether a given timed automaton is determinizable or whether the complement of a timed regular language is timed regular. We show that the problem of the minimization of the number of clocks of a timed automaton is undecidable. It is also undecidable whether the shuffle of two timed regular languages is timed regular. We show that in the case of timed Büchi automata accepting infinite timed words some of these problems are Π_1 ^1-hard, hence highly undecidable (located beyond the arithmetical hierarchy).

Timed and weak timed simulation relations are often used to show that operations on hybrid systems result in equivalent behavior or in conservative overapproximations. Given that systems are frequently designed and verified in a modular approach, it is desirable that this relationship is compositional, which is not the case for hybrid systems in general. We identify subclasses of linear hybrid automata that are compositional with respect to timed, respectively weak timed simulation.

Real-time systems usually encompass parts that are best described by a continuous-time model, such as physical processes under control, together with other components that are more naturally formalized by a discrete-time model, such as digital computing modules. Describing such systems in a unified framework based on metric temporal logic requires to integrate formulas which are interpreted over discrete and continuous time. In this paper, we tackle this problem with reference to the metric temporal logic TRIO, that admits both a discrete-time and a continuous-time semantics. We identify sufficient conditions under which TRIO formulas have a consistent truth value when moving from continuous-time to discrete-time interpretations, or vice versa. These conditions basically involve the restriction to a proper subset of the TRIO language and a requirement on the finite variability over time of the basic items in the specification formulas. We demonstrate the approach with an example of specification and verification.

Well-known hierarchies discriminate between the computational power of discrete time and space dynamical systems. A contrario the situation is more confused for dynamical systems when time and space are continuous. A possible way to discriminate between these models is to state whether they can simulate Turing machine. For instance, it is known that continuous systems described by an ordinary differential equation (ODE) have this power. However, since the involved ODE is defined by overlapping local ODEs inside an infinite number of regions, this result has no significant application for differentiable models whose ODE is defined by an explicit representation. In this work, we considerably strengthen this result by showing that Time Differentiable Petri Nets (TDPN) can simulate Turing machines. Indeed the ODE ruling this model is expressed by an explicit linear expression enlarged with the “minimum” operator. More precisely, we present two simulations of a two counter machine by a TDPN in order to fulfill opposite requirements: robustness and boundedness. These simulations are performed by nets whose dimension of associated ODEs is constant. At last, we prove that marking coverability, submarking reachability and the existence of a steady-state are undecidable for TDPNs.

We extend the framework of ATL model-checking to “simply timed” concurrent game structures, i.e., multi-agent structures where each transition carry an integral duration (or interval thereof). While the case of single durations is easily handled from the semantics point of view, intervals of durations raise several interesting questions. Moreover subtle algorithmic problems have to be handled when dealing with model checking. We propose a semantics for which we develop efficient ( PTIME ) algorithms for timed ATL without equality constraints, while the general case is shown to be EXPTIME -complete.

We consider interval measurement logic IML , a sublogic of Zhou and Hansen’s interval logic, with measurement functions which provide real-valued measurement of some aspect of system behaviour in a given time interval. We interpret IML over a variety of time domains (continuous, sampled, integer) and show that it can provide a unified treatment of many diverse temporal logics including duration calculus (DC), interval duration logic (IDL) and metric temporal logic (MTL). We introduce a fragment GIML with restricted measurement modalities which subsumes most of the decidable timed logics considered in the literature. Next, we introduce a guarded first-order logic with measurements MGF . As a generalisation of Kamp’s theorem, we show that over arbitrary time domains, the measurement logic GIML is expressively complete for it. We also show that MGF has the 3-variable property. In addition, we have a preliminary result showing the decidability of a subset of GIML when interpreted over timed words.

We show how to transform formulae written in the real-time temporal logic MITL into timed automata that recognize their satisfying models. This compositional construction is much simpler than previously known and can be easily implemented.