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.

翻译：交替时间自动机（ATA）是时间自动机的扩展，在补运算下封闭，因此适用于逻辑到自动机的转换。包括度量时序逻辑（MTL）在内的多种时序逻辑可被转换为等价的单时钟ATA（1-ATA）。MTL公式的可满足性问题可归约为1-ATA的空性检验。通过简单修改1-ATA空性算法，可将其应用于针对1-ATA规约的时间自动机模型检验。然而，现有的1-ATA空性算法基于扩展区域构造实现，不适用于实际部署。本文旨在开创性地研究直接面向1-ATA的基于区域的方法。我们首先在1-ATA语法中引入时钟停用操作，允许在转移中显式停用时钟。利用该操作，我们改进了现有的MTL到1-ATA转换方法，并提出了一个MTL片段，其对应的1-ATA仅生成有限数量的变量。其次，我们发展了1-ATA的区域概念，提出了一种通过探索对应区域图实现空性检验的算法。为确保算法终止，需要特殊的区域间蕴涵关系检验。我们的主要技术贡献包括：（1）使用简单区域操作实现蕴涵检验的算法；（2）证明一般情况下蕴涵检验具有NP难度。最后，我们将该方法适配于针对1-ATA规约的时间自动机模型检验问题。我们发现当时间自动机具有强非Zeno特性，或当1-ATA生成有限数量变量时，可采用具有二次复杂度的改进型蕴涵检验。