The Existence of $ω$-Chains for Transitive Mixed Linear Relations and Its Applications
| dc.creator | Dang, Zhe | |
| dc.creator | Ibarra, Oscar | |
| dc.date | 2001-10-31 | |
| dc.date | 2005-04-29 | |
| dc.date.accessioned | 2026-07-07T03:17:52Z | |
| dc.date.available | 2026-07-07T03:17:52Z | |
| dc.description | 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. | |
| dc.description | 26 pages | |
| dc.identifier | https://arxiv.org/abs/cs/0110063 | |
| dc.identifier | http://arxiv.org/abs/cs/0110063 | |
| dc.identifier.uri | http://salesiana.dossiersoluciones.com/handle/123456789/30885 | |
| dc.subject | Logic in Computer Science | |
| dc.subject | D.2.4; F.1.1 | |
| dc.title | The Existence of $ω$-Chains for Transitive Mixed Linear Relations and Its Applications | |
| dc.type | text |