Mightyl: A compositional translation from mitl to timed automata

BRIHAYE, T, GEERAERTS, G, HO, Hsi-Ming and MONMEGE, B (2017). Mightyl: A compositional translation from mitl to timed automata. Computer Aided Verification 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part I, 10426, 421-440.

Ho_MightyL_A_Compositional(AM).pdf - Accepted Version
All rights reserved.

Download (632kB) | Preview
Official URL: https://link.springer.com/chapter/10.1007/978-3-31...
Open Access URL: https://hal.archives-ouvertes.fr/hal-01525524 (Accepted version)
Link to published version:: https://doi.org/10.1007/978-3-319-63387-9_21
Related URLs:


    Metric Interval Temporal Logic (MITL) was first proposed in the early 1990s as a specification formalism for real-time systems. Apart from its appealing intuitive syntax, there are also theoretical evidences that make MITL a prime real-time counterpart of Linear Temporal Logic (LTL). Unfortunately, the tool support for MITL verification is still lacking to this day. In this paper, we propose a new construction from MITL to timed automata via very-weak one-clock alternating timed automata. Our construction subsumes the well-known construction from LTL to Büchi automata by Gastin and Oddoux and yet has the additional benefits of being compositional and integrating easily with existing tools. We implement the construction in our new tool MightyL and report on experiments using Uppaal and LTSmin as back-ends.

    Item Type: Article
    Uncontrolled Keywords: 08 Information and Computing Sciences; Artificial Intelligence & Image Processing
    Identification Number: https://doi.org/10.1007/978-3-319-63387-9_21
    Page Range: 421-440
    SWORD Depositor: Symplectic Elements
    Depositing User: Symplectic Elements
    Date Deposited: 05 Feb 2020 11:09
    Last Modified: 18 Mar 2021 02:38
    URI: https://shura.shu.ac.uk/id/eprint/25237

    Actions (login required)

    View Item View Item


    Downloads per month over past year

    View more statistics