Model-checking real-time systems: revisiting the alternating automaton route

TL;DR

This paper revisits the automaton-based approach to model-checking real-time systems by developing zone-based methods for alternating timed automata, improving efficiency and applicability for certain logical fragments.

Contribution

It introduces a zone-based emptiness algorithm for 1-clock alternating timed automata, including a deactivation operation and bounded variable generation for specific MTL fragments.

Findings

Developed a zone graph exploration method for 1-ATA emptiness checking.

Proposed an entailment check algorithm with quadratic complexity under certain conditions.

Established NP-hardness of the general entailment check.

Abstract

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. A straightforward modification of the 1-ATA emptiness algorithm can be applied 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. Our goal in this work is to initiate the study of zone-based methods directly for 1-ATAs. We first introduce a deactivation operation on the 1-ATA syntax to allow 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 NP-hardness for the entailment check in the general case. Finally, we adapt our methods to the problem of model-checking timed automata models against 1-ATA specifications. We observe that when the timed automaton is strongly non-Zeno or when the 1-ATA generates a bounded number of variables, a modified entailment check with quadratic complexity can be applied.