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.
|
PDF
Ho Revisiting Timed Logics with Automata Modalities.pdf - Accepted Version 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.
Item Type: | Book Section |
---|---|
Additional Information: | ISSN: 2168-4081 |
Identification Number: | https://doi.org/10.1145/3302504.3311818 |
Page Range: | 67-76 |
SWORD Depositor: | Symplectic Elements |
Depositing User: | Symplectic Elements |
Date Deposited: | 29 Nov 2019 14:59 |
Last Modified: | 17 Mar 2021 14:30 |
URI: | https://shura.shu.ac.uk/id/eprint/25238 |
Actions (login required)
View Item |
Downloads
Downloads per month over past year