HO, HM (2019). Revisiting timed logics with automata modalities. In: HSCC '19 Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. ACM Press, 67-76. [Book Section]
Documents
25238:539762
PDF
Ho Revisiting Timed Logics with Automata Modalities.pdf - Accepted Version
Available under License All rights reserved.
Ho Revisiting Timed Logics with Automata Modalities.pdf - Accepted Version
Available under License All rights reserved.
Download (912kB) | Preview
Abstract
© 2019 ACM. It is well known that (timed) ω-regular properties such as 'p holds at every even position' and 'p occurs at least three times within the next 10 time units' cannot be expressed in Metric Interval Temporal Logic (MITL) and Event Clock Logic (ECL). A standard remedy to this deficiency is to extend these with modalities defined in terms of automata. In this paper, we show that the logics EMITL0, ∞ (adding non-deterministic finite automata modalities into the fragment of MITL with only lower- and upper-bound constraints) and EECL (adding automata modalities into ECL) are already as expressive as EMITL (full MITL with automata modalities). In particular, the satisfiability and model-checking problems for EMITL0, ∞ and EECL are PSPACE-complete, whereas the same problems for EMITL are EXPSPACE-complete. We also provide a simple translation from EMITL0, ∞ to diagonal-free timed automata, which enables practical satisfiability and model checking based on off-the-shelf tools.
More Information
Statistics
Downloads
Downloads per month over past year
Metrics
Altmetric Badge
Dimensions Badge
Share
Actions (login required)
View Item |