Computing the binary reachability relation of Timed Pushdown Automata

The reachability problem asks, for a fixed initial and final configuration, whether there is a run of the system going from the former to the latter. The binary reachability problem generalises the reachability problem: The aim now is to logically characterise the set of *all pairs* of such initial and final configurations (not just for fixed two of them).

 

Timed pushdown automata (TPDA) are an expressive model extending pushdown automata with timing information (clocks), both in the control locations and in the stack.

We show that the binary reachability relation for TPDA can effectively be expressed in the hybrid logic (Z, ≤, ≡, +, 0, 1) ∪ (Q, ≤, +, 0), i.e., consisting of Presburger arithmetic (integer values) and linear arithmetic (fractional values).

This result generalises known characterisations for timed automata [1, 2] and pushdown timed automata (untimed stack) [3]. The generalisation is strict w.r.t. [3] since in our TPDA model the stack cannot be untimed.

 

This is joint work with Sławek Lasota (a.k.a. SL in connection with semilinear sets).

 

REFERENCES

 

[1] "Timed Automata and the Theory of Real Numbers", Comon, Jurski, CONCUR'99.

[2] "Revisiting reachability in timed automata", Quaas, Shirmohammadi, Worrell, LICS'17.

[3] "Pushdown timed automata: a binary reachability characterization and safety verification", Dang, TCS'03.