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 DL_ν, a temporal logic over Multi-Timed Labeled Transition Systems (MLTS), capturing properties of systems with unsynchronized clocks. We show that model checking for DL_ν is EXPTIME-complete. Finally, we present MIMETIC, a model checking tool supporting idTA and DL_ν, providing a platform for analyzing clock interactions and verification of Distributed Real-time Systems (DRTS).