Simulations for Event-Clock Automata
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2022
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866929449918791680 |
|---|---|
| author | Akshay, S Gastin, Paul Govind, R Srivathsan, B |
| author_facet | Akshay, S Gastin, Paul Govind, R Srivathsan, B |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2207_02633 |
| institution | arXiv |
| publishDate | 2022 |
| record_format | arxiv |
| spellingShingle | Simulations for Event-Clock Automata Akshay, S Gastin, Paul Govind, R Srivathsan, B Formal Languages and Automata Theory 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. |
| title | Simulations for Event-Clock Automata |
| topic | Formal Languages and Automata Theory |
| url | https://arxiv.org/abs/2207.02633 |