Reachability relations of timed pushdown automata

TL;DR

This paper demonstrates that reachability relations in timed pushdown automata can be expressed in linear arithmetic, enabling more effective analysis of their behavior by combining recursion and timing constraints.

Contribution

The paper introduces a novel quantifier elimination technique for clock constraints and applies Parikh's theorem to characterize reachability in TPDA.

Findings

Reachability relations are expressible in linear arithmetic.

Quantifier elimination simplifies TPDA transition syntax.

Clock difference relations effectively capture fractional clock behaviors.

Abstract

Timed pushdown automata (TPDA) are an expressive formalism combining recursion with a rich logic of timing constraints. We prove that reachability relations of TPDA are expressible in linear arithmetic, a rich logic generalising Presburger arithmetic and rational arithmetic. The main technical ingredients are a novel quantifier elimination result for clock constraints (used to simplify the syntax of TPDA transitions), the use of clock difference relations to express reachability relations of the fractional clock values, and an application of Parikh's theorem to reconstruct the integral clock values.