Binary reachability of timed pushdown automata via quantifier elimination and cyclic order atoms

TL;DR

This paper demonstrates that the binary reachability relation of extended timed pushdown automata can be effectively expressed using hybrid linear arithmetic and cyclic order atoms, enabling new analysis techniques.

Contribution

It introduces a method to express binary reachability of timed pushdown automata with modular and fractional clocks using quantifier elimination and cyclic order atoms.

Findings

Binary reachability is expressible in hybrid linear arithmetic.

The approach subsumes previous results for untimed and finite automata.

Reduction to register pushdown automata over cyclic order atoms is achieved.

Abstract

We study an expressive model of timed pushdown automata extended with modular and fractional clock constraints. We show that the binary reachability relation is effectively expressible in hybrid linear arithmetic with a rational and an integer sort. This subsumes analogous expressibility results previously known for finite and pushdown timed automata with untimed stack. As key technical tools, we use quantifier elimination for a fragment of hybrid linear arithmetic and for cyclic order atoms, and a reduction to register pushdown automata over cyclic order atoms.