Reachability relations of timed pushdown automata (Q2221811): Difference between revisions

The timed automata (TA) of [\textit{R. Alur} and \textit{D. L. Dill}, Theor. Comput. Sci. 126, No. 2, 183--235 (1994; Zbl 0803.68071)] are a seminal contribution to real-time systems modeling. These automata extend classical finite-state automata with finitely many real-time clocks that can be reset and compared under inequalities by the transitions. These automata hence allow to reason about system execution under timing constraints and are commonly used as the underlying model in formal verification tools for real-time systems. However, finite automata have well-known limitations as to the kind of behavior they can represent. It is hence of paramount importance to investigate to which extent more expressive models can also be amenable to computational processing. This paper studies such an extension, namely timed pushdown automata (TPDA). This model extends usual finite-state pushdown automata with a finite number of control and stack real-valued clocks. TPDA transitions furthermore allow to increase all clocks by the same elapse time, read an input letter, test control clock constraints, reset some control clocks, and push/pop a stack symbol on/from the stack under constraints over control and stack clocks. In this last case, a (stack) symbol and fresh copies of the stack clocks are pushed/popped on/from the stack. These automata hence allow to reason about timing constraints between push and pop operations and are therefore appropriate to study timing constraints in recursive behavior. In a TPDA clock values are also always nondeterministically chosen in order to fulfill clock constraints. TPDA use comparisons of the form \(\geq k\) and \(\equiv_m k\) (congruence modulo \(m\)) for integers \(k\) and positive integers \(m\). Here, two reals are congruent modulo \(m\) when their difference is an integer multiple of \(m\). Furthermore, the values compared in a TPDA are clock values, their integer or fractional parts (the value minus its integer part), or difference of clock values, integer or fractional parts. Finally, TPDA use Boolean combinations of such constraints. A fundamental question in system verification is to determine whether two system states can be reached by an execution path. In this paper, the authors show that for TPDA this reachability relation is expressible by an existential formula of linear arithmetic (of doubly exponential size). In this context, linear arithmetic is the theory of \[ (\mathbb{R};+,\leq,\lfloor -\rfloor,\{-\},k\cdot -,\equiv_m,0,1;k\in \mathbb{Z},m \in \mathbb{N}\setminus\{0\}) \] where \(\lfloor -\rfloor\) is the integer operator and \(\{-\}\) is the fractional part operator. This structure generalizes both Presburger arithmetic \((\mathbb{Z},\leq,\equiv_m,+,0;m \in \mathbb{N}\setminus\{0\})\) and rational arithmetic \((\mathbb{R},\leq,+,0)\). More precisely, the authors show that for a TPDA with states \(p\) and \(q\) there is an existential formula of linear arithmetic such that there exists a sequence of transitions \(w\) from \(p\) (with empty stack) to \(q\) (with empty stack) exactly when this formula is satisfied by initial and final clock values, and the number of times each transition in \(w\) is used. In order to prove this result, the paper introduces a novel quantifier elimination procedure for linear arithmetic.