University of Warsaw<EMAIL_ADDRESS>https://orcid.org/0000-0003-0578-9103 Partially supported by Polish NCN grant
2017/26/D/ST6/00201. University of Warsaw<EMAIL_ADDRESS>https://orcid.org/0000-0001-8674-4470 Partially supported by Polish NCN grant
2016/21/B/ST6/01505. Lorenzo Clemente and Sławomir Lasota

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

Lorenzo Clemente  and  Sławomir Lasota

###### 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.

###### Key words and phrases:

timed automata, reachability relation, timed pushdown automata, linear
arithmetic

###### 1991 Mathematics Subject Classification:

F.1.1 Models of Computation, F.4.1 Mathematical Logic

##  1\. Introduction

Timed automata (ta) are one of the most studied models of reactive timed
systems. The fundamental result that paved the way to automatic verification
of timed systems is decidability (and PSPACE-completeness) of the reachability
problem for ta [2]. However, in certain applications, such as in parametric
verification, deciding reachability is insufficient, and one needs to
construct the more general _binary reachability relation_ , i.e., the entire
(possibly infinite) set of of pairs of configurations $(c_{i},c_{f})$ s.t.
there is an execution from $c_{i}$ to $c_{f}$. The reachability relation for
ta has been shown to be effectively expressible in hybrid linear arithmetic
with rational and integer sorts [11, 14, 16, 19]. Since hybrid logic is
decidable, this yields an alternative proof of decidability of the
reachability problem.

In this paper, we compute the reachability relation for timed automata
extended with a stack. An early model of _pushdown timed automata_ (ptda)
extending ta with a (classical, untimed) stack has been considered by
Bouajjani _et al._ [5]. More recently, _dense-timed pushdown automata_ (dtpda)
have been proposed by Abdulla _et al._ [1] as an extension of ptda. In dtpda,
stack symbols are equipped with rational _ages_ , which initially are $0$ and
increase with the elapse of time at the same rate as global clocks; when a
symbol is popped, its age is tested for membership in an interval. While dtpda
syntactically extend ptda by considering a timed stack, timed constraints can
in fact be removed while preserving the timed language recognised by the
dtpda, and thus they semantically collapse to ptda [9]. This motivates the
quest for a strictly more expressive generalisation of ptda and dtpda with a
truly timed stack. It has been observed in [22] that adding fractional stack
constraints prevents the stack from being untimed, and thus strictly enriches
the expressive power111For ta, fractional constraints can be handled by the
original region construction and do not make the model harder to analyse [2].
.

We embrace this observation and propose the model of _timed pushdown automata_
(tpda), which extends timed automata with a timed stack and integer,
fractional, and modulo diagonal/non-diagonal constraints. The model features
local clocks and stack clocks. As time elapses, all clocks increase their
values, and they do so at the same rate. Local clocks can be reset and
compared according to the generalised constraints above. At the time of a push
operation, new stack clocks are created whose values are initialised, possibly
non-deterministically, as to satisfy a given push constraint between stack
clocks and local clocks; similarly, a pop operation requires that stack clocks
to be popped satisfy a given pop constraint of analogous form. Stack push/pop
constraints are also of the form of diagonal/non-diagonal integer, modulo, and
fractional constraints.

##### Contributions.

We compute the _binary reachability relation_ of tpda, i.e., the family of
binary relations $\left\\{\stackrel{{\scriptstyle}}{{\leadsto}}_{\ell
r}\right\\}\subseteq\mathbb{Q}_{\geq 0}^{X}\times\mathbb{Q}_{\geq 0}^{X}$ for
control locations $\ell,r$ s.t. from the initial clock valuation
$\mu\in\mathbb{Q}_{\geq 0}^{X}$ and control location $\ell$ we can reach the
final clock valuation $\nu\in\mathbb{Q}_{\geq 0}^{X}$ and control location
$r$, written $\mu\stackrel{{\scriptstyle}}{{\leadsto}}_{\ell r}\nu$. The stack
is empty at the beginning and at the end of the computation. The main
contribution of the paper is the effective computation of the tpda
reachability relation in the existential fragment of _linear arithmetic_
$\mathcal{L}_{\mathbb{Z},\mathbb{Q}}$, a two-sorted logic combining Presburger
arithmetic $(\mathbb{Z},\leq,(\equiv_{m})_{m\in\mathbb{N}},+,0)$ and linear
rational arithmetic $(\mathbb{Q},\leq,+,0)$. As a byproduct of our
constructions, we actually characterise the more general _ternary reachability
relation_ $\mu\stackrel{{\scriptstyle\pi}}{{\leadsto}}_{\ell r}\nu$, where
$\mu,\nu$ are as above and $\pi:\mathbb{N}^{\Sigma}$ additionally counts the
number of occurrences of input letters over a finite alphabet $\Sigma$, i.e.,
the Parikh image of the run. To our knowledge, the ternary reachability
relation was not previously considered. As an application of ternary
reachability, we can model, for instance, letter counts of initial and final,
possibly non-empty, stack contents. Thus, ternary reachability is an
expressive extension of binary reachability.

The computation of the ternary reachability relation is achieved by two
consecutive translations. First, we transform a tpda into a _fractional tpda_,
which uses only fractional constraints. In this step we exploit _quantifier
elimination_ for a fragment of linear arithmetic corresponding to clock
constraints. Quantifier elimination is a pivotal tool in this work, and to our
knowledge its use in the study of timed models is novel. The final integer
value of clocks is reconstructed by letting the automaton input special tick
symbol $\checkmark_{\\!\\!x}$ every time clock $x$ reaches an integer value
(provided it is not reset anymore later); it is here that ternary reachability
is more suitable than binary reachability.

Secondly, a fractional tpda is transformed into a pda with registers (rpda)
over the so called _cyclic order atoms_ $(\mathbb{Q}\cap[0,1),K)$ [8], where
$K$ is the ternary cyclic order relation

$\displaystyle K(a,b,c)\equiv a<b<c\vee b<c<a\vee c<a<b,\qquad\textrm{ for
}a,b,c\in\mathbb{Q}\cap[0,1).$ (1)

In other words, $K(a,b,c)$ holds if, distributing $a,b,c$ on the unit circle
and going clockwise from $a$, then we fist visit $b$ and afterwards $c$. Since
fractional values are wrapped around $0$ when time increases, $K$ is invariant
under time elapse. We use registers to store the fractional parts of absolute
times of last clock resets; fractional constraints on clocks are simulated by
constraints on registers using $K$. In order to compute the reachability
relation for rpda we use again quantifier elimination, this time over cyclic
order atoms. The latter property holds since cyclic order atoms constitute a
homogeneous structure [17]. Therefore, another contribution of this work is
the solution of a nontrivial problem such as computing the reachability
relation for tpda, which is a clock model, as an application of rpda, which is
a register model. The analysis of rpda is substantially easier than a direct
analysis of (fractional) tpda.

From the complexity standpoint, the formula characterising the reachability
relation of a tpda is computable in double exponential time. However, when
cast down to ta or tpda with timeless stack (which subsume ptda and, a
posteriori, dtpda), the complexity drops to singly exponential, matching the
previously known complexity for ta [19]. For ptda, no complexity was
previously given in [12], and thus the result is new. For tpda, the binary
reachability problem has not been studied before. Since the existential
fragment of $\mathcal{L}_{\mathbb{Z},\mathbb{Q}}$ is decidable in NP (because
so is existential linear rational arithmetic [20] and existential Presburger
arithmetic [24]), we can solve the reachability problem of tpda in 2NEXP by
reduction to satisfiability for $\mathcal{L}_{\mathbb{Z},\mathbb{Q}}$. Since
our constructions preserve the languages of all the models involved, untimed
tpda languages are context-free.

##### Discussion.

From a syntactic point of view, tpda significantly lifts the restrictions of
dtpda—which allow only classical non-diagonal constraints, i.e., interval
tests, and thus has neither diagonal, nor modulo, nor fractional
constraints—and of the model of [22]—which additionally allows diagonal/non-
diagonal fractional tests, and thus does not have modulo constraints. Since
classical diagonal constraints reduce to classical non-diagonal constraints,
and, _in the presence of fractional constraints_ , integer and modulo
constraints can be removed altogether (cf. Sec. 4), tpda are expressively
equivalent to [22]. However, while [22] solves the control state reachability
problem, we solve the more general problem of computing the binary
reachability relation. Our reduction technique not only preserves
reachability, like [22], but additionally enables the reconstruction of the
reachability relation.

Our expressivity result generalises analogous results for ta [11, 14, 16, 19]
and ptda [12]. The proof of [11] for ta has high technical difficulty and does
not yield complexity bounds. The proof of [14] for ta uses an automata
representation for sets of clock valuations; the idea of _reset-point
semantics_ employed in [14] is analogous to using registers instead of clocks.
The paper [16] elegantly expresses the reachability relation for ta with
_clock difference relations_ (CDR) over the fractional values of clocks. It is
remarkable that the formulas expressing the reachability relations that we
obtain are of the same shape as CDR. The recent paper [19] shows that the ta
binary reachability relation can be expressed in the same fragment of hybrid
linear arithmetic that we use for tpda, which we find very intriguing. Their
proof converts the integer value of clocks into counters, and then observes
that, thanks to the specific reset policy of clocks, these counter machines
have a semilinear reachability relation; the latter is proved by encoding the
value of counters into the language. In our proof, we bring the encoding of
the integer value of clocks into the language to the forefront, via the
introduction of the ternary reachability relation. The proof of [12] for ptda
also separates clocks into their integer and fractional part. It is not clear
how any of the previous approaches could handle a timed stack.

Another approach for computing the reachability relation for tpda would be to
reduce it directly to a more expressive register model, such as _timed
register pushdown automata_ (trpda) [9, 10], which considers both integer
$(\mathbb{Z},\leq,+1)$ and rational registers $(\mathbb{Q}_{\geq 0},\leq)$.
While such a reduction for the reachability problem is possible since (the
integer part of) large clock values can be “forgotten”, e.g., along the lines
of [9], this does not hold anymore if we want to preserve the reachability
relation. For this reason, in the present work we first remove the integer
part of clocks (by encoding it in the untimed language) and then we reduce to
rpda, which have only fractional registers and no integer register, and are
thus easier to analyse than trpda 222trpda are more general than rpda—cyclic
order atoms can be interpreted into $(\mathbb{Q}_{\geq 0},\leq)$. The binary
reachability relation for trpda can be computed by refining the reductions of
[10] used for deciding the reachability problem. However, we do not know how
to use the reachability relation of trpda to compute that of tpda. . The
method of quantifier elimination was recently applied to the analysis of
another timed model, namely _timed communicating automata_ [7].

Finally, another expressive extension of ta, called _recursive timed automata_
(rta), has been proposed [21, 3]. rta use a timed stack to store the current
clock valuation, which does not evolve as time elapses and can be restored at
the time of pop. This facility makes rta expressively incomparable to all
models previously mentioned.

##### Notations.

Let $\mathbb{Q}$, $\mathbb{Q}_{\geq 0}$, $\mathbb{Z}$, and $\mathbb{N}$ denote
the rationals, the non-negative rationals, the integers, and the natural
numbers; let $\mathbb{I}=\mathbb{Q}_{\geq 0}\cap[0,1)$ be the unit rational
interval. Let $\equiv_{m}$ denote the congruence modulo
$m\in\mathbb{N}\setminus\left\\{0\right\\}$ in $\mathbb{Z}$. For
$a\in\mathbb{Q}$, let $\lfloor a\rfloor\in\mathbb{Z}$ denote the largest
integer $k$ s.t. $k\leq a$, and let $\left\\{a\right\\}=a-\lfloor a\rfloor$
denote its fractional part. Let $\mathbbm{1}_{C?}$, for a condition $C$, be
$1$ if $C$ holds, and $0$ otherwise.

##  2\. Linear arithmetic and quantifier elimination

Consider the two-sorted structure ${\cal A}={\cal A}_{\mathbb{Z}}\uplus{\cal
A}_{\mathbb{Q}}$, where ${\cal
A}_{\mathbb{Z}}=(\mathbb{Z},\leq,(\equiv_{m})_{m\in\mathbb{N}},+,(k)_{k\in\mathbb{Z}})$
and ${\cal A}_{\mathbb{Q}}=(\mathbb{Q},\leq,+,(k)_{k\in\mathbb{Q}})$. We
consider “$+$” as a binary function, and we have a constant $k$ for every
integer/rational number. By _linear arithmetic_ , denoted
$\mathcal{L}_{\mathbb{Z},\mathbb{Q}}$, we mean the two-sorted first-order
language in the vocabulary of ${\cal A}$. Restriction to the integer sort
yields Presburger arithmetic $\mathcal{L}_{\mathbb{Z}}$ (_integer formulas_),
and restriction to the rational sort yields linear rational arithmetic
$\mathcal{L}_{\mathbb{Q}}$ (_rational formulas_). We assume constants are
encoded in binary.

Two formulas are _equivalent_ if they are satisfied by the same valuations. It
is well-known that the theories of ${\cal A}_{\mathbb{Z}}$ [18] and ${\cal
A}_{\mathbb{Q}}$ [15] admit effective elimination of quantifiers: Every
formula can effectively be transformed in an equivalent quantifier-free one.
Therefore, the theory of ${\cal A}$ also admits quantifier elimination, by the
virtue of the following general fact (when speaking of a structure admitting
quantifier elimination, we have in mind its theory).

######  Lemma 2.1.

If the structures ${\cal A}_{1}$ and ${\cal A}_{2}$ admit (effective)
elimination of quantifiers, then the two-sorted structure ${\cal
A}_{1}\uplus{\cal A}_{2}$ also does so. For conjunctive formulas, the
complexity is the maximum of the two complexities.

For clock constraints, we will use the first-order language over the two
sorted structure ${\cal A}^{\mathrm{c}}={\cal
A}^{\mathrm{c}}_{\mathbb{N}}\uplus{\cal A}^{\mathrm{c}}_{\mathbb{I}}$, where
the integer sort is restricted to ${\cal
A}^{\mathrm{c}}_{\mathbb{N}}=(\mathbb{N},\leq,(\equiv_{m})_{m\in\mathbb{N}},+1,0)$—the
domain is now $\mathbb{N}$ and full addition “$+$” is replaced by the unary
successor operation “$+1$”)—and the rational sort to ${\cal
A}^{\mathrm{c}}_{\mathbb{I}}=(\mathbb{I},\leq,0)$— the domain is now the unit
interval, there is no addition, and the only constant is $0$. Let
$\mathcal{L}^{\mathrm{c}}_{\mathbb{N},\mathbb{I}}$ be such a sub-logic. (As
syntactic sugar we allow to use addition of arbitrary, even negative, integer
constants in integer formulas, e.g. $x-4\leq y+2$.) As before,
$\mathcal{L}^{\mathrm{c}}_{\mathbb{N}}$ and
$\mathcal{L}^{\mathrm{c}}_{\mathbb{I}}$ are the restrictions to the respective
sorts. All the sub-logics above admit effective elimination of quantifiers.

######  Lemma 2.2.

The structures ${\cal A}^{\mathrm{c}}_{\mathbb{N}}$ and ${\cal
A}^{\mathrm{c}}_{\mathbb{I}}$ admit effective elimination of quantifiers. For
${\cal A}^{\mathrm{c}}_{\mathbb{N}}$ the complexity is singly exponential for
conjunctive formulas, while for ${\cal A}^{\mathrm{c}}_{\mathbb{I}}$ is
quadratic.

Notice that since $\mathcal{L}^{\mathrm{c}}_{\mathbb{N}}$ is a fragment of
Presburger arithmetic $\mathcal{L}_{\mathbb{Z}}$, we could apply the
quantifier elimination for $\mathcal{L}_{\mathbb{Z}}$ to get a quantifier-free
$\mathcal{L}_{\mathbb{Z}}$ formula. Our result is stronger since we get a
quantifier-free formula of the more restrictive fragment
$\mathcal{L}^{\mathrm{c}}_{\mathbb{N}}$.

######  Corollary 2.3.

The structure ${\cal A}^{\mathrm{c}}$ admits effective quantifier elimination.
The complexity is exponential for conjunctive formulas.

##  3\. Timed pushdown automata

##### Clock constraints.

Let $X$ be a finite set of clocks. We consider constraints which can
separately speak about the integer $\lfloor x\rfloor$ and fractional value
$\left\\{x\right\\}$ of a clock $x\in X$. A _clock constraint_ over $X$ is a
boolean combination of _atomic clock constraints_ of one of the forms

(inte ger) (modu lar) (fracti onal) (non-diagonal) $\displaystyle\lfloor
x\rfloor$ $\displaystyle\leq k\ \ $ $\displaystyle\lfloor x\rfloor$
$\displaystyle\equiv_{m}k\ \ $ $\displaystyle\left\\{x\right\\}$
$\displaystyle=0$ (diagonal) $\displaystyle\lfloor x\rfloor-\lfloor y\rfloor$
$\displaystyle\leq k$ $\displaystyle\lfloor x\rfloor-\lfloor y\rfloor$
$\displaystyle\equiv_{m}k$ $\displaystyle\left\\{x\right\\}$
$\displaystyle\leq\left\\{y\right\\}$

where $x,y\in X$, $m\in\mathbb{N}$,a and $k\in\mathbb{Z}$. Since we allow
arbitrary boolean combinations, we consider also the constraint
$\mathbf{true}$, which is always satisfied, and variants with any $\sim\
\in\\{\leq,<,\geq,>\\}$ in place of $\leq$. A _clock valuation_ is a mapping
$\mu\in\mathbb{Q}_{\geq 0}^{X}$ assigning a non-negative rational number to
every clock in $X$; we write $\lfloor\mu\rfloor$ for the valuation in
$\mathbb{N}^{X}$ s.t. $\lfloor\mu\rfloor(x):=\lfloor\mu(x)\rfloor$ and
$\left\\{\mu\right\\}$ for the valuation in $\mathbb{I}^{X}$ s.t.
$\left\\{\mu\right\\}(x):=\left\\{\mu(x)\right\\}$. For a valuation $\mu$ and
a clock constraint $\varphi$ we say that $\mu$ _satisfies_ $\varphi$ if
$\varphi$ is satisfied when integer clock values $\lfloor x\rfloor$ are
evaluated according to $\lfloor\mu\rfloor$ and fractional values
$\left\\{x\right\\}$ according to $\left\\{\mu\right\\}$.

######  Remark 3.1 (Clock constraints as quantifier-free
$\mathcal{L}^{\mathrm{c}}_{\mathbb{N},\mathbb{I}}$ formulas).

Up to syntactic sugar, a clock constraint over clocks
$\\{x_{1},\ldots,x_{n}\\}$ is the same as a quantifier-free
$\mathcal{L}^{\mathrm{c}}_{\mathbb{N},\mathbb{I}}$ formula $\varphi(\lfloor
x_{1}\rfloor,\ldots,\lfloor
x_{n}\rfloor,\left\\{x_{1}\right\\},\ldots,\left\\{x_{n}\right\\})$ over $n$
integer and $n$ rationals variables.

######  Remark 3.2 (Classical clock constraints).

Integer and fractional constraints subsume classical ones. For clocks $x,y$,
since $x=\lfloor x\rfloor+\left\\{x\right\\}$ (and similarly for $y$)333We
often identify a clock $x$ with its value for simplicity of notation.,
$x-y\leq k$ for an integer $k$ is equivalent to $(\lfloor x\rfloor-\lfloor
y\rfloor\leq k\wedge\left\\{x\right\\}\leq\left\\{y\right\\})\vee\lfloor
x\rfloor-\lfloor y\rfloor\leq k-1$, and similarly for $x\leq k$. On the other
hand, the fractional constraint $\left\\{x\right\\}=0$ is not expressible as a
classical constraint.

######  Remark 3.3 ($\lfloor x\rfloor-\lfloor y\rfloor$ versus $\lfloor
x-y\rfloor$).

In the presence of fractional constraints, the expressive power would not
change if, instead of atomic constraints $\lfloor x\rfloor-\lfloor
y\rfloor\equiv_{m}k$ and $\lfloor x\rfloor-\lfloor y\rfloor\leq k$ speaking of
the _difference of the integer parts_ , we would choose $\lfloor
x-y\rfloor\equiv_{m}k$ and $\lfloor x-y\rfloor\leq k$ speaking of the _integer
part of the difference_ , since the two are inter-expressible:

$\displaystyle\lfloor x-y\rfloor=\lfloor x\rfloor-\lfloor
y\rfloor-\mathbbm{1}_{\left\\{x\right\\}<\left\\{y\right\\}?}\qquad\textrm{
and }\qquad\left\\{x-y\right\\}$
$\displaystyle=\left\\{x\right\\}-\left\\{y\right\\}+\mathbbm{1}_{\left\\{x\right\\}<\left\\{y\right\\}?}.$
(2)

##### The model.

A _timed pushdown automaton_ (tpda) is a tuple
$\mathcal{P}=\left\langle\Sigma,\Gamma,L,X,Z,\Delta\right\rangle$ where
$\Sigma$ is a finite input alphabet, $\Gamma$ is a finite stack alphabet, $L$
is a finite set of control locations, $X$ is a finite set of _global clocks_ ,
and $Z$ is a finite set of _stack clocks_ disjoint from $X$. The last item
$\Delta$ is a set of transition rules $\langle\ell,\mathsf{op},r\rangle$ with
$\ell,r\in L$ control locations, where $\mathsf{op}$ determines the type of
transition:

  * •

_time elapse_ $\mathsf{op}=\mathsf{elapse}$,

  * •

_input_ $\mathsf{op}=a\in\Sigma_{\varepsilon}:=\Sigma\cup\\{\varepsilon\\}$ an
input letter,

  * •

_test_ $\mathsf{op}=\varphi$ a _transition constraint_ over clocks $X$,

  * •

_reset_ $\mathsf{op}=\mathsf{reset}(Y)$ with $Y\subseteq X$ a set of clocks to
be reset,

  * •

_push_ $\mathsf{op}={\mathsf{push}(\alpha:\psi)}$ with $\alpha\in\Gamma$ a
stack symbol to be pushed on the stack under the _stack constraint_ $\psi$
over clocks $X\cup Z$, or

  * •

_pop_ $\mathsf{op}={\mathsf{pop}(\alpha:\psi)}$ similarly as push.

We assume that every atomic constraint in a stack constraint contains some
stack variable from $Z$. Throughout the paper, let $x_{0}$ be a global clock
that is never reset (and thus measures the total elapsed time), and let
$z_{0}$ be a stack clock that is $0$ when pushed. A tpda has _untimed stack_
if the only stack constraint is $\mathbf{true}$. Without push/pop operations,
we obtain nondeterministic timed automata (ta).

######  Remark 3.4 (Complexity).

For complexity estimations, we assume that constraints are conjunctions of
atomic constraints, that constants therein are encoded in binary, that $M$ is
the maximal constant, and that all modular constraints use the same modulus
$M$.

######  Remark 3.5 (Time elapse).

The standard semantics of timed automata where time can elapse freely in every
control location is simulated by adding explicit time elapse transitions
$\langle\ell,\mathsf{elapse},\ell\rangle$ for suitable locations $\ell$. Our
explicit modelling of the elapse of time will simplify the constructions in
Sec. 4.

######  Remark 3.6 (Comparison with dtpda).

The dtpda model [1] allows only one stack clock $Z=\left\\{z\right\\}$ and
stack constraints of the form $z\sim k$. As shown in [9], this model is
equivalent to tpda with untimed stack. Our extension is two-fold. First, our
definition of stack constraint is more liberal, since we allow more general
_diagonal stack constraints_ of the form $z-x\sim k$. Second, we also allow
_modular_ $\lfloor y\rfloor-\lfloor x\rfloor\equiv_{m}k$ and _fractional
constraints_ $\left\\{x\right\\}\sim\left\\{y\right\\}$, where clocks $x,y$
can be either global or stack clocks. As demonstrated in Example 3.7 below,
this model is not reducible to untimed stack, and thus tpda are more
expressive than dtpda.

##### Semantics.

Every stack symbol is equipped with a fresh copy of clocks from $Z$. At the
time of ${\mathsf{push}(\alpha:\psi)}$, the push constraint $\psi$ specifies
possibly nondeterministically the initial value of all clocks in $Z$ w.r.t.
global clocks in $X$. Both global and stack clocks evolve at the same rate
when a time elapse transition is executed. At the time of
${\mathsf{pop}(\alpha:\psi)}$, the pop constraint $\psi$ specifies the final
value of all clocks in $Z$ w.r.t. global clocks in $X$. A _timed stack_ is a
sequence $w\in(\Gamma\times\mathbb{Q}_{\geq 0}^{Z})^{*}$ of pairs
$(\gamma,\mu)$, where $\gamma$ is a stack symbol and $\mu$ is a valuation for
stack clocks in $Z$. For a clock valuation $\mu$ and a set of clocks $Y$, let
$\mu[Y\mapsto 0]$ be the same as $\mu$ except that clocks in $Y$ are mapped to
$0$. For $\delta\in\mathbb{Q}_{\geq 0}$, let $\mu+\delta$ be the clock
valuation which adds $\delta$ to the value of every clock, i.e.,
$(\mu+\delta)(x):=\mu(x)+\delta$, and for a timed stack
$w=(\gamma_{1},\mu_{1})\cdots(\gamma_{k},\mu_{k})$, let $w+\delta$ be
$(\gamma_{1},\mu_{1}+\delta)\cdots(\gamma_{k},\mu_{k}+\delta)$. A
_configuration_ is a triple $\left\langle\ell,\mu,w\right\rangle\in
L\times\mathbb{Q}_{\geq 0}^{X}\times(\Gamma\times\mathbb{Q}_{\geq 0}^{Z})^{*}$
where $\ell$ is a control location, $\mu$ is a clock valuation over the global
clocks $X$, and $w$ is a timed stack. Let
$\left\langle\ell,\mu,u\right\rangle,\left\langle r,\nu,v\right\rangle$ be two
configurations. For every input symbol or time increment
$a\in(\Sigma_{\varepsilon}\cup\mathbb{Q}_{\geq 0})$ we have a transition
$\left\langle\ell,\mu,u\right\rangle\xrightarrow{a}\left\langle
r,\nu,v\right\rangle$ whenever there exists a rule
$\langle\ell,\mathsf{op},r\rangle\in\Delta$ s.t. one of the following holds:

  * •

$\mathsf{op}=\mathsf{elapse}$, $a\in\mathbb{Q}_{\geq 0}$, $\nu=\mu+a$,
$v=u+a$.

  * •

$\mathsf{op}=a\in\Sigma_{\varepsilon}$, $\nu=\mu$, $u=v$.

  * •

$\mathsf{op}=\varphi$, $a=\varepsilon$, $\mu\models\varphi$, $\nu=\mu$, $u=v$.

  * •

$\mathsf{op}=\mathsf{reset}(Y)$, $a=\varepsilon$, $\nu=\mu[Y\mapsto 0]$,
$v=u$.

  * •

$\mathsf{op}={\mathsf{push}(\gamma:\psi)}$, $a=\varepsilon$, $\mu=\nu$,
$v=u\cdot\left\langle\gamma,\mu_{1}\right\rangle$ if
$\mu_{1}\in\mathbb{Q}_{\geq 0}^{Z}$ satisfies $(\mu,\mu_{1})\models\psi$,
where $(\mu,\mu_{1})\in\mathbb{Q}_{\geq 0}^{X\cup Z}$ is the unique clock
valuation that agrees with $\mu$ on $X$ and with $\mu_{1}$ on $Z$.

  * •

$\mathsf{op}={\mathsf{pop}(\gamma:\psi)}$, $a=\varepsilon$, $\mu=\nu$,
$u=v\cdot\left\langle\gamma,\mu_{1}\right\rangle$ provided that
$\mu_{1}\in\mathbb{Q}_{\geq 0}^{Z}$ satisfies $(\mu,\mu_{1})\models\psi$.

A _timed word_ is a sequence
${w=\delta_{1}a_{1}\cdots\delta_{n}a_{n}\in(\mathbb{Q}_{\geq
0}\Sigma_{\varepsilon})^{*}}$ of alternating time elapses and input symbols;
the one-step transition relation
$\left\langle\ell,\mu,u\right\rangle\xrightarrow{a}\left\langle
r,\nu,v\right\rangle$ is extended on timed words $w$ as
$\left\langle\ell,\mu,u\right\rangle\xrightarrow{w}\left\langle
r,\nu,v\right\rangle$ in the natural way. The _timed language_ from location
$\ell$ to $r$ is $L(\ell,r):=\left\\{\pi_{\varepsilon}(w)\in(\mathbb{Q}_{\geq
0}\Sigma)^{*}\;\middle|\;\left\langle\ell,\mu_{0},\varepsilon\right\rangle\xrightarrow{w}\left\langle
r,\mu_{0},\varepsilon\right\rangle\right\\}$ where $\pi_{\varepsilon}(w)$
removes the $\varepsilon$’s from $w$ and $\mu_{0}$ is the valuation that
assigns $\mu_{0}(x)=0$ to every clock $x$. The corresponding _untimed
language_ $L^{\textrm{un}}(\ell,r)$ is obtained by removing the time elapses
from $L(\ell,r)$.

######  Example 3.7.

Let $L$ be the timed language of even length palindromes s.t. the time
distance between every pair of matching symbols is an integer:

$\displaystyle
L=\left\\{\delta_{1}a_{1}\cdots\delta_{2n}a_{2n}\;\middle|\;\forall(1\leq
i\leq
n){\;\cdot\;}a_{i}=a_{2n-i+1}\wedge\delta_{i+1}+\cdots+\delta_{2n-i+1}\in\mathbb{N}\right\\}.$

$L$ can be recognised by a tpda over input and stack alphabet
$\Sigma=\Gamma=\left\\{a,b\right\\}$, with locations $\ell,r$, no global
clock, one stack clock $Z=\left\\{z\right\\}$, and the following transition
rules (omitting some intermediate states), where $\alpha$ ranges over
$\left\\{a,b\right\\}$:

$\displaystyle\langle\ell,\alpha;{\mathsf{push}(\alpha:\left\\{z\right\\}=0)},\ell\rangle$
$\displaystyle\langle\ell,\varepsilon,r\rangle$ $\displaystyle\langle
r,\alpha;{\mathsf{pop}(\alpha:\left\\{z\right\\}=0)},r\rangle$
$\displaystyle\langle\ell,\mathsf{elapse},\ell\rangle,\langle
r,\mathsf{elapse},r\rangle$

We have $L=L(\ell,r)$. Since $L$ cannot be recognised by tpda with untimed
stack (cf. [22]), fractional stack constraints strictly increase the
expressive power of the model.

##### The reachability relation.

The _Parikh image_ of a timed word $w$ is the mapping $\text{\sc
pi}_{w}\in\mathbb{N}^{\Sigma}$ s.t. $\text{\sc pi}_{w}(a)$ is the number of
$a$’s in $w$, ignoring the elapse of time and $\varepsilon$’s. For two control
locations $\ell,r$, clock valuations $\mu,\nu\in\mathbb{Q}_{\geq 0}^{X}$, and
a timed word $w\in(\mathbb{Q}_{\geq 0}\Sigma_{\varepsilon})^{*}$, we write
$\mu\stackrel{{\scriptstyle w}}{{\leadsto}}_{\ell r}\nu$ if
$\left\langle\ell,\mu,\varepsilon\right\rangle\xrightarrow{w}\left\langle
r,\nu,\varepsilon\right\rangle$. We overload the notation and, for
$\pi\in\mathbb{N}^{\Sigma}$, we write
$\mu\stackrel{{\scriptstyle\pi}}{{\leadsto}}_{\ell r}\nu$ if there exists a
timed word $w$ s.t. $\mu\stackrel{{\scriptstyle w}}{{\leadsto}}_{\ell r}\nu$
and $\pi=\text{\sc pi}_{w}$. We see
$\left\\{\stackrel{{\scriptstyle}}{{\leadsto}}_{\ell r}\right\\}_{\ell,r\in
L}$ as a family of subsets of $\mathbb{Q}_{\geq
0}^{X}\times\mathbb{N}^{\Sigma}\times\mathbb{Q}_{\geq 0}^{X}$ and we call it
the _ternary reachability relation_.

Let $\left\\{\psi_{\ell
r}(\lfloor\overline{x}\rfloor,\left\\{\overline{x}\right\\},\overline{f},\lfloor\overline{y}\rfloor,\left\\{\overline{y}\right\\})\right\\}_{\ell,r\,\in
L}$ be a family of $\mathcal{L}_{\mathbb{Z},\mathbb{Q}}$ formulas, where
$\lfloor\overline{x}\rfloor,\lfloor\overline{y}\rfloor$ represent the integer
values of initial and final clocks,
$\left\\{\overline{x}\right\\},\left\\{\overline{y}\right\\}$ their fractional
values, and $\overline{f}$ letter counts. The reachability relation
$\left\\{\stackrel{{\scriptstyle}}{{\leadsto}}_{\ell r}\right\\}_{\ell,r\in
L}$ is _expressed_ by the family of formulas $\left\\{\psi_{\ell
r}\right\\}_{\ell,r\in L}$ if the following holds: For every control locations
$\ell,r\in L$, clock valuations $\mu,\nu\in\mathbb{Q}_{\geq 0}^{X}$ and
$\pi\in\mathbb{N}^{\Sigma}$,
$\mu\stackrel{{\scriptstyle\pi}}{{\leadsto}}_{\ell r}\nu$ holds, if, and only
if,
$(\lfloor\mu\rfloor,\left\\{\mu\right\\},\pi,\lfloor\nu\rfloor,\left\\{\nu\right\\})\models\psi_{\ell
r}$ holds.

##### Main results.

As the main result of the paper we show that the reachability relation of tpda
and ta is expressible in linear arithmetic
$\mathcal{L}_{\mathbb{Z},\mathbb{Q}}$.

######  Theorem 3.8.

The reachability relation of a tpda is expressed by a family of existential
$\mathcal{L}_{\mathbb{Z},\mathbb{Q}}$ formulas computable in double
exponential time. For ta, the complexity is exponential.

This is a strengthening of analogous results for ta [11, 19] since our model,
even without stack, is more expressive than classical ta due to fractional
constraints. As a side effect of the proofs we get:

######  Theorem 3.9.

Untimed tpda languages $L^{\textrm{un}}(\ell,r)$ are effectively context-free.

The following two sections are devoted to proving the two theorem above.

##  4\. Fractional tpda

A tpda is _fractional_ if it contains only fractional constraints. We show
that computing the reachability relation reduces to the same problem for
fractional tpda. Our transformation is done in three steps, each one further
restricting the set of allowed constraints.

  * A

The tpda is _push-copy_ , that is, push operations can only copy global clocks
into stack clocks. There is one stack clock $z_{x}$ for each global clock $x$,
and the only push constraint is

$\displaystyle\psi_{\mathsf{copy}}(\overline{x},\overline{z}_{\overline{x}})\
\equiv\ \bigwedge_{x\in X}\lfloor z_{x}\rfloor=\lfloor
x\rfloor\wedge\left\\{z_{x}\right\\}=\left\\{x\right\\}.$ (3)

By pushing copies of global clocks into the stack, we can postpone checking
all non-trivial stack constraints to the time of pop. This steps uses
quantifier elimination. The blowup of the number of pop constraints and stack
alphabet is exponential.

  * B

The tpda is _pop-integer-free_ , that is, pop transitions do not contain
integer constraints. The construction is similar to a construction from [9]
and is presented in Sec. A.4. Removing pop integer constraints is crucial
towards removing all integer clocks (modulo constraints will be removed by the
next step). This step strongly relies on the fact that stack clocks are copies
of global clocks, which allows one to remove integer pop constraints by
reasoning about analogous constraints between global clocks at the time of
push and their future values at the time of pop, thus bypassing the stack
altogether. We introduce one global clock for each integer pop constraint,
exponentially many locations in the number of clocks and pop constraints, and
exponentially many stack symbols in the number of pop constraints. When
combined with the previous step, altogether exponentially many new clocks are
introduced, and doubly exponentially many locations/stack symbols. It is
remarkable that pop integer constraints can be removed by translating them
into finitely many transition constraints on global clocks.

  * C

The tpda is fractional. All integer clocks are removed. In order to recover
their values (which are needed to express the reachability relation), a
special symbol $\checkmark_{\\!\\!x}$ is produced when an integer clock
elapses one time unit. This step introduces a further exponential blowup of
control locations w.r.t. global clocks and polynomial in the maximal constant
$M$. The overall complexity of control locations thus stays double
exponential.

By A+B+C (in this order, since the latter properties are ensured assuming the
previous ones), we get the following theorem.

######  Theorem 4.1.

A tpda $\mathcal{P}$ can be effectively transformed into a fractional tpda
$\mathcal{Q}$ s.t. a family of $\mathcal{L}_{\mathbb{Z},\mathbb{Q}}$ formulas
$\left\\{\varphi_{\ell r}\right\\}$ expressing the reachability relation of
$\mathcal{P}$ can effectively be computed from a family of
$\mathcal{L}_{\mathbb{Z},\mathbb{Q}}$ formulas
$\left\\{\varphi_{\ell^{\prime}r^{\prime}}^{\prime}\right\\}$ expressing the
reachability relation of $\mathcal{Q}$. The number of control locations and
the size of the stack alphabet in $\mathcal{Q}$ have a double exponential
blowup, and the number of clocks has an exponential blowup.

If there is no stack, then we do not need the first two steps, and we can do
directly C.

######  Corollary 4.2.

The reachability relation of push-copy tpda/ ta effectively reduces to the
reachability relation of fractional tpda/ ta with an exponential blowup in
control locations.

### (A) The tpda is push-copy

Let $K_{\leq}$ be the non-strict variant of the ternary cyclic order $K$ from
(1), defined as $K_{\leq}(a,b,c)\equiv K(a,b,c)\vee a=b\vee b=c$ for
$a,b,c\in\mathbb{I}$. Let $\psi_{\mathsf{push}}(\overline{x},\overline{z})$ be
a push constraint, and let
$\psi_{\mathsf{pop}}(\overline{x}^{\prime},\overline{z}^{\prime})$ be the
corresponding pop constraint. Since stack clock $z_{0}$ is $0$ when pushed on
the stack, $z_{0}^{\prime}$ is the total time elapsed between push and pop;
let $\overline{z}_{0}^{\prime}=(z_{0}^{\prime},\dots,z_{0}^{\prime})$ (the
length of which depends on the context). Let
$\overline{z}_{\overline{x}}^{\prime}$ be a vector of stack variables
representing the value of _global clocks_ at the time of pop, provided they
were not reset since the matching push. Since all clocks evolve at the same
rate, for every global clock $x$ and stack clock $z$, we have

$\displaystyle x=z^{\prime}_{x}-z_{0}^{\prime}\qquad\textrm{ and }\qquad
z=z^{\prime}-z_{0}^{\prime}.$ (4)

If at the time of push, instead of pushing $\overline{z}$, we push on the
stack a copy of global clocks $\overline{x}$, then at the time of pop it
suffices to check that the following formula holds

$\displaystyle\psi_{\mathsf{pop}}^{\prime}(\overline{x}^{\prime},\overline{z}^{\prime}_{\overline{x}})\
\equiv\
\exists\overline{z}^{\prime}\geq\overline{0}{\;\cdot\;}\psi_{\mathsf{push}}(\overline{z}^{\prime}_{\overline{x}}-\overline{z}_{0}^{\prime},\overline{z}^{\prime}-\overline{z}_{0}^{\prime})\wedge\psi_{\mathsf{pop}}(\overline{x}^{\prime},\overline{z}^{\prime}).$
(5)

Note that the assumption that $z_{0}=0$ at the time of push makes the
existential quantification satisfiable by exactly one value of
$z^{\prime}_{0}$, namely the total time elapsed between push and pop. However,
$\psi_{\mathsf{push}}(\overline{z}^{\prime}_{\overline{x}}-\overline{z}_{0}^{\prime},\overline{z}^{\prime}-\overline{z}_{0}^{\prime})$
is not a constraint anymore, since variables are replaced by differences of
variables. We resolve this issue by showing that the latter is in fact
equivalent to a clock constraint. Thanks to (4), for every clock $x$ we have
${\lfloor x\rfloor=\lfloor
z^{\prime}_{x}-z_{0}^{\prime}\rfloor},{\left\\{x\right\\}=\left\\{z^{\prime}_{x}-z_{0}^{\prime}\right\\}}$,
and ${\lfloor z\rfloor=\lfloor
z^{\prime}-z_{0}^{\prime}\rfloor},{\left\\{z\right\\}=\left\\{z^{\prime}-z_{0}^{\prime}\right\\}}$.
Thus, a fractional constraint $\left\\{y\right\\}\leq\left\\{z\right\\}$ in
$\psi_{\mathsf{push}}$ is equivalent to
$\left\\{z^{\prime}_{y}-z_{0}^{\prime}\right\\}\leq\left\\{z^{\prime}-z_{0}^{\prime}\right\\}$,
which is in turn equivalent to
$C=K_{\leq}(\left\\{z_{0}^{\prime}\right\\},\left\\{z^{\prime}_{y}\right\\},\left\\{z^{\prime}\right\\})$,
which is definable from $\leq$. Moreover, $\lfloor y\rfloor-\lfloor
z\rfloor=\lfloor z^{\prime}_{y}-z_{0}^{\prime}\rfloor-\lfloor
z^{\prime}-z_{0}^{\prime}\rfloor=(z^{\prime}_{y}-z_{0}^{\prime}-\left\\{z^{\prime}_{y}-z_{0}^{\prime}\right\\})-(z^{\prime}-z_{0}^{\prime}-\left\\{z^{\prime}-z_{0}^{\prime}\right\\})=(z^{\prime}_{y}-z^{\prime})-\left\\{z^{\prime}_{y}-z_{0}^{\prime}\right\\}+\left\\{z^{\prime}-z_{0}^{\prime}\right\\}=(z^{\prime}_{y}-z^{\prime})-\left\\{z^{\prime}_{y}-z^{\prime}\right\\}+\mathbbm{1}_{D?}=\lfloor
z^{\prime}_{y}-z^{\prime}\rfloor+\mathbbm{1}_{D?}$, with
$D=C\wedge\left\\{z^{\prime}_{y}\right\\}\neq\left\\{z^{\prime}\right\\}$.
(Notice that $\lfloor z_{0}^{\prime}\rfloor$ disappears in this process: This
is not a coincidence, since diagonal integer/modular/fractional constraints
are invariant under the elapse of an _integer_ amount of time.) Thus by (2) we
obtain a constraint
$\psi_{\mathsf{push}}^{\prime}(\overline{z}^{\prime}_{\overline{x}},\overline{z}^{\prime})$
logically equivalent to
${\psi_{\mathsf{push}}(\overline{z}^{\prime}_{\overline{x}}-\overline{z}_{0}^{\prime},\overline{z}^{\prime}-\overline{z}_{0}^{\prime})}$,
and, by separating the fractional and integer constraints (cf. Remark 3.1),
$\psi_{\mathsf{pop}}^{\prime}(\overline{x}^{\prime},\overline{z}^{\prime}_{\overline{x}})\equiv\exists\lfloor\overline{z}^{\prime}\rfloor,\left\\{\overline{z}^{\prime}\right\\}{\;\cdot\;}\psi_{\mathsf{push}}^{\prime}(\lfloor\overline{z}^{\prime}_{\overline{x}}\rfloor,\left\\{\overline{z}^{\prime}_{\overline{x}}\right\\},\lfloor\overline{z}^{\prime}\rfloor,\left\\{\overline{z}^{\prime}\right\\})\wedge\psi_{\mathsf{pop}}(\lfloor\overline{x}^{\prime}\rfloor,\left\\{\overline{x}^{\prime}\right\\},\lfloor\overline{z}^{\prime}\rfloor,\left\\{\overline{z}^{\prime}\right\\})$.
By Corollary 2.3, we can perform quantifier elimination and we obtain a
logically equivalent clock constraint of exponential size (in DNF)
$\xi_{\psi_{\mathsf{push}},\psi_{\mathsf{pop}}}(\lfloor\overline{x}^{\prime}\rfloor,\left\\{\overline{x}^{\prime}\right\\},\lfloor\overline{z}^{\prime}_{\overline{x}}\rfloor,\left\\{\overline{z}^{\prime}_{\overline{x}}\right\\}),$
where the subscript indicates that this formula depends on the pair
$(\psi_{\mathsf{push}},\psi_{\mathsf{pop}})$ of push and pop constraints. The
construction of $\mathcal{P}^{\prime}$ consists in checking
$\xi_{\psi_{\mathsf{push}},\psi_{\mathsf{pop}}}$ in place of
$\psi_{\mathsf{pop}}$, assuming that the push constraint was
$\psi_{\mathsf{push}}$. The latter is replaced by $\psi_{\mathsf{copy}}$.
Control states are the same in the two automata; we can break down the
$\xi_{\psi_{\mathsf{push}},\psi_{\mathsf{pop}}}$ in DNF and record each
conjunct in the stack, yielding a new stack alphabet of exponential size.

######  Lemma 4.3.

Let $\left\\{\stackrel{{\scriptstyle}}{{\leadsto}}_{\ell
r}\right\\}_{\ell,r\in L}$,
$\left\\{\stackrel{{\scriptstyle}}{{\leadsto}}_{\ell
r}^{\prime}\right\\}_{\ell,r\in L}$ be the reachability relations of
$\mathcal{P}$, resp., $\mathcal{P}^{\prime}$. Then,
$\stackrel{{\scriptstyle}}{{\leadsto}}_{\ell
r}=\stackrel{{\scriptstyle}}{{\leadsto}}_{\ell r}^{\prime}$ for every
$\ell,r\in L$, and $\mathcal{P}^{\prime}$ has stack alphabet exponential in
the size of $\mathcal{P}$.

### (C) The tpda is fractional

Assume that the tpda $\mathcal{P}$ is both push-copy (A) and pop-integer-free
(B). We remove diagonal integer $\lfloor y\rfloor-\lfloor x\rfloor\sim k$ and
modulo $\lfloor y\rfloor-\lfloor x\rfloor\equiv_{m}k$ constraints on global
clocks $x,y$ as in ta [2]. In the rest of the section, transition and stack
constraints of $\mathcal{P}$ are of the form

(trans.) $\displaystyle\lfloor x\rfloor$ $\displaystyle\leq k,$
$\displaystyle\lfloor x\rfloor$ $\displaystyle\equiv_{m}k,$
$\displaystyle\left\\{x\right\\}$ $\displaystyle=0,$
$\displaystyle\left\\{x\right\\}$ $\displaystyle\leq\left\\{y\right\\},$ (6)
(push) $\displaystyle\lfloor z_{x}\rfloor$ $\displaystyle=\lfloor x\rfloor,$
$\displaystyle\left\\{z_{x}\right\\}$ $\displaystyle=\left\\{x\right\\},$ (7)
(pop) $\displaystyle\lfloor y\rfloor-\lfloor z_{x}\rfloor$
$\displaystyle\equiv_{m}k,$ $\displaystyle\left\\{z_{x}\right\\}$
$\displaystyle=0,$ $\displaystyle\left\\{y\right\\}$
$\displaystyle\leq\left\\{z_{x}\right\\},$ (8) $\displaystyle\lfloor
z_{y}\rfloor-\lfloor z_{x}\rfloor$ $\displaystyle\equiv_{m}k,$
$\displaystyle\left\\{z_{y}\right\\}$
$\displaystyle\leq\left\\{z_{x}\right\\}.$

##### Unary abstraction.

We replace the integer value of clocks by their _unary abstraction_ :
Valuations $\mu,\nu\in\mathbb{Q}_{\geq 0}^{X}$ are _$M$ -unary equivalent_,
written $\mu\approx_{M}\nu$, if, for every clock $x\in X$,
$\lfloor\mu(x)\rfloor\equiv_{M}\lfloor\nu(x)\rfloor$ and
$\lfloor\mu(x)\rfloor\leq M\Leftrightarrow\lfloor\nu(x)\rfloor\leq M$. Let
$\Lambda_{M}$ be the (finite) set of $M$-unary equivalence classes of clock
valuations. For $\lambda\in\Lambda_{M}$ we abuse notation and write
$\lambda(x)$ to indicate $\mu(x)$ for some $\mu\in\lambda$, where the choice
of representative $\mu$ does not matter. We write $\lambda[Y\mapsto 0]$ for
the equivalence class of $\nu[Y\mapsto 0]$ and we write $\lambda[x\mapsto
x+1]$ for the equivalence class of $\nu[x\mapsto\nu(x)+1]$, for some
$\nu\in\lambda$ (whose choice is irrelevant). Let
$\varphi_{\lambda}(\overline{x})\equiv\bigwedge_{x\in X}\lfloor
x\rfloor\equiv_{M}\lambda(x)\wedge(\lfloor
x\rfloor<M\Leftrightarrow\lambda(x)<M)$ say that clocks belong to $\lambda$.
For $\varphi$ containing transition constraints of the form (6),
$\left.\varphi\right|_{\lambda}$ is $\varphi$ where every integer $\lfloor
x\rfloor\leq k$ or modulo constraint $\lfloor x\rfloor\equiv_{M}k$ is uniquely
resolved to be $\mathbf{true}$ or $\mathbf{false}$ by replacing every
occurrence of $\lfloor x\rfloor$ with $\lambda(x)$. Similarly, for $\psi$ a
pop constraint of the form (8),
$\left.\psi\right|_{\lambda_{\mathsf{push}},\lambda_{\mathsf{pop}}}$ is
obtained by resolving modulo constraints $\lfloor y\rfloor-\lfloor
z_{x}\rfloor\equiv_{M}k$ and $\lfloor z_{y}\rfloor-\lfloor
z_{x}\rfloor\equiv_{M}k$ to be $\mathbf{true}$ or $\mathbf{false}$ by
replacing every occurrence of $\lfloor y\rfloor$ by its abstraction at the
time of pop $\lambda_{\mathsf{pop}}(y)$, and every occurrence of $\lfloor
z_{x}\rfloor$ by
$\lambda_{\mathsf{push}}(x)+\Delta(\lambda_{\mathsf{push}},\lambda_{\mathsf{pop}})$,
i.e., the initial value of clock $x$ plus the total integer time elapsed until
the pop, defined as
$\Delta(\lambda_{\mathsf{push}},\lambda_{\mathsf{pop}})=\lambda_{\mathsf{pop}}(x_{0})-\lambda_{\mathsf{push}}(x_{0})-\mathbbm{1}_{\left\\{z_{0}\right\\}>\left\\{x_{0}\right\\}?}$,
i.e., we take the difference of $x_{0}$ (which is never reset) between push
and pop, possibly corrected by “$-1$” if the last time unit only partially
elapsed; the substitution for $\lfloor z_{y}\rfloor$ is analogous. Fractional
constraints are unchanged.

##### Sketch of the construction.

Given a push-copy and pop-integer-free tpda $\mathcal{P}$, we build a
fractional tpda $\mathcal{Q}$ over the extended alphabet
$\Sigma^{\prime}=\Sigma\cup\left\\{\checkmark_{\\!\\!x}\;\middle|\;x\in
X\right\\}$ as follows. We eliminate integer $\lfloor x\rfloor\leq k$ and
modulo constraints $\lfloor x\rfloor\equiv_{M}k$ by storing in the control the
$M$-unary abstraction $\lambda$. To reconstruct the reachability relation of
$\mathcal{P}$, we store the set of clocks $Y$ which will not be reset anymore
in the future. Thus, control locations $L^{\prime}$ of $\mathcal{Q}$ are of
the form $\left\langle\ell,\lambda,Y\right\rangle$. In order to properly
update the $M$-unary abstraction $\lambda$, the automaton checks how much time
elapses by looking at the fractional values of clocks. When $\lambda$ is
updated to $\lambda[x\mapsto x+1]$, a symbol $\checkmark_{\\!\\!x}$ is
optionally produced if $x\in Y$ was guessed not to be reset anymore in the
future. A test transition $\langle\ell,\varphi,r\rangle$ is simulated by
$\langle\left\langle\ell,\lambda,Y\right\rangle,\left.\varphi\right|_{\lambda},\left\langle
r,\lambda,Y\right\rangle\rangle$. A push-copy transition
$\langle\ell,{\mathsf{push}(\alpha:\psi_{\mathsf{copy}})},r\rangle$ is
simulated by
$\langle\left\langle\ell,\lambda,Y\right\rangle,{\mathsf{push}(\left\langle\alpha,\lambda\right\rangle:\bigwedge_{x\in
X}\left\\{z_{0}\right\\}=0\wedge\left\\{z_{x}\right\\}=\left\\{x\right\\})},\left\langle
r,\lambda,Y\right\rangle\rangle$ copying only the fractional parts and the
unary class of global clocks. A pop-integer-free transition
$\langle\ell,{\mathsf{pop}(\alpha:\psi)},r\rangle$ is simulated by
$\langle\left\langle\ell,\lambda_{\mathsf{pop}},Y\right\rangle,{\mathsf{pop}(\left\langle\alpha,\lambda_{\mathsf{push}}\right\rangle:\left.\psi\right|_{\lambda_{\mathsf{push}},\lambda_{\mathsf{pop}}})},\left\langle
r,\lambda_{\mathsf{pop}},Y\right\rangle\rangle$. The reachability formula
$\varphi_{\ell r}$ for $\mathcal{P}$ can be expressed by guessing the initial
and final abstractions $\lambda,\mu$, and the set of clocks $Y$ which is never
reset in the run. For clocks $x\in Y$, we must observe precisely $\lfloor
x^{\prime}\rfloor-\lfloor x\rfloor$ ticks $\checkmark_{\\!\\!x}$, and for the
others, $\lfloor x^{\prime}\rfloor$, where $x$ is the initial and $x^{\prime}$
the final value. Let $g^{Y}_{x}=\lfloor x^{\prime}\rfloor-\lfloor x\rfloor$ if
$x\in Y$, and $\lfloor x^{\prime}\rfloor$ otherwise.

######  Lemma 4.4.

Let
$\left\\{\psi_{\ell^{\prime}r^{\prime}}(\left\\{\overline{x}\right\\},(\overline{f},\overline{g}),\left\\{\overline{x}^{\prime}\right\\})\right\\}_{\ell^{\prime},r^{\prime}\in
L^{\prime}}$ express the reachability relation of the fractional $\mathcal{Q}$
where $\left\\{\overline{x}\right\\},\left\\{\overline{x}^{\prime}\right\\}$
are the fractional values of clocks (we ignore integer values), $\overline{f}$
is the Parikh image of the original input letters from $\Sigma$, and
$\overline{g}$ of the new input letters $\checkmark_{\\!\\!x}$’s. The
reachability relation of $\mathcal{P}$ is expressed by $\varphi_{\ell
r}(\lfloor\overline{x}\rfloor,\left\\{\overline{x}\right\\},\overline{f},\lfloor\overline{x}^{\prime}\rfloor,\left\\{\overline{x}^{\prime}\right\\})\equiv\bigvee_{\lambda,Y,\mu}\varphi_{\lambda}(\lfloor\overline{x}\rfloor)\wedge\psi_{\left\langle\ell,\lambda,Y\right\rangle\left\langle
r,\mu,X\right\rangle}(\left\\{\overline{x}\right\\},(\overline{f},\overline{g}^{Y}),\left\\{\overline{x}^{\prime}\right\\})$.

##  5\. From fractional tpda to register pda

The aim of this section is to prove the following result which, together with
Theorem 4.1, completes the proof of our main result Theorem 3.8.

######  Theorem 5.1.

The fractional reachability relation of a fractional tpda $\mathcal{P}$ is
expressed by existential $\mathcal{L}_{\mathbb{Z},\mathbb{Q}}$ formulas,
computable in time exponential in the number of clocks and polynomial in the
number of control locations and stack alphabet.

##### Cyclic atoms.

We model fractional clock values by the _cyclic atoms_ structure
${(\mathbb{I},K)}$ with universe $\mathbb{I}=\mathbb{Q}\cap[0,1)$, where $K$
is the ternary cyclic order (1). Since $K$ is invariant under cyclic shift, it
is convenient to think of elements of $\mathbb{I}$ as placed clockwise on a
circle of unit perimeter; cf. Fig. 1(a). An _automorphism_ is a bijection
$\alpha$ that preserves and reflects $K$, i.e., $K(a,b,c)$ iff
$K(\alpha(a),\alpha(b),\alpha(c))$; automorphisms are extended to tuples
$\mathbb{I}^{n}$ point-wise.

(a)•0•$a$•$b$•$c$

(b)•0•$a$•$b$

Figure 1.  (a) Relation $K$. (b) The cyclic difference $b\ominus a$.

Cyclic atoms are homogeneous [17] and thus $\mathbb{I}^{n}$ splits into
exponentially many _orbits_ $\mathrm{Orb}(\mathbb{I}^{n})$, where
$u,v\in\mathbb{I}^{n}$ are in the same orbit if some automorphism maps $u$ to
$v$. An orbit is an equivalence class of indistinguishable tuples, similarly
as regions for clock valuations, but in a different logical structure: For
instance $(0.2,0.3,0.7)$, $(0.7,0.2,0.3)$, and $(0.8,0.2,0.3)$ belong to the
same orbit, while $(0.2,0.3,0.3)$ belongs to a different orbit.

##### Register PDA.

We extend classical pushdown automata with additional $\mathbb{I}$-valued
_registers_ , both in the finite control (i.e., global registers) and in the
stack. Registers can be compared by quantifier-free formulas with equality and
$K$, called _$K$ -constraints_. For simplicity, we assume that there are the
same number of global and stack registers. A _register pushdown automaton_
(rpda) is a tuple
$\mathcal{Q}=\left\langle\Sigma,\Gamma,L,X,Z,\Delta\right\rangle$ where
$\Sigma$ is a finite input alphabet, $\Gamma$ is a finite stack alphabet, $L$
is a finite set of control locations, $X$ is a finite set of _global
registers_ , $Z$ is a finite set of _stack registers_ , and the last item
$\Delta$ is a set of transition rules $\langle\ell,\mathsf{op},r\rangle$ with
$\ell,r\in L$ control locations, where $\mathsf{op}$ is either: 1) an input
letter $a\in\Sigma_{\varepsilon}$, 2) a $2k$-ary $K$-constraint
$\psi(\overline{x},\overline{x}^{\prime})$ relating pre- and post-values of
global registers, 3) a push operation
${\mathsf{push}(\alpha:\psi(\overline{x},\overline{z}))}$ with
$\alpha\in\Gamma$ a stack symbol to be pushed on the stack under the $2k$-ary
$K$-constraint $\psi$ relating global $\overline{x}$ and stack $\overline{z}$
registers, or 4) a pop operation
${\mathsf{pop}(\alpha:\psi(\overline{x},\overline{z}))}$, similarly as push.
We consider rpda as symbolic representations of classical pda with infinite
sets of control states $\widetilde{L}=L\times\mathbb{I}^{X}$ and infinite
stack alphabet $\widetilde{\Gamma}=\Gamma\times\mathbb{I}^{Z}$. A
_configuration_ is thus a tuple $\left\langle\ell,\mu,w\right\rangle\in
L\times\mathbb{I}^{X}\times\widetilde{\Gamma}^{*}$ where $\ell$ is a control
location, $\mu$ is a valuation of the global registers, and $w$ is the current
content of the stack. Let $\left\langle\ell,\mu,u\right\rangle,\left\langle
r,\nu,v\right\rangle$ be two configurations. For every input symbol
$a\in\Sigma_{\varepsilon}$ we have a transition
$\left\langle\ell,\mu,u\right\rangle\xrightarrow{a}\left\langle
r,\nu,v\right\rangle$ whenever there exists a rule
$\langle\ell,\mathsf{op},r\rangle\in\Delta$ s.t. one of the following holds:
1) $\mathsf{op}=a\in\Sigma_{\varepsilon}$, $\mu=\nu$, $u=v$, or 2)
$\mathsf{op}=\varphi$, $a=\varepsilon$, $(\mu,\nu)\models\varphi$, $u=v$, or
3) $\mathsf{op}={\mathsf{push}(\gamma:\psi)}$, $a=\varepsilon$, $\mu=\nu$,
$v=u\cdot\left\langle\gamma,\mu_{1}\right\rangle$ if
$\mu_{1}\in\mathbb{I}^{Z}$ satisfies $(\mu,\mu_{1})\models\psi$, or 4)
$\mathsf{op}={\mathsf{pop}(\gamma:\psi)}$, $a=\varepsilon$, $\mu=\nu$,
$u=v\cdot\left\langle\gamma,\mu_{1}\right\rangle$ if
$\mu_{1}\in\mathbb{I}^{Z}$ satisfies $(\mu,\mu_{1})\models\psi$.

##### Reachability relation.

The reachability relations $\mu\stackrel{{\scriptstyle w}}{{\leadsto}}_{\ell
r}\nu$ and $\mu\stackrel{{\scriptstyle f}}{{\leadsto}}_{\ell r}\nu$ are
defined as for tpda by extending one-step transitions
$\left\langle\ell,\mu,u\right\rangle\xrightarrow{a}\left\langle
r,\nu,v\right\rangle$ to words $w\in\Sigma^{*}$ and their Parikh images
$f=\text{\sc pi}_{w}\in\mathbb{N}^{\Sigma}$. Thus, $\mu\stackrel{{\scriptstyle
f}}{{\leadsto}}_{\ell r}\nu$ is a subset of
$\mathbb{I}^{X}\times\mathbb{N}^{\Sigma}\times\mathbb{I}^{X}$, which is
furthermore invariant under orbits. In the following let $X^{\prime}$ be a
copy of global clocks. An initial valuation $\mu$ belongs to $\mathbb{I}^{X}$,
a final valuation $\nu$ to $\mathbb{I}^{X^{\prime}}$, and the joint valuation
$(\mu,\nu)$ belongs to $\mathbb{I}^{X\times X^{\prime}}$. The following two
lemmas hold for rpda with homogeneous atoms; cf. [8], or Sec. 9 in [4].

######  Lemma 5.2.

If $(\mu,\nu),(\mu^{\prime},\nu^{\prime})$ belong to the same orbit of
$\mathbb{I}^{X\times X^{\prime}}$, then $\mu\stackrel{{\scriptstyle
f}}{{\leadsto}}_{\ell r}\nu$ iff $\mu^{\prime}\stackrel{{\scriptstyle
f}}{{\leadsto}}_{\ell r}\nu^{\prime}$.

######  Lemma 5.3.

Given a rpda $\mathcal{Q}$ one can construct a context-free grammar $G$ of
exponential size with nonterminals of the form $X_{\ell ro}$, for control
locations $\ell,r$ and an orbit $o\in\mathrm{Orb}(\mathbb{I}^{X\times
X^{\prime}})$, recognising the language $L(X_{\ell
ro})=\left\\{\pi_{\Sigma}(w)\in\Sigma^{*}\;\middle|\;\exists(\mu,\nu)\in
o{\;\cdot\;}\mu\stackrel{{\scriptstyle w}}{{\leadsto}}_{\ell r}\nu\right\\},$
where $\pi_{\Sigma}(w)$ is $w$ without the $\varepsilon$’s. Consequently, rpda
recognise context-free languages.

######  Lemma 5.4 (Theorem 4 of [23]).

The Parikh image of $L(X_{\ell ro})$ is expressed by an existential Presburger
formula $\varphi^{\mathbb{Z}}_{\ell ro}$ computable in time linear in the size
of the grammar.

######  Corollary 5.5.

Let $\varphi^{\mathbb{I}}_{o}$ be the characteristic $K$-constraint of the
orbit $o\in\mathrm{Orb}({\mathbb{I}^{X\times X^{\prime}}})$. The reachability
relation $\stackrel{{\scriptstyle}}{{\leadsto}}_{\ell r}$ of an rpda
$\mathcal{Q}$ is expressed by $\varphi_{\ell
r}(\overline{x},\overline{f},\overline{x}^{\prime})\ \equiv\
\bigvee_{o\in\mathrm{Orb}({\mathbb{I}^{X\times
X^{\prime}}})}\varphi^{\mathbb{Z}}_{\ell
ro}(\overline{f})\wedge\varphi^{\mathbb{I}}_{o}(\overline{x},\overline{x}^{\prime})$.
The size of $\varphi_{\ell r}$ is exponential in the size of $\mathcal{Q}$.

######  Proof 5.6 (Proof of Theorem 5.1).

Define _cyclic sum_ and _difference_ of $a,b\in\mathbb{Q}$ to be $a\oplus
b=\left\\{a+b\right\\}$, resp., $a\ominus b:=\left\\{a-b\right\\}$. For a set
of clocks $X$, let $X_{x_{0}}=X\cup\left\\{x_{0}\right\\}$ be its extension
with an extra clock $x_{0}\notin X$ which is never reset, and let
$\hat{X}_{x_{0}}=\left\\{\hat{x}\;\middle|\;x\in X_{x_{0}}\right\\}$ be a
corresponding set of registers. The special register $\hat{x}_{0}$ stores the
(fractional part of the) current timestamp, and register $\hat{x}$ stores the
(fractional part of the) timestamp of the last reset of $x$. In this way we
can recover the fractional value of $x$ as the cyclic difference
$\left\\{x\right\\}=\hat{x}_{0}\ominus\hat{x}$. Let (cf. Fig. 1(b))

$\displaystyle\varphi_{\ominus}(\overline{x},\overline{\hat{x}})\equiv\bigwedge_{x\in
X}\left\\{x\right\\}=\hat{x}_{0}\ominus\hat{x}.$ (9)

Resetting clocks in $Y\subseteq X$ is simulated by
$\varphi_{\mathsf{reset}(Y)}\equiv\hat{x}_{0}^{\prime}=\hat{x}_{0}\wedge\bigwedge_{x\in
Y}\hat{x}^{\prime}=\hat{x}_{0}\wedge\bigwedge_{x\in X\setminus
Y}\hat{x}^{\prime}=\hat{x}$ and time elapse by
$\varphi_{\mathsf{elapse}}\equiv\bigwedge_{x\in X}\hat{x}^{\prime}=\hat{x}$.
The equality $\hat{x}_{0}^{\prime}=\hat{x}_{0}$ in
$\varphi_{\mathsf{reset}(Y)}$ says that time does not elapse, and the absence
of constraints on $\hat{x}_{0},\hat{x}_{0}^{\prime}$ in
$\varphi_{\mathsf{elapse}}$ allows for an arbitrary elapse of time. A clock
constraint $\varphi$ is converted into a $K$-constraint $\hat{\varphi}$ by
replacing $\left\\{x\right\\}=0$ with $\hat{x}=\hat{x}_{0}$ and
$\left\\{x\right\\}\leq\left\\{y\right\\}$ by
$K_{\leq}(\hat{y},\hat{x},\hat{x}_{0})$, for $x,y\in X\cup Z$. For a tpda
$\mathcal{P}=\left\langle\Sigma,\Gamma,L,X,Z,\Delta\right\rangle$, we define
the following rpda
$\mathcal{Q}=\left\langle\Sigma,\Gamma,L,\hat{X}_{x_{0}},\hat{Z},\hat{\Delta}\right\rangle$.
The input rules are preserved. A reset rule
$\langle\ell,\mathsf{reset}(Y),r\rangle\in\Delta$, is simulated by
$\langle\ell,\varphi_{\mathsf{reset}(Y)},r\rangle\in\hat{\Delta}$, a time
elapse rule $\langle\ell,\mathsf{elapse},r\rangle\in\Delta$ is simulated by
$\langle\ell,\varphi_{\mathsf{elapse}},r\rangle\in\hat{\Delta}$, a push rule
$\langle\ell,{\mathsf{push}(\gamma:\varphi)},r\rangle\in\Delta$ is simulated
by
$\langle\ell,{\mathsf{push}(\gamma:\hat{\varphi})},r\rangle\in\hat{\Delta}$,
and similarly for pop rules. By Corollary 5.5, let $\varphi_{\ell
r}(\overline{\hat{x}},\overline{f},\overline{\hat{x}^{\prime}})$ express the
reachability relation of $\mathcal{Q}$, and define
$\xi_{o}^{\mathbb{I}}(\overline{x},\overline{x}^{\prime})\equiv\exists\overline{\hat{x}},\overline{\hat{x}^{\prime}}{\;\cdot\;}\varphi_{o}^{\mathbb{I}}(\overline{\hat{x}},\overline{\hat{x}^{\prime}})\wedge\varphi_{\ominus}(\overline{x},\overline{\hat{x}})\wedge\varphi_{\ominus}(\overline{x}^{\prime},\overline{\hat{x}^{\prime}}).$
The reachability relation of $\mathcal{P}$ is recovered as

$\displaystyle\begin{aligned} \psi_{\ell
r}(\overline{x},\overline{f},\overline{x}^{\prime})\equiv\bigvee\\{\varphi^{\mathbb{Z}}_{\ell
ro}(\overline{f})\wedge\xi^{\mathbb{I}}_{o}(\overline{x},\overline{x}^{\prime})|{o\in\mathrm{Orb}({\mathbb{I}^{X\times
X^{\prime}}})}\\}.\end{aligned}$ (10)

Intuitively, we guess the value for registers
$\overline{\hat{x}},\overline{\hat{x}^{\prime}}$ and we check that they
correctly describe the fractional values of global clocks as prescribed by
$\varphi_{\ominus}$. We now remove the quantifiers from $\xi_{o}^{\mathbb{I}}$
to uncover the structure of fractional value comparisons. Introduce a new
variable $\delta=\hat{x}_{0}\ominus\hat{x}_{0}^{\prime}$, and perform the
following substitutions in $\varphi_{o}^{\mathbb{I}}$ (c.f. the definition of
$\varphi_{\ominus}$ in (9)):
$\hat{x}\mapsto\hat{x}_{0}\ominus\left\\{x\right\\}$,
$\hat{x}^{\prime}\mapsto(\hat{x}_{0}\ominus\delta)\ominus\left\\{x^{\prime}\right\\}$,
and $\hat{x}_{0}^{\prime}\mapsto\hat{x}_{0}\ominus\delta$. By writing
$(\hat{x}_{0}\ominus\delta)\ominus\left\\{x^{\prime}\right\\}$ as
$\hat{x}_{0}\ominus(\delta\oplus\left\\{x^{\prime}\right\\})$, we have only
atomic constraints of the forms $K(\hat{x}_{0}\ominus u,\hat{x}_{0}\ominus
v,\hat{x}_{0}\ominus t)$ and $\hat{x}_{0}\ominus u=\hat{x}_{0}\ominus v$,
where terms $u,v,t$ are of one of the forms $0$, $\left\\{x\right\\}$,
$\delta\oplus\left\\{x^{\prime}\right\\}$, $\delta$. These constraints are
equivalent, respectively, to $K(t,v,u)$ and $u=v$. By expanding the definition
of $K$ (cf. (1)), we obtain only constraints of the form $u\precsim v$ with
$\precsim\in\left\\{<,\leq\right\\}$. Since $\delta$ appears at most once on
either side, it can either be eliminated if it appears on both $u,v$, or
otherwise exactly one of $u,v$ is of the form $\delta$ or
$\delta\oplus\left\\{x^{\prime}\right\\}$, and the other of the form $0$ or
$\left\\{x\right\\}$. By moving $\left\\{x^{\prime}\right\\}$ on the other
side of the inequality in constraints containing
$\delta\oplus\left\\{x^{\prime}\right\\}$, $\xi_{o}^{\mathbb{I}}$ is
equivalent to $\bigwedge_{i}s_{i}\precsim t_{i}\ \wedge\ \exists
0\leq\delta<1{\;\cdot\;}\bigwedge_{j}u_{j}\precsim\delta\wedge\bigwedge_{k}\delta\precsim
v_{k}$, where the terms $s_{i},t_{i},u_{j},v_{k}$’s are of the form $0$,
$\left\\{x\right\\}$, or
$\left\\{x\right\\}\ominus\left\\{y^{\prime}\right\\}$. We can now eliminate
the quantification on $\delta$ and get a constraint of the form
$\bigwedge_{h}s_{h}\precsim t_{h}$. Finally, by expanding $b\ominus a$ as
$b-a+1$ if $b<a$ and $b-a$ otherwise (since $a,b\in\mathbb{I}$) we have
$\xi_{o}^{\mathbb{I}}(\overline{x},\overline{x}^{\prime})\ \equiv\
\bigwedge_{h}s_{h}^{\prime}\precsim t_{h}^{\prime},$ where the
$s_{h}^{\prime},t_{h}^{\prime}$’s are of one of the forms: $0$,
$\left\\{x\right\\}$, $\left\\{x\right\\}-\left\\{y^{\prime}\right\\}$, or
$\left\\{x\right\\}-\left\\{y^{\prime}\right\\}+1$.

## References

  * [1] P. A. Abdulla, M. F. Atig, and J. Stenman.  Dense-timed pushdown automata.  In Proc. LICS’12, pages 35–44. IEEE, 2012.  doi:10.1109/LICS.2012.15.
  * [2] Rajeev Alur and David L. Dill.  A theory of timed automata.  Theor. Comput. Sci., 126:183–235, 1994.
  * [3] M. Benerecetti, S. Minopoli, and A. Peron.  Analysis of timed recursive state machines.  In Proc. TIME’10, pages 61–68. IEEE, sept. 2010.  doi:10.1109/TIME.2010.10.
  * [4] Mikołaj Bojańczyk.  Slightly infinite sets.  URL: https://www.mimuw.edu.pl/~bojan/paper/atom-book.
  * [5] Ahmed Bouajjani, Rachid Echahed, and Riadh Robbana.  On the automatic verification of systems with continuous variables and unbounded discrete data structures.  In Proc. Hybrid Systems ’94, volume 999 of LNCS, pages 64–85. Springer, 1995.
  * [6] L. Clemente and S. Lasota.  Timed pushdown automata revisited.  ArXiv e-prints, March 2015.  arXiv:1503.02422.
  * [7] Lorenzo Clemente.  Decidability of timed communicating automata.  ArXiv e-prints, 04 2018.  arXiv:1804.07815.
  * [8] Lorenzo Clemente and Slawomir Lasota.  Reachability analysis of first-order definable pushdown systems.  In Proc. of CSL’15, volume 41 of LIPIcs, pages 244–259. Dagstuhl, 2015.
  * [9] Lorenzo Clemente and Slawomir Lasota.  Timed pushdown automata revisited.  In Proc. LICS’15, pages 738–749. IEEE, July 2015.
  * [10] Lorenzo Clemente, Sławomir Lasota, Ranko Lazić, and Filip Mazowiecki.  Timed pushdown automata and branching vector addition systems.  In Proc. of LICS’17, 2017.
  * [11] Hubert Comon and Yan Jurski.  Timed automata and the theory of real numbers.  In Proc. of CONCUR’99, CONCUR ’99, pages 242–257, London, UK, UK, 1999. Springer-Verlag.
  * [12] Zhe Dang.  Pushdown timed automata: a binary reachability characterization and safety verification.  Theor. Comput. Sci., 302(1–3):93–121, June 2003.  doi:10.1016/S0304-3975(02)00743-0.
  * [13] Zhe Dang, Oscar H. Ibarra, Tevfik Bultan, Richard A. Kemmerer, and Jianwen Su.  Binary reachability analysis of discrete pushdown timed automata.  In E. Allen Emerson and Aravinda Prasad Sistla, editors, Proc. of CAV 2000, pages 69–84, Berlin, Heidelberg, 2000.  doi:10.1007/10722167_9.
  * [14] C. Dima.  Computing reachability relations in timed automata.  In In Proc. of LICS’02, pages 177–186, 2002.
  * [15] Jeanne Ferrante and Charles Rackoff.  A decision procedure for the first order theory of real addition with order.  SIAM Journal on Computing, 4(1):69–76, 1975.
  * [16] Pavel Krčál and Radek Pelánek.  On sampled semantics of timed systems.  In Sundar Sarukkai and Sandeep Sen, editors, In Proc. of FSTTCS’05, volume 3821 of LNCS, pages 310–321. Springer, 2005.
  * [17] Dugald Macpherson.  A survey of homogeneous structures.  Discrete Mathematics, 311(15):1599–1634, 2011.
  * [18] Mojżesz Presburger.  Über der vollständigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchen die addition als einzige operation hervortritt.  Comptes Rendus Premier Congrès des Mathématicienes des Pays Slaves, 395:92–101, 1930.
  * [19] K. Quaas, M. Shirmohammadi, and J. Worrell.  Revisiting reachability in timed automata.  In Proc. of LICS’17, pages 1–12, June 2017.  doi:10.1109/LICS.2017.8005098.
  * [20] Eduardo D. Sontag.  Real addition and the polynomial hierarchy.  Information Processing Letters, 20(3):115–120, 1985.
  * [21] Ashutosh Trivedi and Dominik Wojtczak.  Recursive timed automata.  In Proc. ATVA’10, volume 6252 of LNCS, pages 306–324. Springer, 2010.
  * [22] Yuya Uezato and Yasuhiko Minamide.  Synchronized recursive timed automata.  In Proc. of LPAR’15, 2015.
  * [23] Kumar Neeraj Verma, Helmut Seidl, and Thomas Schwentick.  On the complexity of equational Horn clauses.  In Proc. CADE-20, 2005, pages 337–352, 2005.  doi:10.1007/11532231_25.
  * [24] Volker Weispfenning.  The complexity of linear problems in fields.  Journal of Symbolic Computation, 5(1):3–27, 1988.

##  Appendix A Appendix

###  A.1. Quantifier elimination

The following appeared as Lemma 2.1 in the main text. See 2.1

######  Proof A.1.

It suffices to consider a conjunctive formula of the form
$\varphi\equiv\exists y\cdot\varphi_{1}\wedge\varphi_{2}$ where $\varphi_{1}$
is a quantifier-free ${\cal A}_{1}$-formula and $\varphi_{2}$ is a quantifier-
free ${\cal A}_{2}$-formula. W.l.o.g. suppose $y$ is quantified over ${\cal
A}_{1}$. Since $y$ is a variable of the first sort, it does not appear free in
$\varphi_{2}$, and thus $\varphi\equiv(\exists
y\cdot\varphi_{1})\wedge\varphi_{2}$. By assumption that ${\cal A}_{1}$ admits
quantifier elimination, $\exists y\cdot\varphi_{1}$ is equivalent to a
quantifier free formula $\widetilde{\varphi}_{1}$, and thus the original
formula $\varphi$ is equivalent to $\widetilde{\varphi}_{1}\wedge\varphi_{2}$.
It is easy to see that the complexities combine as claimed.

Let $\left\ldbrack\varphi\right\rdbrack$ be the set of valuations satisfying
$\varphi$.

The following appeared as Lemma A.2 in the main text. See 2.2 We prove this by
splitting it in two claims.

######  Lemma A.2.

The structure ${\cal A}^{\mathrm{c}}_{\mathbb{N}}$ admits effective
elimination of quantifiers. The complexity is singly exponential for
conjunctive formulas.

######  Proof A.3.

We assume that all modulo statements are over the same modulus $m$. It
suffices to consider a conjunctive formula of the form

$\displaystyle\exists y\cdot\varphi\ \equiv\ \exists
y\cdot\bigwedge_{i}x_{i}+\alpha_{i}\leq y\leq x_{i}+\beta_{i}\ \wedge\
y\equiv_{m}x_{i}+\gamma_{i},$ (11)

where, for every $i$,
$\alpha_{i},\beta_{i}\in\mathbb{Z}\cup\left\\{-\infty,+\infty\right\\}$ with
$\alpha_{i}\leq\beta_{i}$, $\gamma_{i}\in\left\\{0,\dots,m-1\right\\}$, where
for uniformity of notation we assume $x_{0}=0,\alpha_{0}\geq 0$ in order to
model non-diagonal constraints on $y$. If not all $\alpha_{i}$’s are equal to
$-\infty$, then a satisfying $y$ will be of the form $x_{j}+\alpha_{j}+\delta$
with $\delta\in\left\\{0,\dots,m-1\right\\}$ where $j$ maximises
$x_{j}+\alpha_{j}$. We claim that the following quantifier free formula
$\widetilde{\varphi}$ is equivalent to (11):

$\displaystyle\bigvee_{\delta\in\left\\{0,\dots,m-1\right\\}}\bigvee_{j}\bigwedge_{i}x_{i}+\alpha_{i}\leq
x_{j}+\alpha_{j}+\delta\leq x_{i}+\beta_{i}\ \wedge\
x_{j}+\alpha_{j}+\delta\equiv_{m}x_{i}+\gamma_{i}.$ (12)

For the complexity claim, $\widetilde{\varphi}$ is exponentially bigger than
(11) when constants are encoded in binary. For the inclusion
$\left\ldbrack\widetilde{\varphi}\right\rdbrack\subseteq\left\ldbrack\exists
y\cdot\varphi\right\rdbrack$, let
$(a_{1},\dots,a_{n})\in\left\ldbrack\widetilde{\varphi}\right\rdbrack$. There
exist $\delta$ and $j$ as per (12), and thus taking
$a_{0}:=a_{j}+\alpha_{j}+\delta$ yields
$(a_{0},a_{1},\dots,a_{n})\in\left\ldbrack\exists
y\cdot\varphi\right\rdbrack$. For the other inclusion, let
$(a_{0},a_{1},\dots,a_{n})\in\left\ldbrack\varphi\right\rdbrack$. Let $j\neq
0$ be s.t. $a_{j}+\alpha_{j}$ is maximised, and define
$\delta:=a_{0}-(a_{j}+\alpha_{j})\mod m$. Clearly $\delta\geq 0$ since $a_{0}$
satisfies all the lower bounds $a_{i}+\alpha_{i}$. Since $a_{0}$ satisfies all
the upper bounds $a_{i}+\beta_{i}$ and $a_{j}+\alpha_{j}+\delta\leq a_{0}$,
upper bounds are also satisfied. Finally, since
$a_{0}\equiv_{m}a_{i}+\gamma_{i}$ and
$a_{0}\equiv_{m}a_{j}+\alpha_{j}+\delta$, we have that also the modular
constraints $a_{j}+\alpha_{j}+\delta\equiv_{m}a_{i}+\gamma_{i}$ are satisfied.
Thus, we have
$(a_{1},\dots,a_{n})\in\left\ldbrack\widetilde{\varphi}\right\rdbrack$, as
required.

If all $\alpha_{i}$’s are equal to $-\infty$, then there are no lower bound
constraints and only modulo constraints remain, hence and a satisfying $y$ (if
it exists) can be taken in the interval $\left\\{0,\dots,m-1\right\\}$,
yielding

$\displaystyle\bigvee_{\delta\in\left\\{0,\dots,m-1\right\\}}\bigwedge_{i}\
\delta\leq x_{i}+\beta_{i}\ \wedge\ \delta\equiv_{m}x_{i}+\gamma_{i}.$

The same complexity holds. The formula above is shown equivalent to (11) by a
reasoning as in the previous paragraph.

######  Lemma A.4.

The structure ${\cal A}^{\mathrm{c}}_{\mathbb{I}}$ admits effective
elimination of quantifiers. The complexity is quadratic for conjunctive
formulas.

######  Proof A.5.

It suffices to consider a conjunctive formula of the form
$\varphi\equiv\exists y\cdot\bigwedge_{k}\varphi_{k}$ where $\varphi_{k}$ are
atomic rational formulas. If any $\varphi_{k}$ is the constraint $y=0$, then
we obtain $\widetilde{\varphi}$ by replacing $y$ with $0$ everywhere.
Otherwise, $\varphi$ is of the form

$\displaystyle\exists y\cdot\bigwedge_{i\in I}{x_{i}}\leq
y\wedge\bigwedge_{j\in J}y\leq{x_{j}},$

and we can eliminate $y$ by writing the equivalent constraint
$\widetilde{\varphi}$

$\displaystyle\bigwedge_{i\in I}\bigwedge_{j\in J}{x_{i}}\leq{x_{j}}.$

The size of $\widetilde{\varphi}$ is quadratic in the size of $\varphi$.

###  A.2. Characterisation of the reachability relation

The following characterisation is used in the proof of Lemma 4.3.

######  Lemma A.6.

The relation $\stackrel{{\scriptstyle}}{{\leadsto}}_{\ell r}$ is the least
relation satisfying the following rules, for valuations
$\mu,\nu,\mu^{\prime},\nu^{\prime}:\mathbb{Q}^{X}$ and words
$w,u,v\in\Sigma^{*}$:

(input) $\displaystyle\frac{}{\mu\stackrel{{\scriptstyle a}}{{\leadsto}}_{\ell
r}\mu}\qquad$ $\displaystyle\textrm{ if
}\exists\langle\ell,a,r\rangle\in\Delta$ (test)
$\displaystyle\frac{}{\mu\stackrel{{\scriptstyle\varepsilon}}{{\leadsto}}_{\ell
r}\mu}\qquad$ $\displaystyle\textrm{ if
}\exists\langle\ell,\varphi,r\rangle\in\Delta{\;\cdot\;}\mu\models\varphi$
(reset)
$\displaystyle\frac{}{\mu\stackrel{{\scriptstyle\varepsilon}}{{\leadsto}}_{\ell
r}\mu[Y\mapsto 0]}\qquad$ $\displaystyle\textrm{ if
}\exists\langle\ell,\mathsf{reset}(Y),r\rangle\in\Delta$ (elapse)
$\displaystyle\frac{}{\mu\stackrel{{\scriptstyle\varepsilon}}{{\leadsto}}_{\ell
r}\nu}\qquad$ $\displaystyle\textrm{ if
}\exists\langle\ell,\mathsf{elapse},r\rangle\in\Delta,\delta>0{\;\cdot\;}\nu=\left\\{\mu+\delta\right\\}$
(push-pop) $\displaystyle\frac{\mu\stackrel{{\scriptstyle
w}}{{\leadsto}}_{\ell^{\prime}r^{\prime}}\nu}{\mu\stackrel{{\scriptstyle
w}}{{\leadsto}}_{\ell r}\nu}\qquad$ if (15) (transitivity)
$\displaystyle\frac{\mu\stackrel{{\scriptstyle
u}}{{\leadsto}}_{\ell\ell^{\prime}}\mu^{\prime}\
\mu^{\prime}\stackrel{{\scriptstyle
v}}{{\leadsto}}_{\ell^{\prime}r}\nu}{\mu\stackrel{{\scriptstyle
uv}}{{\leadsto}}_{\ell r}\nu}$
$\displaystyle\bigvee_{\begin{subarray}{c}\langle\ell,{\mathsf{push}(\gamma:\psi_{\mathsf{push}})},\ell^{\prime}\rangle,\\\
\langle
r^{\prime},{\mathsf{pop}(\gamma:\psi_{\mathsf{pop}})},r\rangle\in\Delta\end{subarray}}\exists\mu_{Z}\in\mathbb{Q}_{\geq
0}^{Z},\exists\delta\in\mathbb{Q}_{\geq
0}{\;\cdot\;}\left\\{\begin{array}[]{l}(\mu,\mu_{Z})\models\psi_{\mathsf{push}}(\overline{x},\overline{z})\
\wedge\\\
(\nu,\mu_{Z}+\delta)\models\psi_{\mathsf{pop}}(\overline{x},\overline{z}).\end{array}\right.$
(15)

###  A.3. Missing details for (A) push-copy

Let $\Xi$ be the set of all
$\xi_{\psi_{\mathsf{push}},\psi_{\mathsf{pop}}}$’s. Let the original tpda be
$\mathcal{P}=(\Sigma,\Gamma,L,X,Z,\Delta)$, let $\Psi_{\mathsf{push}}$ be the
set of all push constraints $\psi_{\mathsf{push}}$ of $\mathcal{P}$, and let
$\Psi_{\mathsf{pop}}$ be the set of all pop constraints $\psi_{\mathsf{pop}}$
of $\mathcal{P}$. We construct an equivalent tpda
$\mathcal{P}^{\prime}=(\Sigma,\Gamma^{\prime},L,X,Z^{\prime},\Delta^{\prime})$
which only pushes on the stack copies of stack clocks. Let
$\Gamma^{\prime}=\Gamma\times\Xi$, $Z^{\prime}=\left\\{z_{x}\;\middle|\;x\in
X\right\\}$, and transitions in $\Delta^{\prime}$ are determined as follows.

Every input, test, time elapse, and clock reset transitions in $\mathcal{P}$
generate identical transitions in $\mathcal{P}^{\prime}$. For every push
transition $\langle\ell,{\mathsf{push}(\alpha:\psi_{\mathsf{push}})},r\rangle$
in $\mathcal{P}$, we have a push transition in $\mathcal{P}^{\prime}$ of the
form

$\displaystyle\langle\ell,{\mathsf{push}(\left\langle\alpha,\xi_{\psi_{\mathsf{push}},\psi_{\mathsf{pop}}}\right\rangle:\psi_{\mathsf{copy}}\wedge
z_{0}=0)},r\rangle$

($z_{0}=0$ is compatible with push-copy by adding a new clock $x_{0}$ which is
$0$ at the time of push and using $z_{0}=x_{0}$; we avoid this for simplicity)
for every guessed pop constraint $\psi_{\mathsf{pop}}\in\Psi_{\mathsf{pop}}$
of $\mathcal{P}$ and corresponding new pop constraint
$\xi_{\psi_{\mathsf{push}},\psi_{\mathsf{pop}}}\in\Xi$ and where
$\psi_{\mathsf{copy}}$ is as in (3). Finally, for every pop transition
$\langle\ell,{\mathsf{pop}(\alpha:\psi_{\mathsf{pop}})},r\rangle$ in
$\mathcal{P}$ and for every potential push constraint
$\psi_{\mathsf{push}}\in\Psi_{\mathsf{push}}$, we have a pop transition in
$\mathcal{P}^{\prime}$

$\displaystyle\langle\ell,{\mathsf{pop}(\left\langle\alpha,\xi_{\psi_{\mathsf{push}},\psi_{\mathsf{pop}}}\right\rangle:\xi_{\psi_{\mathsf{push}},\psi_{\mathsf{pop}}})},r\rangle$

which checks that the pop constraint $\psi_{\mathsf{pop}}$ was indeed
correctly guessed.

This translation preserves the reachability relation. The following appeared
as Lemma 4.3 in the main text. See 4.3

######  Proof A.7.

We prove

$\mu\stackrel{{\scriptstyle w}}{{\leadsto}}_{\ell
r}\nu\quad\Leftrightarrow\quad\mu\stackrel{{\scriptstyle
w}}{{\leadsto}}^{\prime}_{\ell r}\nu$

by induction on the length of derivations, following the characterisation of
Lemma A.6. Let $\mu\stackrel{{\scriptstyle w}}{{\leadsto}}_{\ell r}\nu$ (the
other direction is proved analogously). Since all transitions are the same
except push and pop transitions, it suffices to prove it for matching pairs of
push-pop transitions. By (15), there exist transitions
$\langle\ell,{\mathsf{push}(\gamma:\psi_{\mathsf{push}})},\ell^{\prime}\rangle,\langle
r^{\prime},{\mathsf{pop}(\gamma:\psi_{\mathsf{pop}})},r\rangle\in\Delta$, a
stack clock valuation $\mu_{Z}\in\mathbb{Q}_{\geq 0}^{Z}$, and a time elapse
$\delta\in\mathbb{Q}_{\geq 0}$ s.t.
$(\mu,\mu_{Z})\models\psi_{\mathsf{push}}(\overline{x},\overline{z})$,
$(\nu,\mu_{Z}+\delta)\models\psi_{\mathsf{pop}}(\overline{x}^{\prime},\overline{z}^{\prime})$,
and $\mu\stackrel{{\scriptstyle w}}{{\leadsto}}_{\ell^{\prime}r^{\prime}}\nu$
in $\mathcal{P}$. By inductive hypothesis, $\mu\stackrel{{\scriptstyle
w}}{{\leadsto}}_{\ell^{\prime}r^{\prime}}^{\prime}\nu$ in
$\mathcal{P}^{\prime}$. By construction, $\mathcal{P}^{\prime}$ has matching
transitions
$\langle\ell,{\mathsf{push}(\left\langle\gamma,\xi_{\psi_{\mathsf{push}},\psi_{\mathsf{pop}}}\right\rangle:\psi_{\mathsf{copy}})},\ell^{\prime}\rangle$
and $\langle
r^{\prime},{\mathsf{pop}(\left\langle\gamma,\xi_{\psi_{\mathsf{push}},\psi_{\mathsf{pop}}}\right\rangle:\xi_{\psi_{\mathsf{push}},\psi_{\mathsf{pop}}})},r\rangle$.
Clearly,
$(\mu,\mu)\models\psi_{\mathsf{copy}}(\overline{x},\overline{z}_{\overline{x}})$,
where $z_{x}$ is the stack clock copying the value of clock $x$ at the time of
push. Since stack clock $z_{0}$ was initially $0$, we have that its value at
the end is exactly $\delta$. We show that

$(\overline{x}^{\prime}:\nu,\overline{z}^{\prime}_{\overline{x}}:\mu+\delta)\models\xi_{\psi_{\mathsf{push}},\psi_{\mathsf{pop}}}(\overline{x}^{\prime},\overline{z}^{\prime}_{\overline{x}}),$

thus showing $\mu\stackrel{{\scriptstyle
w}}{{\leadsto}}_{\ell^{\prime}r^{\prime}}^{\prime}\nu$ in
$\mathcal{P}^{\prime}$ by (15). By its definition,
$\xi_{\psi_{\mathsf{push}},\psi_{\mathsf{pop}}}(\overline{x}^{\prime},\overline{z}^{\prime}_{\overline{x}})$
is equivalent to
$\psi_{\mathsf{pop}}^{\prime}(\overline{x}^{\prime},\overline{z}^{\prime}_{\overline{x}})$
from (5). Take $\mu_{Z}+\delta$ as the valuation for $\overline{z}^{\prime}$,
and we have

$(\overline{x}^{\prime}:\nu,\overline{z}^{\prime}:\mu_{Z}+\delta,\overline{z}^{\prime}_{\overline{x}}:\mu+\delta)\models\psi_{\mathsf{push}}(\overline{z}^{\prime}_{\overline{x}}-\overline{\delta},\overline{z}^{\prime}-\overline{\delta})\wedge\psi_{\mathsf{pop}}(\overline{x}^{\prime},\overline{z}^{\prime})$

because
$(\overline{x}^{\prime}:\nu,\overline{z}^{\prime}:\mu_{Z}+\delta)\models\psi_{\mathsf{pop}}(\overline{x}^{\prime},\overline{z}^{\prime})$
and
$(\overline{z}_{\overline{x}}:\mu,\overline{z}:\mu_{Z})\models\psi_{\mathsf{push}}(z_{\overline{x}},\overline{z})$.

###  A.4. (B) The tpda is pop-integer-free

The aim of this section is to remove integer constraints from pop transitions.
Thanks to (A), we assume that the tpda is push-copy. Since diagonal integer
constraints can simulate non-diagonal ones, we can further assume that pop
transitions do not contain non-diagonal integer constraints (i.e., of the form
$\lfloor z\rfloor\leq k$), and thus we only need to eliminate the diagonal
ones.

Let $\mathcal{P}$ be a push-copy tpda. By Remark 3.2, we replace integer pop
constraints of the form ${\lfloor x\rfloor-\lfloor z_{y}\rfloor\leq k}$,
${\lfloor z_{x}\rfloor-\lfloor z_{y}\rfloor\leq k}$ by _classical_
${x-z_{y}\leq k}$, resp., $z_{x}-z_{y}\leq k$, and fractional constraints.
This has the advantage that classical diagonal constraints are invariant under
time elapse, which will simplify the construction below. Pop constraints of
the form $z_{y}-z_{x}\sim k$ can easily be eliminated since, thanks to push-
copy, they can be checked at the time of push as the _transition_ constraint
$y-x\sim k$. Thus, we concentrate on pop constraints

$\displaystyle\psi_{\mathsf{pop}}\ \equiv\
\psi^{\textrm{c}}_{1}\wedge\cdots\wedge\psi^{\textrm{c}}_{m}\wedge\psi^{\textrm{nc}}$
(16)

where the $\psi^{\textrm{c}}_{i}$’s are classical diagonal constraints of the
form ${y-z_{x}\sim k}$, with ${\sim\;\in\\!\left\\{<,\leq,\geq,>\right\\}}$,
and $\psi^{\textrm{nc}}$ contains only non-classical (i.e., modular and
fractional) constraints. Let be $\mathcal{C}$ the set of all
$\psi^{\textrm{c}}_{i}$’s. Constraints $y-z_{x}\sim k$ are eliminated by
introducing linearly many new global clocks (one for each atomic clock
constraint) satisfying suitable conditions at the time of push. Thus, in the
new automaton pop constraints are only of the form $\psi^{\textrm{nc}}$, i.e.,
modulo and fractional, as required. The construction is similar to [9].
Control states of the new automaton $\mathcal{P}^{\prime}$ are of the form
$\left\langle\ell,T,\Phi^{-},\Phi^{+}\right\rangle$, where $T$ is a set of
clocks and $\Phi^{-},\Phi^{+}$ are sets of atomic constraints. Thus, from a
complexity standpoint, the number of control locations of
$\mathcal{P}^{\prime}$ is exponential in the number of clocks and constraints,
and the size of the stack alphabet is exponential in the number of
constraints.

######  Lemma A.8.

Let the reachability relation of $\mathcal{P}^{\prime}$ be expressed by the
formula $\varphi_{\ell^{\prime}r^{\prime}}$. The reachability relation of
$\mathcal{P}$ is expressed by
$\bigvee\left\\{\varphi_{\left\langle\ell,T,\emptyset,\emptyset\right\rangle\left\langle
r,\emptyset,\Phi^{-},\Phi^{+}\right\rangle}\;\middle|\;T\subseteq
X,\Phi^{-},\Phi^{+}\subseteq\mathcal{C}\right\\}$.

######  Proof A.9.

Let $\mathcal{P}$ be a push-copy tpda $(\Sigma,\Gamma,L,X,Z,\Delta)$. Let
$\mathcal{C}^{-}/\mathcal{C}^{+}$ be the set of all lower/upper bound
classical pop constraints of the form $y-z_{x}\geq k,y-z_{x}>k$, or, resp.,
$y-z_{x}\leq k,y-z_{x}<k$, and let
$\mathcal{C}=\mathcal{C}^{-}\cup\mathcal{C}^{+}$. We construct a tpda
$\mathcal{P}^{\prime}=(\Sigma,\Gamma^{\prime},L^{\prime},X^{\prime},Z,\Delta^{\prime})$
with the same set of stack clocks as $\mathcal{P}$, and with global clocks
being those of $\mathcal{P}$, plus a copy of each global clock for each
lower/upper bound constraint:
$X^{\prime}:=X\cup\left\\{x_{\psi}\;\middle|\;\psi\in\mathcal{C}\right\\}$. A
control location of $\mathcal{P}^{\prime}$ is of the form
$(\ell,T,\Phi^{-},\Phi^{+})\in L^{\prime}$, where

  * •

$\ell$ is a control location of $\mathcal{P}$,

  * •

$T\subseteq X$ is a set of clocks of $\mathcal{P}$ which cannot be reset till
the next push (this is used to guess and check last resets before a push), and

  * •

$\Phi^{-}\\!\subseteq\\!\mathcal{C}^{-},\Phi^{+}\\!\subseteq\\!\mathcal{C}^{+}$
are the currently _active_ lower/upper bound constraints.

The new stack alphabet $\Gamma^{\prime}$ consists of tuples of the form
$\left\langle\alpha,\Phi^{-},\Phi^{+}\right\rangle$ with $\alpha\in\Gamma$ a
stack symbol of $\mathcal{P}$ and $\Phi^{-},\Phi^{+}$ as above.

Let $\langle\ell,\mathsf{op},r\rangle$ be a transition in $\mathcal{P}$. If it
is either an input $\mathsf{op}=a\in\Sigma_{\varepsilon}$, test
$\mathsf{op}=\varphi$, or time elapse $\mathsf{op}=\mathsf{elapse}$
transition, then it generates corresponding transitions in $\mathcal{P}$ of
the form
${\langle(\ell,T,\Phi^{-},\Phi^{+}),\mathsf{op},(r,T,\Phi^{-},\Phi^{+})\rangle}$
for every choice of $T,\Phi^{-},\Phi^{+}$. A reset transition
$\mathsf{op}=\mathsf{reset}(Y)$ generates several reset transitions of the
form

${\langle(\ell,T,\Phi^{-},\Phi^{+}),\mathsf{reset}(Y\cup Y^{\prime}),(r,T\cup
U,\Phi^{-}\cup\Psi^{-},\Phi^{+}\cup\Psi^{+})\rangle}$

whenever

  1. (1)

$Y\cap T=\emptyset$ (no forbidden clock is reset),

  2. (2)

$U\subseteq Y$ is a subset of reset clocks which are guessed to be reset for
the last time till the next push,

  3. (3)

$\Psi^{-}\subseteq\bigcup_{x\in U}\mathcal{C}^{-}_{x}\setminus\Phi^{-}$ is a
new set of lower bound constraints involving newly reset clocks in $U$,
similarly

  4. (4)

$\Psi^{+}\subseteq\bigcup_{x\in U}\mathcal{C}^{+}_{x}\setminus\Phi^{+}$
likewise for the upper bound constraints, and finally

  5. (5)

$Y^{\prime}\subseteq\left\\{x_{\psi}\;\middle|\;\psi\in\mathcal{C}\right\\}$
contains all clocks relating to _new_ active lower bound constraints, and all
clocks relating to (new or not) active upper bound constraints w.r.t. clocks
$Y$ reset in this transition:

$\displaystyle Y^{\prime}$
$\displaystyle=\left\\{x_{\varphi}\;\middle|\;\varphi\in\Psi^{-}\textrm{ or
}\varphi\in\Phi^{+}_{Y}\cup\Psi^{+}\right\\},\textrm{ where }$
$\displaystyle\Phi^{+}_{Y}$ $\displaystyle=\left\\{(y-z_{x}\lesssim
k)\in\Phi^{+}\;\middle|\;x\in Y\right\\}.$

A push transition $\mathsf{op}={\mathsf{push}(\alpha:\psi_{\mathsf{copy}})}$
(where $\psi_{\mathsf{copy}}$ is defined in (3)), generates a transition in
$\mathcal{P}^{\prime}$ of the form

$\displaystyle\langle(\ell,T,\Phi^{-},\Phi^{+}),{\mathsf{push}(\left\langle\alpha,\Phi^{-},\Phi^{+}\right\rangle:\psi_{\mathsf{copy}})},(r,T^{\prime},\Phi^{-},\Phi^{+})\rangle$

only if $T=X$, i.e., all clocks were correctly guessed to be reset for the
last time till this push, and for every set of clocks $T^{\prime}\subseteq X$
which are guessed not to be reset till the _next_ push. Moreover, we push on
the stack the current set of guessed constraints $\Phi^{-},\Phi^{+}$. Finally,
a pop transition $\mathsf{op}=\mathsf{pop}(\alpha\models\psi_{\mathsf{pop}})$
of $\mathcal{P}$ with $\psi_{\mathsf{pop}}$ as in (16), generates in
$\mathcal{P}^{\prime}$ a test followed by a pop transition of the form
(omitting the intermediate state)

$\displaystyle\langle(\ell,T,\Phi^{-},\Phi^{+}),\ \widetilde{\psi};\
{\mathsf{pop}(\left\langle\alpha,\hat{\Phi}^{-},\hat{\Phi}^{+}\right\rangle:\psi^{\textrm{nc}})},\
(r,T,\hat{\Phi}^{-},\hat{\Phi}^{+})\rangle$

for every $T\subseteq X$, $\hat{\Phi}^{-}\subseteq\mathcal{C}^{-}$,
$\hat{\Phi}^{+}\subseteq\mathcal{C}^{+}$, whenever
$\Phi^{-}\cup\Phi^{+}=\left\\{\psi^{\textrm{c}}_{1}\wedge\cdots\wedge\psi^{\textrm{c}}_{m}\right\\}$,
i.e., the guess of upper and lower bounds was indeed correct, and where
$\widetilde{\psi}$ is defined as $\widetilde{\psi}\ \equiv\
\bigwedge\left\\{y-x_{\psi^{\textrm{c}}_{i}}\sim
k\;\middle|\;\psi^{\textrm{c}}_{i}\in\Phi^{-}\cup\Phi^{+},\psi^{\textrm{c}}_{i}\equiv
y-z_{x}\sim k\right\\}.$ We have removed pop integer constraints
$\psi^{\textrm{c}}_{i}$’s by introducing classical constraints in
$\widetilde{\psi}$, and the latter can be converted into integer and
fractional constraints according to Remark 3.2. Notice that the stack non-
classical constraint $\psi^{\textrm{nc}}$ is preserved from $\mathcal{P}$ to
$\mathcal{P}^{\prime}$. Thus, we obtain a pop-integer-free tpda, as required.

The number of control locations of $\mathcal{P}^{\prime}$ is
$|{L^{\prime}}|=|{L}|\cdot 2^{|{X}|}\cdot 2^{2\cdot|{\mathcal{C}}|}$, the
number of stack symbols of $\mathcal{P}^{\prime}$ is
$|{\Gamma^{\prime}}|=|{\Gamma}|\cdot 2^{2\cdot|{\mathcal{C}}|}$, and the
number of clocks of $\mathcal{P}^{\prime}$ is
$|{X^{\prime}}|=|{X}|+|{\mathcal{C}}|$. Thus, $\mathcal{P}^{\prime}$ has
number of control locations and stack symbols exponential in the size of
$\mathcal{P}$, and number of clocks linear in the size of $\mathcal{P}$.

The construction can be proved correct by the same argument for stack
classical constraints as in [6], except that now non-classical stack
constraints (not considered in [6]) are kept unchanged.

###  A.5. Missing details for (C) fractional

Recall the structure of fractional values ${\cal
A}^{\mathrm{c}}_{\mathbb{I}}=(\mathbb{I},\leq,0)$. An _automorphism_ of ${\cal
A}^{\mathrm{c}}_{\mathbb{I}}$ is a bijection $\alpha$ s.t. $\alpha(0)=0$ and
$a\leq b$ iff $\alpha(a)\leq\alpha(b)$; in other words, $0$ is fixed, but
otherwise distances can be stretched or compressed monotonically. The set
$\mathbb{I}^{X}$ of (fractional parts of) clock valuations splits into
finitely many _orbits_ , where $u,v\in\mathbb{I}^{n}$ are in the same orbit if
some automorphism of ${\cal A}^{\mathrm{c}}_{\mathbb{I}}$ maps $u$ to $v$.
Note that an orbit $o$ is determined by the order of elements, their equality
type, and their equalities with $0$; hence the number of orbits is exponential
in $|{X}|$. For an orbit $o$, let its _characteristic formula_ be the
following quantifier-free $(\mathbb{I},\leq,0)$ formula

$\displaystyle\varphi_{o}(\overline{x})\equiv\bigwedge_{\tilde{a}_{i}=0}x_{i}=0\wedge\bigwedge_{\tilde{a}_{i}\leq\tilde{a}_{j}}x_{i}\leq
x_{j},$ (17)

where $(\tilde{a}_{1},\dots,\tilde{a}_{n})$ is any fixed element of $o$ (by
the definition of orbit, $\varphi_{o}$ does not depend on the choice of
representative).

Let $\mathcal{P}=(\Sigma,\Gamma,L,X,Z,\Delta)$ be a push-copy and pop-integer-
free tpda. We build a fractional tpda
$\mathcal{P}^{\prime}=(\Sigma^{\prime},\Gamma^{\prime},L^{\prime},X,Z,\Delta^{\prime})$
where $\Sigma^{\prime}$ equals $\Sigma$ extended with an extra symbol
$\checkmark_{\\!\\!x}\not\in\Sigma$ for every clock $x$ of $\mathcal{P}$,
$\Gamma^{\prime}=\Gamma\times\Lambda_{M}$ extends $\Gamma$ by recording the
$M$-unary equivalence class of clocks which are pushed on the stack, and
$L^{\prime}=L\times\Lambda_{M}\times 2^{X}\cup L_{\bullet}$, where $Y_{1}\in
2^{X}$ is the set of clocks which are _not_ allowed to be reset any more in
the future, and $L_{\bullet}$ contains some extra control locations used in
the simulation. Every transition $\langle\ell,\mathsf{op},r\rangle\in\Delta$
generates one or more transitions in $\Delta^{\prime}$ according to
$\mathsf{op}$. If $\mathsf{op}=a\in\Sigma_{\varepsilon}$ is an input
transition, then $\Delta^{\prime}$ contains a corresponding input transition
$\langle\left\langle\ell,\lambda,Y_{1}\right\rangle,a,\left\langle
r,\lambda,Y_{1}\right\rangle\rangle$, for every choice of $\lambda,Y_{1}$. If
$\mathsf{op}=\varphi$ is a test transition, then $\Delta^{\prime}$ contains a
corresponding test transition

$\langle\left\langle\ell,\lambda,Y_{1}\right\rangle,\left.\varphi\right|_{\lambda},\left\langle
r,\lambda,Y_{1}\right\rangle\rangle,$

where $\left.\varphi\right|_{\lambda}$ contains only fractional constraints.
If $\mathsf{op}=\mathsf{reset}(Y)$ is a reset transition, then
$\Delta^{\prime}$ contains a reset transition

$\langle\left\langle\ell,\lambda,Y_{1}\right\rangle,\mathsf{reset}(Y),\left\langle
r,\lambda[Y\mapsto 0],Y_{1}\cup Y_{2}\right\rangle\rangle$

provided that $Y\subseteq X\setminus Y_{1}$ (no forbidden clocks are reset),
and where $Y_{2}\subseteq Y$ are declared to be reset now for the last time.
If $\mathsf{op}=\mathsf{elapse}$ is a time elapse transition, then we have the
following 4 groups of transitions:

  1. (1)

First, we silently go to control location
$\left\langle\ell,\lambda,Y_{1},1\right\rangle$ to start the simulation:

$\displaystyle\langle\left\langle\ell,\lambda,Y_{1}\right\rangle,\varepsilon,\left\langle\ell,\lambda,Y_{1},1\right\rangle\rangle.$

  2. (2)

We test that the current orbit of fractional values is $o$, we let time
elapse, and then we test that the new orbit is $o^{\prime}$. We can
reconstruct the set of clocks $Y_{o,o^{\prime}}$ which have just overflown and
for which we need to update their unary abstraction as
$Y_{o,o^{\prime}}=\left\\{x\in X\;\middle|\;o(x)>0\textrm{ and
}o^{\prime}(x)=0\right\\}$. This yields the following sequence of transitions,
where we omit the intermediate states for conciseness:

$\displaystyle\langle\left\langle\ell,\lambda,Y_{1},1\right\rangle,(\varphi_{o};\mathsf{elapse};\varphi_{o^{\prime}}),\left\langle\ell,\lambda,Y_{1},Y_{o,o^{\prime}},2\right\rangle\rangle.$

  3. (3)

For each clock that needs to be updated in $Y_{o,o^{\prime}}$, we increment
its unary abstraction one by one, and we optionally emit a tick if this clock
was guessed not to be reset anymore in the future:

$\displaystyle\langle\left\langle\ell,\lambda,Y_{1},Y_{2},2\right\rangle,\checkmark_{\\!\\!x}^{?},\left\langle\ell,\lambda[x\mapsto
x+1],Y_{1},Y_{2}\setminus\left\\{x\right\\},2\right\rangle\rangle,$

where $\checkmark_{\\!\\!x}^{?}$ equals $\checkmark_{\\!\\!x}$ if $x\in
Y_{2}\cap Y_{1}$, and $\varepsilon$ if $x\in Y_{2}\setminus Y_{1}$.

  4. (4)

When the unary class of all overflown clocks has been updated, we either
return to the beginning of the simulation (in order to simulate longer elapses
of time), or we quit:

$\displaystyle\langle\left\langle\ell,\lambda,Y_{1},\emptyset,2\right\rangle,\varepsilon,\left\langle\ell,\lambda,Y_{1},1\right\rangle\rangle,\quad\langle\left\langle\ell,\lambda,Y_{1},\emptyset,2\right\rangle,\varepsilon,\left\langle
r,\lambda,Y_{1}\right\rangle\rangle.$

If $\mathsf{op}={\mathsf{push}(\alpha:\psi_{\mathsf{copy}})}$ is a push-copy
transition, then $\Delta^{\prime}$ contains a push transition copying only the
fractional parts and the unary class of global clocks:

$\langle\left\langle\ell,\lambda,Y_{1}\right\rangle,{\mathsf{push}(\left\langle\alpha,\lambda\right\rangle:\bigwedge_{x\in
X}\left\\{z_{0}\right\\}=0\wedge\left\\{z_{x}\right\\}=\left\\{x\right\\})},\left\langle
r,\lambda,Y_{1}\right\rangle\rangle.$

If $\mathsf{op}={\mathsf{pop}(\alpha:\psi)}$ is a pop-integer-free transition,
then $\Delta^{\prime}$ contains a fractional pop transition of the form

$\langle\left\langle\ell,\lambda_{\mathsf{pop}},Y_{1}\right\rangle,{\mathsf{pop}(\left\langle\alpha,\lambda_{\mathsf{push}}\right\rangle:\left.\psi\right|_{\lambda_{\mathsf{push}},\lambda_{\mathsf{pop}}})},\left\langle
r,\lambda_{\mathsf{pop}},Y_{1}\right\rangle\rangle.$

We eliminated all occurrences of $\lfloor x\rfloor$ both from transition and
push/pop stack constraints. Thus, transition and stack constraints of
$\mathcal{P}^{\prime}$ are only fractional.

##### Reconstruction of the reachability relation.

We reconstruct the reachability relation of $\mathcal{P}$ from that of
$\mathcal{P}^{\prime}$ as follows. The reachability relation
$\stackrel{{\scriptstyle}}{{\leadsto}}_{\ell r}$ of $\mathcal{P}$ is expressed
as the $\L_{\mathbb{Z},\mathbb{Q}}$ formula

$\displaystyle\varphi_{\ell
r}(\lfloor\overline{x}\rfloor,\left\\{\overline{x}\right\\},\overline{f},\lfloor\overline{x}^{\prime}\rfloor,\left\\{\overline{x}^{\prime}\right\\})$
$\displaystyle\ \equiv\
\bigvee_{\lambda,Y,\mu}\exists\overline{g}\cdot\varphi_{\lambda}(\lfloor\overline{x}\rfloor)\wedge\varphi_{\textrm{step}}\wedge\varphi_{\textrm{end}},\textrm{
where }$ $\displaystyle\varphi_{\textrm{step}}$ $\displaystyle\ \equiv\
\psi_{\left\langle\ell,\lambda,Y\right\rangle\left\langle
r,\mu,X\right\rangle}(\left\\{\overline{x}\right\\},(\overline{f},\overline{g}),\left\\{\overline{x}^{\prime}\right\\})$
$\displaystyle\varphi_{\textrm{end}}$ $\displaystyle\ \equiv\ \bigwedge_{x\in
Y}\lfloor x^{\prime}\rfloor=\lfloor x\rfloor+g_{x}\wedge\bigwedge_{x\not\in
Y}\lfloor x^{\prime}\rfloor=g_{x}.$

  * •

The formula $\varphi_{\lambda}$ ensures that the initial integer value of
clocks has the same unary class as prescribed by $\lambda$.

  * •

The formula $\varphi_{\textrm{step}}$ invokes the fractional reachability
relation of $\mathcal{P}^{\prime}$ where $g_{x}$ counts the number of marks
$\checkmark_{\\!\\!x}$ since clock $x$ was last reset.

  * •

The formula $\varphi_{\textrm{end}}$ uniquely determines the final integer
values $\lfloor x^{\prime}\rfloor$ of all clocks of $\mathcal{P}$: For those
clocks $x\not\in Y$ which are ever reset during the run, the final value of
its integer part $\lfloor x^{\prime}\rfloor$ equals the integer time $g_{x}$
that elapsed since the last reset; for those clocks $x\in Y$ which are not
reset during the run, $\lfloor x^{\prime}\rfloor$ equals their initial value
plus the time elapsed since the beginning.

We can eliminate the existential quantification on $\overline{g}$ from the
formula above by noticing that $\varphi_{\textrm{end}}$ uniquely determines
$\overline{g}$ as a function of
$\lfloor\overline{x}\rfloor,\lfloor\overline{x}^{\prime}\rfloor$ and $Y$, thus
obtaining the equivalent $\L_{\mathbb{Z},\mathbb{Q}}$ formula in the following
lemma. The following appeared as Lemma 4.4 in the main text. See 4.4 In the
statement above, $\overline{g}^{Y}$ is defined as follows:

$\displaystyle g^{Y}_{x}\equiv\left\\{\begin{array}[]{ll}\lfloor
x^{\prime}\rfloor-\lfloor x\rfloor&\textrm{ if }x\in Y\\\ \lfloor
x^{\prime}\rfloor&\textrm{ otherwise}.\end{array}\right.$

###  A.6. Missing proofs from Sec. 5

The following appeared as Lemma 5.3 in the main text. See 5.3

######  Proof A.10.

This is a special case of the following general fact: An equivariant orbit-
finite pda over homogeneous atoms can be transformed into an equivariant
orbit-finite context-free grammar (see [4, 8]). For concreteness, we provide
the productions of the grammar. For $o\in\mathrm{Orb}(\mathbb{I}^{X\times
X^{\prime}})$ we write $o_{1}$ (resp. $o_{2}$) for the projections of $o$ on
the first (resp. last) $k$ coordinates. For every input transition
$\langle\ell,a,r\rangle$ and $o$ s.t. $o_{1}=o_{2}$ we have in the grammar a
production

(input) $\displaystyle\qquad X_{\ell ro}\leftarrow a.$ For every global
transition rule $\langle\ell,\varphi,r\rangle$ and $o$ s.t. $o\models\varphi$
we have a production (global) $\displaystyle\qquad X_{\ell
ro}\leftarrow\varepsilon.$ For an orbit
$o\in\mathrm{Orb}(\mathbb{I}^{X_{1}\times X_{2}\times X_{3}})$ and
$i,j\in\left\\{1,2,3\right\\}$, denote by
$o_{ij}\in\mathrm{Orb}(\mathbb{I}^{X_{i}\times X_{j}})$ the projection of $o$
to ($k$-ary) components $i,j$. For every orbit
$o\in\mathrm{Orb}(\mathbb{I}^{X\times X^{\prime}\times X^{\prime\prime}})$ we
have a production (transitivity) $\displaystyle\qquad X_{\ell
ro_{13}}\leftarrow X_{\ell\ell^{\prime}o_{12}}\cdot X_{\ell^{\prime}ro_{23}}.$
Finally, for every pair of transitions
$\langle\ell,\mathsf{push}(\gamma\models\varphi),\ell^{\prime}\rangle,\langle
r^{\prime},\mathsf{pop}(\gamma\models\psi),r\rangle\in\Delta$ and orbit
$o\in\mathrm{Orb}(\mathbb{I}^{X\times X^{\prime}\times Z})$ s.t.
$o_{13}\models\varphi$ and $o_{23}\models\psi$, we have a production (push-
pop) $\displaystyle\qquad X_{\ell ro_{12}}\leftarrow
X_{\ell^{\prime}r^{\prime}o_{12}}.$

####  A.6.1. Correctness of the construction

We argue that $\mathcal{Q}$ and $\mathcal{P}$ faithfully simulate each other
by providing a variant of strong bisimulation between their configurations. A
configuration $\left\langle\ell,\mu,u\right\rangle$ of $\mathcal{P}$ _is
consistent with_ a configuration $\left\langle r,\nu,v\right\rangle$ of
$\mathcal{Q}$, if

  * •

they have the same control locations $\ell=r$,

  * •

every global clock $x$ and the corresponding register $\hat{x}$ satisfy
$\left\\{\mu(x)\right\\}=\nu(\hat{x}_{0})\ominus\nu(\hat{x})$,

  * •

$u=(\gamma_{1},\mu_{1})\cdots(\gamma_{n},\mu_{n})$,
$v=(\gamma_{1},\nu_{1})\cdots(\gamma_{n},\nu_{n})$ and, for every $1\leq i\leq
n$, stack clock $z$ and corresponding register $\hat{z}$, we have
$\left\\{\mu_{i}(z)\right\\}=\nu(\hat{x}_{0})\ominus\nu_{i}(\hat{z})$.

The consistency is not one-to-one, for two reasons: on the side of
$\mathcal{P}$ the integer parts of clocks are irrelevant and hence can be
arbitrary; and on the side of $\mathcal{Q}$ the configuration is unique only
up to cyclic shift.

A configuration $\left\langle r,\nu,v\right\rangle$ (of $\mathcal{P}$ or
$\mathcal{Q}$) is an _$a$ -successor_ of $\left\langle\ell,\mu,u\right\rangle$
if $\left\langle\ell,\mu,u\right\rangle\xrightarrow{a}\left\langle
r,\nu,v\right\rangle$ (in $\mathcal{P}$ or $\mathcal{Q}$, resp.); in
$\mathcal{P}$, additionally, if $a\in\mathbb{Q}_{\geq 0}$, then we call
$\left\langle r,\nu,v\right\rangle$ an $\varepsilon$-successor of
$\left\langle\ell,\mu,u\right\rangle$. By inspection of the construction of
$\mathcal{Q}$ we deduce:

######  Claim 1.

Every configuration of $\mathcal{P}$ (resp. $\mathcal{Q}$) is consistent with
some configuration of $\mathcal{Q}$ (resp. $\mathcal{P}$). Moreover, for every
pair of consistent configurations of $\mathcal{P}$ and $\mathcal{Q}$,
respectively, and $a\in\Sigma_{\varepsilon}$, every $a$-successor of one of
the configurations is consistent with exactly one $a$-successor of the other
one.

Thus, once a pair of consistent configurations is fixed, the $a$-successors in
$\mathcal{P}$ and $\mathcal{Q}$ are in a one-to-one correspondence. For the
correctness of (10) in Sec. 5 observe that a configuration
$\left\langle\ell,\mu,\varepsilon\right\rangle$ of $\mathcal{P}$ and a
configuration $\left\langle\ell,\nu,\varepsilon\right\rangle$ of $\mathcal{Q}$
are consistent if, and only if, $(\mu,\nu)\models\varphi_{\ominus}.$