Alternating timed automata (ATA) are an extension of timed automata where the effect of each transition is described by a positive boolean combination of (state-reset) pairs. Unlike classical timed automata, ATAs are closed under complementation and are therefore amenable to logic-to-automata translations. Several timed logics, including Metric Temporal Logic (MTL), can be converted to equivalent 1-clock ATA (1-ATAs). But currently, tools for model checking timed systems don't use 1-ATAs directly in computation, and instead use sophisticated conversions to timed automata instead. A reason for this could be that zone-based methods don't exist for 1-ATAs, unlike those extensively studied for TAs.
Our goal is to initiate the study of zone-based algorithms directly for 1-ATAs. We first introduce a deactivation operator to the 1-ATA syntax, and using it define the class of bounded 1-ATAs. We then define a zone-based emptiness algorithm for 1-ATAs, and look closely at the entailment relation that guarantees the termination of this algorithm.
This is a joint work with B. Srivathsan and Patricia Bouyer that was accepted at FoSSaCS 2025.