The Existence of $\omega$-Chains for Transitive Mixed Linear Relations and Its Applications
<|reference_start|>The Existence of $\omega$-Chains for Transitive Mixed Linear Relations and Its Applications: 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.<|reference_end|>
@article{dang2001the,
    title={The Existence of $\omega$-Chains for Transitive Mixed Linear Relations
  and Its Applications},
    author={Zhe Dang and Oscar Ibarra},
    journal={arXiv preprint arXiv:cs/0110063},
    year={2001},
    archivePrefix={arXiv},
    eprint={cs/0110063},
    primaryClass={cs.LO}
}