Model-Checking Real-Time Systems: Revisiting the Alternating Automaton Route
摘要
Alternating timed automata (ATA) are an extension of timed automata, that are closed under complementation and hence amenable to logic-to-automata translations. Several timed logics, including Metric Temporal Logic (MTL), can be converted to equivalent 1-clock ATAs (1-ATAs). Satisfiability of an MTL formula reduces to checking emptiness of a 1-ATA. Furthermore, algorithms for 1-ATA emptiness can be adapted for model-checking timed automata models against 1-ATA specifications. However, existing emptiness algorithms for 1-ATA proceed by an extended region construction, and are not suitable for implementations. In this work, we initiate the study of zone-based methods for 1-ATAs. The challenge here, as opposed to timed automata, is the fact that the zone graph may generate an unbounded number of variables. We first introduce a deactivation operation to the 1-ATA syntax that allows for an explicit deactivation of the clock in transitions. Using the deactivation operation, we improve the existing MTL-to-1-ATA conversion and present a fragment of MTL for which the equivalent 1-ATA generate a bounded number of variables. Secondly, we develop the idea of zones for 1-ATA and present an emptiness algorithm which explores a corresponding zone graph. For termination, a special entailment check between zones is necessary. Our main technical contributions are: (1) an algorithm for the entailment check using simple zone operations and (2) an \(\textsf{NP}\) -hardness for the entailment check in the general case. Finally, for 1-ATA which generate a bounded number of variables, we present a modified entailment check with quadratic complexity.