传递混合线性关系的$ω$ -链的存在性及其应用
The Existence of $ω$-Chains for Transitive Mixed Linear Relations and Its Applications
摘要：
证明了传递混合线性关系是否有$ω$ -链是可判定的。利用这一结果，我们在一个统一的框架内研究了一些广义时间自动机的活性验证问题。更确切地说，我们证明了（1）具有密集时钟，反向有界计数器和自由计数器的时间自动机的混合线性活性问题是可判定的，以及（2）具有离散时钟，反向有界计数器和下推堆栈的时间自动机的Presburger活性问题是可判定的。
英文摘要：
We show that it is decidable whether a transitive mixed linear relation has an $ω$-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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
