Simulations for Event-Clock Automata

TL;DR

The paper addresses reachability for event-clock automata (ECA), where prophecy clocks complicate standard zone-based analysis. It extends the TA-based zone approach by adopting a G-simulation framework tailored to ECAs, introducing event-zones and distance-graph representations that handle undefined values via $+\infty$ and $-\infty$. The authors define a concrete, algorithmic $\mathcal{G}$-based simulation $\preceq_{\mathcal{A}}$ for ECAs and prove its finiteness on reachable zones, ensuring termination of a finite-zone enumeration that remains sound and complete for reachability. A key insight is a prophecy-clock invariant that constrains the structure of reachable zones, enabling a finite index $\sim_{M}$ to bound the combinatorics of valuations. Collectively, this yields a practical, TA-compatible reachability procedure for ECAs (and EPA in particular) with potential implementation in tools like TChecker, bridging theory and tooling for real-time specification formalisms.

Abstract

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.

Figures (11)

• Figure 1: Valuation of event-clocks.
• Figure 2: Representation of valuations in event-clock automata. Here, $v' = v+ \delta$.
• Figure 3: The event-clock automaton $\mathcal{A}_1$ recognizes the language $\{b^n a \mid n \ge 1 \}$ such that there exists some $b$ which occurs exactly one time unit before $a$. Its event-zone graph is on the left.
• Figure 4: An example of a distance graph for timed automata with clocks $x, y$. The dotted edge in black denotes that the edge is obtained by canonicalization, and the dotted edge in red depicts an edge introduced by a guard.
• Figure 5: Distance graph with standardization using the extended algebra. Note that the green edges are the edges induced by standardization.

Theorems & Definitions (73)

• Definition 2.1: Valuation
• Remark 2.2
• Definition 2.3: Event-clock automata AlurFH99
• Remark 2.4
• Definition 2.5: Reachability problem for ECA
• Definition 3.1: Weights
• Remark 3.2
• Definition 3.3
• Remark 3.4
• Definition 3.5: Event-zones