Modeling and Verifying Distributed and Real-Time Systems using Timed Automata with Partially Independent Clocks

Défense de thèse de James ORTIZ VEGA

Distributed Real-Time Systems (DRTS) play an increasingly important role in everyday life, from traffic light controllers to airplanes, and from telecommunication networks to medical systems. In the last decades, several formal methods and real-time formalisms have been proposed to formalize and prove properties of DRTS. However, traditional real-time formalisms are not always adequate for reasoning about DRTS because they assume a unique, perfectly synchronous (Newtonian) measure of time. The most successful techniques for modeling real-time systems (RTS) are Timed Automata (TA), Event Clock Automata (ECA) and Recursive Event Clock Automata (RECA). A TA is a finite automaton augmented with real-valued clocks, where all clocks have infinite precision and are perfectly synchronized. This causes TA to have an undecidable language inclusion problem. These negative results for TA spurred the search for expressive but still fully decidable formalisms. To restore decidability, Alur et al. proposed to restrict the behavior of clocks. Thus, an event clock (EC) is reset when a given atomic proposition occurs. The values of the event clocks are deterministic, and thus Event Clock Automata (ECA) are determinizable, which makes the language inclusion decidable. There are other variants of TA called Distributed Timed Automata (DTA) and Timed Automata with Independent Clocks (icTA) proposed by Krishnan et al. and Akshay et al. to model DRTS where the clocks are not necessarily synchronized. DTA and icTA are neither determinable nor complementable, and their inclusion problems are undecidable.

 

In this thesis, we remove the above problems of undecidability, perfect clock synchronization, and single timestamps. We introduce three alternative semantics:

 

(i)                  Distributed Event Clocks: we propose a formal semantics for modeling DRTS based on Recursive Event Clock Automata (RECA) with such distributed (a.k.a. independent) clocks, yielding the Distributed Recursive Event Clock Automata (DECA). We will show that DECA are determinizable, i.e. closed under complementation, and that their respective language inclusion problems are decidable (more precisely, PSPACE-complete). In addition, we propose to extend the existing timed temporal logic (EventClockTL) with distributed clocks to allow the specification of distributed and timed temporal properties. This gives us the Distributed (Recursive) Event Clock Temporal Logic (DECTL), which we show to be PSPACE-complete for the satisfiability and validity problems.

(ii)                 Multiple Independent Clocks: we extend the standard semantics of TA and timed bisimulation to include the notion of multiple independent clocks. Therefore, we extend the Timed Labelled Transition Systems (TLTS) and icTA semantics to work with the notion of multi-timed words. Therefore, we propose a new real-time formalism called Multi-timed Automata (MTA) based on icTA. We also propose a timed modal logic with independent local clocks, which leads to the (multi-timed) modal logic MLν. We extend the classical theory of timed bisimulation with the new notion of multi-timed bisimulation and MTA. We show that multi-timed bisimulation is decidable (more precisely, EXPTIME-complete). Furthermore, we propose an efficient algorithm for multi-timed bisimulation using refinement techniques.

(iii)               Distributed Clock Derivatives: We extend the semantics of TA to include the notion of distributed clock derivatives. Therefore, we extend the semantics of TA and Lν to work with the notion of multi-timed words, yielding the (derivative) multi-timed modal logic DMLν and Timed Automata with Clock Derivatives (DMTA). We show that (derivative) multi-timed bisimulation is decidable (more precisely, EXPTIME-complete). Furthermore, we propose an efficient algorithm for (derivative) multi-timed bisimulation using refinement techniques.Keywords: Formal Verification, Model Checking, Timed Automata, Timed Temporal Logics, Timed Bisimulation

 

Keywords: Formal Verification, Model Checking, Timed Automata, Timed Temporal Logics, Timed Bisimulation.

 

Pour toute inscription:

https://www.unamur.be/info/formulaires/jortiz_thesis

Contact : Isabelle Daelman - isabelle.daelman@unamur.be
Télecharger : vCal