Formal Methods for the Verification of Distributed Timed Systems

Distributed Real-Time Systems (DRTS) take an increasingly important role in everyday life, from traffic light controllers to aircrafts 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. But, the traditional real-time formalisms for reasoning about DRTS, 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 RTS are Timed Automata (TA) [AD94], Event Clock Automata (ECA) [AFH94] and Recursive Event Clock Automata (RECA) [HRS98]. A TA is a finite automaton augmented with real-valued clocks. The model of TA assumes perfect clocks: all clocks have infinite precision and are perfectly synchronized. This causes TA to have an undecidable language inclusion problem [AD94]. These negative results for TA spurred a quest for study of expressive but still fully decidable formalisms. To restore decidability, [AFH94] proposed to restrict the behavior of clocks. Therefore, an Event Clock (EC) is reset when a given atomic proposition occurs. The event clock values are deterministic and thus Event Clock Automata (ECA) are determinizable, making language inclusion decidable.
However, the expressiveness of ECA is rather weak. Furthermore, the temporal logic with Event Clocks [RS97] violates the substitution principle: Any proposition should be replaceable by a formula. Hence [HRS98] introduced the notion of Recursive Event. In a recursive event model (RECA), the reset of a clock is decided by a lower-level automaton (or formula). This automaton cannot read the clock that is resetting. Clock resets are thus still deterministic, but the concept of event is now much more expressive. Also, [HRS98] introduced the temporal logic of recursive event clocks (EventClockTL).
There are other variants of TA called Distributed Timed Automata (DTA) and Timed Automata with Independent Clocks (icTA) who are proposed by [Kri99] and [ABG+08] to model DRTS, where the clocks are not necessarily synchronized. Constraints on the clocks are used to restrict the behaviors of the automata. In DTA, the clocks belonging to one process can be read by another process, but a clock can only be reset by its owner process. DTA and icTA are neither determinizable nor complementable and their inclusion problems are undecidable [ABG+08]. However, the standard semantics of TA is sequential and based on a Timed Labelled Transition System (TLTS), i.e., a run of a TA is given by a sequence of actions and (single) global timestamp, while using several clocks and associate them accordingly several (multiple) timestamps could be an improved representation of real DRTS.
Moreover, it is a well-known fact that, model checking over DRTS becomes rapidly intractable because the state space often grows exponentially with the number of components considered. One of the most effective and successful techniques currently available to reduce the state space is to merge

2
states with the same behavior. For untimed systems, the notion of bisimulation [Mil89] is classically used to this end, and its natural extension for Real-Time Systems (RTS, timed bisimulation, has been used to verify the preservation of sequential behavior and timed properties expressed in timed temporal logics (e.g. Timed CTL [TY01] or Lν [LLW95]). Timed bisimulation was already shown to be decidable for TA [AD94, LLW95], but its standard definition is also based on a TLTS.
In this proposal, we remove the above problems of undecidability, perfect clock synchronization and single timestamps. Here, inspired by [BJLY98, Kri99, ABG+08, HRS98] and [AFH94], we introduce:
1. Distributed Event Clocks (DEC) : A DEC xq (or yq) records the time since the last (resp. next) reset, measured in the local time of process q and the DEC can advance totally independently if they are in different processes. However [Pur98, DWDMR04] studied the opposite case, where the difference between clocks (drift) is infinitesimally small.
2. Multiple Local Times (MLT) : A DRTS involve multiple interconnected real-time components (called here processes) where each process uses its own local clocks running at its own rate. Thus, a single timestamp suffices for global clocks while multiple timestamps support independent local clocks.
We propose formal methods for the specification and verification of 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, thus closed under complementation; also that their respective language inclusion problems are decidable (more exactly, PSPACE-complete). Additionally, we propose extensions of the existing EventClockTL with distributed clocks to allow the specification of distributed and timed properties. This gives us the Distributed (Recursive) Event Clock Temporal Logic (DECTL which we show are PSPACE-complete for the satisfiability and validity problem. Finally, we show the applicability of DECA and DECTL over a DRTS.
Also, we extend the Timed Labelled Transition Systems (TLTS) and icTA semantics [ABG+08] to work with the notion of MLT. Hence, we propose a new real-time formalism called Multi-timed Automata (MTA) based on icTA( and MLT). We extend the classical theory of timed bisimulation [Cer93] with the new notion of multi-timed bisimulation and MTA. We show that multi-timed bisimulation is decidable (more exactly, EXPTIME-complete). Furthermore, we will propose an efficient algorithm for timed bisimulation using refinement techniques. Additionally, we propose to extend the existing Lν and Hennessy-Milner logics with independent local clocks, yielding the (multi-timed) modal logic MLν. Finally, we show the applicability of MTA and MLν over a DRTS.