April 7, 2025
James Jerson Ortiz Vega (Université de Namur)The demand for large-scale, complex distributed applications is growing with the expansion of distributed computing and networking. Distributed Real-Time Applications are essential for controlling and monitoring Distributed Real-Time Systems (DRTS) in domains like aerospace, robotics, and nuclear plants. DRTS often operate on heterogeneous networks with multiple interconnected components, each equipped with independent, unsynchronized clocks. While Timed Automata (TA) and Distributed Timed Automata (DTA) are standard formalisms for modeling DRTS, they have limitations: TA assumes synchronized clocks, and DTA may fail to fully capture indirect interactions or dependencies between clocks. This paper introduces idTA, a novel, more expressive variant of TA and DTA that controls clock drift. We also present DLν, an extension of Lν logic incorporating our idTA semantics, with semantics defined over Multi-Timed Labeled Transition Systems (MLTS). We prove that model checking for DLν is EXPTIME-complete and introduce MIMETIC, a model checking tool tailored for verifying DRTS.