Extending Timed Automata with Clock Derivatives
摘要
The increasing complexity of safety-critical systems in domains like aerospace, robotics, and industrial control demands precise modeling and verification methods. While Timed Automata (TA) and Distributed Timed Automata (DTA) are standard formalisms for real-time systems, they assume synchronized clocks or lack the expressiveness to capture clock drift and indirect timing dependencies. To overcome these limits, we propose Timed Automata with Clock Derivatives (idTA), extending TA with rate constraints to model independent clock evolution. We also introduce \(\textsf {DL}_{\nu }\) , a temporal logic over Multi-Timed Labeled Transition Systems (MLTS), capturing properties of systems with unsynchronized clocks. We show that model checking for \(\textsf {DL}_{\nu }\) is EXPTIME-complete. Finally, we present MIMETIC, a model checking tool supporting idTA and \(\textsf {DL}_{\nu }\) , providing a platform for analyzing clock interactions and verification of Distributed Real-time Systems (DRTS).