The Existence of $\omega$-Chains for Transitive Mixed Linear Relations and Its Applications

TL;DR

This paper proves the decidability of the existence of infinite chains in transitive mixed linear relations and applies this to solve various liveness verification problems in generalized timed automata.

Contribution

It introduces a decision procedure for $\omega$-chains in transitive mixed linear relations and applies it to establish decidability of several complex liveness problems in timed automata.

Findings

Decidability of $\omega$-chains in transitive mixed linear relations.

Decidability of mixed linear liveness problems in timed automata.

Decidability of Presburger liveness problems in timed automata.

Abstract

We show that it is decidable whether a transitive mixed linear relation has an $\omega$-chain. Using this result, we study a number of liveness verification problems for generalized timed automata within a unified framework. More precisely, we prove that (1) the mixed linear liveness problem for a timed automaton with dense clocks, reversal-bounded counters, and a free counter is decidable, and (2) the Presburger liveness problem for a timed automaton with discrete clocks, reversal-bounded counters, and a pushdown stack is decidable.