Modeling and Verifying Distributed and RealTime Systems using Timed Automata with Partially Independent Clocks
Défense de thèse de James ORTIZ VEGA
Date : 04/07/2023 14:00  04/07/2023 16:00
Lieu : PA01
Orateur(s) : James Ortiz Vega
Organisateur(s) : Isabelle Daelman
Distributed RealTime 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 realtime formalisms have been proposed to formalize and prove properties of DRTS. However, traditional realtime 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 realtime systems (RTS) are Timed Automata (TA), Event Clock Automata (ECA) and Recursive Event Clock Automata (RECA). A TA is a finite automaton augmented with realvalued 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, PSPACEcomplete). 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 PSPACEcomplete 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 multitimed words. Therefore, we propose a new realtime formalism called Multitimed Automata (MTA) based on icTA. We also propose a timed modal logic with independent local clocks, which leads to the (multitimed) modal logic MLν. We extend the classical theory of timed bisimulation with the new notion of multitimed bisimulation and MTA. We show that multitimed bisimulation is decidable (more precisely, EXPTIMEcomplete). Furthermore, we propose an efficient algorithm for multitimed 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 multitimed words, yielding the (derivative) multitimed modal logic DMLν and Timed Automata with Clock Derivatives (DMTA). We show that (derivative) multitimed bisimulation is decidable (more precisely, EXPTIMEcomplete). Furthermore, we propose an efficient algorithm for (derivative) multitimed 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