S Akshay ; Paul Gastin ; R Govind ; B Srivathsan - Simulations for Event-Clock Automata

lmcs:10408 - Logical Methods in Computer Science, July 2, 2024, Volume 20, Issue 3 - https://doi.org/10.46298/lmcs-20(3:2)2024
Simulations for Event-Clock AutomataArticle

Authors: S Akshay ; Paul Gastin ; R Govind ; B Srivathsan

    Event-clock automata (ECA) are a well-known semantic subclass of timed automata (TA) which enjoy admirable theoretical properties, e.g., determinizability, and are practically useful to capture timed specifications. However, unlike for timed automata, there exist no implementations for checking non-emptiness of event-clock automata. As ECAs contain special prophecy clocks that guess and maintain the time to the next occurrence of specific events, they cannot be seen as a syntactic subclass of TA. Therefore, implementations for TA cannot be directly used for ECAs, and moreover the translation of an ECA to a semantically equivalent TA is expensive. Another reason for the lack of ECA implementations is the difficulty in adapting zone-based algorithms, critical in the timed automata setting, to the event-clock automata setting. This difficulty was studied by Geeraerts et al. in 2011, where the authors proposed a zone enumeration procedure that uses zone extrapolations for finiteness. In this article, we propose a different zone-based algorithm to solve the reachability problem for event-clock automata, using simulations for finiteness. A surprising consequence of our result is that for event-predicting automata, the subclass of event-clock automata that only use prophecy clocks, we obtain finiteness even without any simulations. For general event-clock automata, our new algorithm exploits the G-simulation framework, which is the coarsest known simulation relation in timed automata literature, and has been recently used for advances in other extensions of timed automata.


    Volume: Volume 20, Issue 3
    Published on: July 2, 2024
    Accepted on: March 20, 2024
    Submitted on: December 1, 2022
    Keywords: Computer Science - Formal Languages and Automata Theory
    Funding:
      Source : OpenAIRE Graph
    • Efficient Techniques and Tools for Verification and Synthesis of Real-Time Systems; Funder: French National Research Agency (ANR); Code: ANR-18-CE40-0015

    Consultation statistics

    This page has been seen 1161 times.
    This article's PDF has been downloaded 559 times.