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).

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Extending Timed Automata with Clock Derivatives

  • David Cortés,
  • Jean Leneutre,
  • Vadim Malvone,
  • James Ortiz,
  • Pierre-Yves Schobbens

摘要

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).