Timed pushdown automata and branching vector addition systems

computational complexity decidability pushdown automata reachability analysis vectors addition operation automata nonemptiness decidability dense-timed pushdown automata doubly exponential time intersection operation least solutions non-emptiness one-dimensional branching vector addition systems orbit-finite timed register pushdown automata reachability union operation Automata Clocks Handheld computers Mathematical model Orbits Registers Upper bound