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.

[img]
Preview
PDF
Ho Revisiting Timed Logics with Automata Modalities.pdf - Accepted Version
All rights reserved.

Download (912kB) | Preview
Official URL: https://dl.acm.org/citation.cfm?id=3302504.3311818
Link to published version:: https://doi.org/10.1145/3302504.3311818
Related URLs:

    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
    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: 29 Nov 2019 15:00
    URI: http://shura.shu.ac.uk/id/eprint/25238

    Actions (login required)

    View Item View Item

    Downloads

    Downloads per month over past year

    View more statistics