Revisiting timed logics with automata modalities

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.

Preview

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

Publication Metrics