Showing cs.LOShow all
2 papers · 1 filter
cs.LO2001
Pushdown Timed Automata: a Binary Reachability Characterization and Safety Verification
Zhe Dang
We consider pushdown timed automata (PTAs) that are timed automata (with dense clocks) augmented with a pushdown stack. A configuration of a PTA includes a control state, dense clo…
cs.LO2001
The Existence of -Chains for Transitive Mixed Linear Relations and Its Applications
Zhe Dang, Oscar Ibarra
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 tim…