Revisiting Reachability in Timed Automata

TL;DR

This paper provides a simplified proof of the definability of reachability in timed automata, introduces an exponential-space model checking procedure for parametric TCTL, and establishes NEXPTIME-hardness.

Contribution

It offers a new, simpler proof of a fundamental reachability result and develops an exponential-space model checking method for parametric TCTL.

Findings

Simplified proof of reachability definability in timed automata

Exponential-space procedure for parametric TCTL model checking

NEXPTIME-hardness of the reachability fragment of parametric TCTL

Abstract

We revisit a fundamental result in real-time verification, namely that the binary reachability relation between configurations of a given timed automaton is definable in linear arithmetic over the integers and reals. In this paper we give a new and simpler proof of this result, building on the well-known reachability analysis of timed automata involving difference bound matrices. Using this new proof, we give an exponential-space procedure for model checking the reachability fragment of the logic parametric TCTL. Finally we show that the latter problem is NEXPTIME-hard.

Equations

$$\phi ::=\text{true}\mid x<k\mid x=k\mid x>k\mid \phi \wedge \phi ,$$

$$t::=c\mid r\mid t+t\mid t-t,$$

$$t::=c\mid z\mid t+t\mid t-t,$$

$$z-z^{\prime }\le c\mid z\le c\mid z-z^{\prime }\equiv c(\mathrm{mod}d)$$

$${\phi }_{\ell ,{\ell }^{\prime }}(z_1,\dots ,z_n,r_1,,\dots ,r_n,z_1^{\prime },\dots ,z_n^{\prime },r_1^{\prime },,\dots ,r_n^{\prime }),$$

$$⟨$$

$$\lfloor {\nu }_1^{\prime }\rfloor ,\dots ,\lfloor {\nu }_n^{\prime }\rfloor ,\mathrm{frac}({\nu }_1^{\prime }),\cdots ,\mathrm{frac}({\nu }_n^{\prime })⟩\models {\phi }_{\ell ,{\ell }^{\prime }}.$$

$${\phi }_{{\ell }_0,{\ell }_3}(z_1,z_2,$$

$$\wedge (r_1<r_2<1)$$

$$\wedge ((z_2^{\prime }-z_1^{\prime }=1\wedge 0\le r_2^{\prime }-r_1^{\prime }<r_2-r_1)$$

$$\vee (z_2^{\prime }-z_1^{\prime }=2\wedge 0\le 1+r_2^{\prime }-r_1^{\prime }<r_2-r_1)),$$

$${\phi }_{{\ell }_0,{\ell }_3}(z_1,z_2,r_1,r_2,$$

$$(r_1=r_2=0)\wedge (r_1^{\prime }=r_2^{\prime })\wedge$$

$$(z_1=z_2=0)\wedge (z_2^{\prime }-z_1^{\prime }\equiv 0(\mathrm{mod}2)).$$

$$\phi ::=p\mid \phi \wedge \phi \mid \neg \phi \mid \exists {◊}_{\sim \alpha }\phi ,$$

$$\psi ::=\phi \mid \theta -{\theta }^{\prime }\sim c\mid {\psi }_1\wedge {\psi }_2\mid \neg \psi \mid \exists \theta \psi ,$$

$$\begin{gathered} ({\ell }_0,\left(\begin{array}{c}0\\ 0\end{array}\right))\stackrel{t}{\Rightarrow }({\ell }_1,\left(\begin{array}{c}0\\ t\end{array}\right))\stackrel{0}{\Rightarrow }({\ell }_2,\left(\begin{array}{c}0\\ t\end{array}\right)) \\ \stackrel{1-t}{\Rightarrow }({\ell }_3,\left(\begin{array}{c}1-t\\ 1\end{array}\right))\stackrel{0}{\Rightarrow }({\ell }_4,\left(\begin{array}{c}0\\ 1\end{array}\right)) \end{gathered}$$

$$\mathbb{V}=(\{<,\le \}\times \mathbb{R})\cup \{(<,\infty )\}.$$

$$\llbracket M\rrbracket=\Big{\{}\nu\in\mathbb{R}_{\geq 0}^{\mathcal{X}}:\bigwedge_{0\leq i,j\leq n}\nu_{i}-\nu_{j}\prec_{i,j}m_{i,j}\Big{\}}\,,$$

$${\prec }^{\prime \prime }=\{\begin{array}{ll}\le & \text{if }\prec =\le \text{ and }{\prec }^{\prime }=\le ,\\ <& \text{otherwise}.\end{array}$$

$$\overrightarrow{M}_{i,j}=\left\{\begin{array}[]{ll}(<,\infty)&\text{if $i\neq 0,j=0$}\\[2.0pt] M_{i,j}&\text{otherwise.}\end{array}\right.$$

$$k_{\ell}=\left\{\begin{array}[]{ll}k&\mbox{ if $k\neq\ell$}\\[2.0pt] 0&\mbox{ otherwise.}\end{array}\right.$$

$$M_{i,j}^{\prime \prime }=\min (M_{i,j},M_{i,p}+M_{p,q}^{\prime }+M_{q,j})$$

$$(\{<,\le \}\times {\mathcal{T}}_{\mathbb{R}}(\tau ))\cup \{(<,\infty )\}.$$

$$\left\{\nu (\mathcal{M}):\mathcal{M}\in closure({\mathcal{M}}_{\tau })\right\}=closure(M_{\nu }).$$

$$\phi ::=\text{true}\mid c<k\mid c=k\mid c>k\mid \phi \wedge \phi ,$$

$$\mathrm{Op}(C)=\{reset(c),inc(c):c\in C\}\cup \{nop\}.$$

$$\to \subseteq (S\times {\mathbb{N}}^n)\times (S\times {\mathbb{N}}^n)$$

$$\{⟨\upsilon ,{\upsilon }^{\prime }⟩\in {\mathbb{N}}^{2n}:⟨s,\upsilon ⟩{⟶}^{\ast }⟨s^{\prime },{\upsilon }^{\prime }⟩\}$$

$${\nu }^{\prime }\models \phi \text{mbox}iff\lfloor {\nu }^{\prime }\rfloor \models {\phi }_{\mathsf{inc}}\text{mbox}and\mathrm{frac}({\nu }^{\prime })\models {\phi }_{\mathsf{frac}}$$

$${\phi }_{\mathsf{int}}\stackrel{\mathrm{def}}{=}(c_1=0)\text{ and }{\phi }_{\mathsf{frac}}\stackrel{\mathrm{def}}{=}(0<x_1<1).$$

$$M_2=(M_1\cap (0<x_1<1))[x_1\leftarrow 0],$$

$${\phi }_{\ell ,{\ell }^{\prime }}(z_1,\dots ,z_n,r_1,,\dots ,r_n,z_1^{\prime },\dots ,z_n^{\prime },r_1^{\prime },,\dots ,r_n^{\prime })$$

Full text

I Introduction

The PSPACE-completeness of the reachability problem for timed automata is arguably the most fundamental result in real-time verification. This theorem was established by Alur and Dill in paper [1] for which they were awarded the Alonzo Church award in 2016. The reachability problem has been intensively studied in the intervening 20 years, leading to practical algorithms and generalisations to more expressive models. As of now, [1] is the most cited paper that has appeared in the journal Theoretical Computer Science.

Properly speaking, Alur and Dill considered reachability between control states (also called locations). The problem of computing the binary reachability relation over configurations (both control states and clock valuations) is more involved. Here the main result is due to Comon and Jurski [2], who showed that the reachability relation of a given timed automaton is effectively definable by a formula of first-order linear arithmetic over the reals augmented with a unary predicate denoting the integers. Importantly, this fragment of mixed linear arithmetic has a decidable satisfiability problem, e.g., by translation to S1S.

Despite its evident utility, particularly for parametric verification, it is fair to say that the result of Comon and Jurski has proven less influential than that of Alur and Dill. We believe that this is due both to the considerable technical complexity of the proof, which runs to over 40 pages in [3], as well as the implicit nature of their algorithm, making it hard to extract complexity bounds.

In this paper we revisit the result of Comon and Jurski. Our two main contributions as follows:

• •

We give a new and conceptually simpler proof that generalises the classical reachability algorithm for timed automata involving difference bound matrices and standard operations thereon. The key new idea is to carry out the algorithm on a symbolically presented initial configuration. This approach is fundamentally different from that of [2], the main part of which involves a syntactic transformation showing that every timed automaton can be effectively emulated by a flat timed automaton, i.e., one that does not contain nested loops in its control graph.

• •

We apply our strengthened formulation of the Comon-Jurski result to parametric model checking. We show that the formula representing the reachability relation can be computed in time singly exponential in the size of the timed automaton. Using this bound on the formula size and utilising results of [4, 5] on quantifier-elimination for first-order logic over the reals and integers, we show that the model checking problem for the reachability fragment of the temporal logic parametric TCTL is decidable in exponential space. We show in the main body of the paper that this problem is NEXPTIME-hard and sketch in the conclusion how to obtain matching upper and lower bounds.

There are two main steps in our approach to computing a formula representing the reachability relation. First, given a timed automaton $\mathcal{A}$ and a configuration $\langle\ell,\nu\rangle$ of $\mathcal{A}$, we construct a version of the region automaton of [1] that represents all configurations reachable from $\langle\ell,\nu\rangle$. Unlike [1] we do not identify all clock values above the maximum clock constant; so our version of the region automaton is a counter machine rather than a finite state automaton. The counters are used to store the integer parts of clock valuations of reachable configurations, while the fractional parts of the clock valuations are aggregated into zones that are represented within the control states of the counter machine by difference bound matrices. Since the counters mimic clocks they are monotonic and so the reachability relation on such a counter machine is definable in a weak fragment of Presburger arithmetic.

The second step of our approach is to make the previous construction parametric: we show that the form of the counter machine does not depend on the precise numerical values of the clocks in the initial valuation $\nu$, just on a suitable logical type of $\nu$. Given such a type, we develop a parametric version of the counter-machine construction. Combining this construction with the fact that the reachability relation for the considered class of counter machines is definable in a fragment of Presburger arithmetic, we obtain a formula that represents the full reachability relation of the timed automaton $\mathcal{A}$.

I-A Related Work

Dang [6] has generalised the result of Comon and Jurski, showing that the binary reachability relation for pushdown timed automata is definable in linear arithmetic. The approach in [6] relies on a finite partition of the fractional parts of clock valuations into so-called patterns, which play a role analogous to types in our approach. The notion of pattern is ad-hoc and, as remarked by Dang, relatively complicated. In particular, patterns lack the simple characterisation in terms of difference constraints that is possessed by types. The latter is key to our result that the reachability relation can be expressed by a Boolean combination of difference constraints.

Dima [7] gives an automata theoretic representation of the reachability relation of a timed automaton. To this end he introduces a class of automata whose runs encode tuples in such a relation. The main technical result of [7] is to show that this class of automata is effectively closed under relational reflexive-transitive closure.

The model checking problem for parametric TCTL was studied by Bruyère et al. [8, 9] in the case of integer-valued parameters. Here we allow real-valued parameters, which leads to a strictly more expressive semantics.

Parametric DBMs have been used in [10, 11] to analyse reachability in parametric timed automata. These are related to but different from the parametric DBMs occurring in Subsection III-C.

I-B Organisation

We introduce and state our main results in the body of the paper. The central constructions underlying our proofs are also given in the body, along with illustrative examples. Many of the proof details are relegated to the appendix.

II Main Definitions and Results

II-A Timed Automata

Given a set $\mathcal{X}=\{x_{1},\ldots,x_{n}\}$ of clocks, the set $\Phi(\mathcal{X})$ of clock constraints is generated by the grammar

[TABLE]

where $k\in\mathbb{N}$ is a natural number and $x\in\mathcal{X}$. A clock valuation is a mapping $\nu:\mathcal{X}\to\mathbb{R}_{\geq 0}$, where $\mathbb{R}_{\geq 0}$ is the set of non-negative real numbers. We denote by $\boldsymbol{0}$ the valuation such that $\boldsymbol{0}(x)=0$ for all $x\in\mathcal{X}$. Let $\mathbb{R}_{\geq 0}^{\mathcal{X}}$ be the set of all clock valuations. We write $\nu\models\varphi$ to denote that $\nu$ satisfies the constraint $\varphi$. Given $t\in\mathbb{R}_{\geq 0}$, we let $\nu+t$ be the clock valuation such that $(\nu+t)(x)=\nu(x)+t$ for all clocks $x\in\mathcal{X}$. Given $\lambda\subseteq\mathcal{X}$, let $\nu[\lambda\leftarrow 0]$ be the clock valuation such that $\nu[\lambda\leftarrow 0](x)=0$ if $x\in\lambda$, and $\nu[\lambda\leftarrow 0](x)=\nu(x)$ if $x\not\in\lambda$. We typically write $\nu_{i}$ as shorthand for $\nu(x_{i})$, and by convention we define $\nu_{0}=0$. For all $r\in\mathbb{R}$, let $\mathrm{frac}(r)$ be the fractional part of $r$, and $\lfloor{r}\rfloor$ be the integer part. Denote by $\mathrm{frac}(\nu)$ and $\lfloor{\nu}\rfloor$ the valuations such that $(\mathrm{frac}(\nu))(x_{i})=\mathrm{frac}(\nu_{i})$ and $\lfloor{\nu}\rfloor(x_{i})=\lfloor{\nu_{i}}\rfloor$ for all clocks $x_{i}\in\mathcal{X}$.

A timed automaton is a tuple $\mathcal{A}=\langle L,\mathcal{X},E\rangle$, where $L$ is a finite set of locations, $\mathcal{X}$ is a finite set of clocks and $E\subseteq L\times\Phi(\mathcal{X})\times 2^{\mathcal{X}}\times L$ is the set of edges.

The semantics of a timed automaton $\mathcal{A}=\langle L,\mathcal{X},E\rangle$ is given by a labelled transition system $\langle Q,\stackrel{{\scriptstyle}}{{\Rightarrow}}\rangle$ with set of configurations $Q=L\times\mathbb{R}_{\geq 0}^{\mathcal{X}}$ and set of transition labels $\mathbb{R}_{\geq 0}$. A configuration $\langle\ell,\nu\rangle$ consists of a location $\ell$ and a clock valuation $\nu$. Given two configurations $\langle\ell,\nu\rangle$ and $\langle\ell^{\prime},\nu^{\prime}\rangle$, we postulate:

• •

a delay transition $\langle\ell,\nu\rangle\stackrel{{\scriptstyle d}}{{\Rightarrow}}\langle\ell^{\prime},\nu^{\prime}\rangle$ for some $d\geq 0$, if $\nu^{\prime}=\nu+d$ and $\ell=\ell^{\prime}$;

• •

a discrete transition $\langle\ell,\nu\rangle\stackrel{{\scriptstyle 0}}{{\Rightarrow}}\langle\ell^{\prime},\nu^{\prime}\rangle$, if there is an edge $\langle\ell,\varphi,\lambda,\ell^{\prime}\rangle$ of $\mathcal{A}$ such that $\nu\models\varphi$ and $\nu^{\prime}=\nu[\lambda\leftarrow 0]$.

A run $\rho=q_{0}\stackrel{{\scriptstyle d_{1}}}{{\Rightarrow}}q_{1}\stackrel{{\scriptstyle d_{2}}}{{\Rightarrow}}q_{2}\stackrel{{\scriptstyle d_{3}}}{{\Rightarrow}}\ldots$ of $\mathcal{A}$ is a (finite or infinite) sequence of delay and discrete transitions in $\langle Q,\stackrel{{\scriptstyle}}{{\Rightarrow}}\rangle$. We require infinite runs to have infinitely many discrete transitions and to be non-zeno, that is, we require $\sum_{i=1}^{\infty}d_{i}$ to diverge.

Henceforth we assume that in any given timed automaton with set $\mathcal{X}$ of clocks, $x_{n}$ is a special reference clock that is never reset. Clearly this assumption is without loss of generality for encoding the reachability relation.

Note that we consider timed automata without diagonal constraints, that is, guards of the form $x_{i}-x_{j}\sim k$, for $k$ an integer. It is known that such constraints can be removed without affecting the reachability relation (see [1, 12]).

II-B Linear Arithmetic

In this section we introduce a first-order language $\mathcal{L}_{\mathbb{R},\mathbb{Z}}$ in which to express the reachability relation of a timed automaton.

Language $\mathcal{L}_{\mathbb{R},\mathbb{Z}}$ has two sorts: a real-number sort and an integer sort. The collection $\mathcal{T}_{\mathbb{R}}$ of terms of real-number sort is specified by the grammar

[TABLE]

where $c\in\mathbb{Q}$ is a constant and $r\in\{r_{0},r_{1},\ldots\}$ is a real-valued variable. Given terms $t,t^{\prime}\in\mathcal{T}_{\mathbb{R}}$, we have an atomic formula $t\leq t^{\prime}$. The collection $\mathcal{T}_{\mathbb{Z}}$ of terms of integer sort is specified by the grammar

[TABLE]

where $c\in\mathbb{Z}$ is a constant and $z\in\{z_{0},z_{1},\ldots\}$ is an integer variable. Given terms $t,t^{\prime}\in\mathcal{T}_{\mathbb{Z}}$, we have atomic formulas $t\leq t^{\prime}$ and ${t\equiv t^{\prime}}\pmod{m}$, where $m\in\mathbb{Z}$. Formulas of $\mathcal{L}_{\mathbb{R},\mathbb{Z}}$ are constructed from atomic formulas using Boolean connectives and first-order quantifiers.

Throughout the paper we consider a fixed semantics for $\mathcal{L}_{\mathbb{R},\mathbb{Z}}$ over the two-sorted structure in which the real-number sort is interpreted by $\mathbb{R}$, the integer sort by $\mathbb{Z}$, and with the natural interpretation of addition and order on each sort.

The sublanguage $\mathcal{L}_{\mathbb{R}}$ of $\mathcal{L}_{\mathbb{R},\mathbb{Z}}$ involving only terms of real-number sort is called real arithmetic. The sublanguage $\mathcal{L}_{\mathbb{Z}}$ involving only terms of integer sort is called Presburger arithmetic. Optimal complexity bounds for deciding satisfiability of sentences of real arithmetic and Presburger arithmetic are given in [13] with, roughly speaking, real arithmetic requiring single exponential space and Presburger arithmetic double exponential space.

Proposition 1**.**

Deciding the truth of a sentence in the existential fragment of $\mathcal{L}_{\mathbb{R},\mathbb{Z}}$ can be done in NP.

Proof.

The respective decision problems for the existential fragment of real arithmetic and the existential fragment of Presburger arithmetic are in NP [14], [15]. Deciding the truth of a sentence in the existential fragment of $\mathcal{L}_{\mathbb{R},\mathbb{Z}}$ is therefore also in NP, since we can guess truth values for the Presburger and real-arithmetic subformulas, and separately check realisability of the guessed truth values in non-deterministic polynomial time. ∎

For the purpose of model checking, it will be useful to establish complexity bounds for a language $\mathcal{L}^{*}_{\mathbb{R},\mathbb{Z}}$, intermediate between $\mathcal{L}_{\mathbb{R}}$ and the full language $\mathcal{L}_{\mathbb{R},\mathbb{Z}}$. The language $\mathcal{L}^{*}_{\mathbb{R},\mathbb{Z}}$ arises from $\mathcal{L}_{\mathbb{R},\mathbb{Z}}$ by restricting the atomic formulas over terms of integer sort to have the form

[TABLE]

for integer variables $z,z^{\prime}$ and integers $c,d$.

Proposition 2**.**

Deciding the truth of a prenex-form sentence $Q_{1}x_{1}\ldots Q_{n}x_{n}\,\varphi$ in $\mathcal{L}^{*}_{\mathbb{R},\mathbb{Z}}$ can be done in space exponential in $n$ and polynomial in $\varphi$.

Proof.

The proposition is known to hold separately for $\mathcal{L}_{\mathbb{R}}$ [4] and for the fragment of $\mathcal{L}_{\mathbb{Z}}$ in which atomic formulas have the form shown in (1) [5, Section 4]. The respective arguments of [4] and [5] can be straightforwardly combined to prove the proposition; see Section -A for details. ∎

II-C Definability of the Reachability Relation

Given a timed automaton $\mathcal{A}$ with $n$ clock variables, we express the reachability relation between every pair of locations $\ell,\ell^{\prime}$ by a formula

[TABLE]

in the existential fragment of $\mathcal{L}_{\mathbb{R},\mathbb{Z}}$ where $z_{1},z^{\prime}_{1},\ldots,z_{n},z^{\prime}_{n}$ are integer variables and $r_{1},r^{\prime}_{1},\ldots,r_{n},r^{\prime}_{n}$ are real variables ranging over the interval $[0,1]$. Our main result, Theorem 10, shows that there is a finite run in $\mathcal{A}$ from configuration $\langle\ell,\nu\rangle$ to configuration $\langle\ell^{\prime},\nu^{\prime}\rangle$ just in case

[TABLE]

Example 1**.**

Consider the following timed automaton:

A brief inspection reveals that location $\ell_{3}$ can be reached from a configuration $\langle\ell_{0},\left(\begin{smallmatrix}\nu_{1}\\ \nu_{2}\end{smallmatrix}\right)\rangle$ if and only if $\nu_{1}<\nu_{2}<1$. The reachability relation between locations $\ell_{0}$ and $\ell_{3}$ is expressed by the formula

[TABLE]

where the real-valued variables $r_{1},r_{2},r^{\prime}_{1},r^{\prime}_{2}$ range over the interval $[0,1]$.

Example 2**.**

Consider the following timed automaton:

We have

[TABLE]

II-D Parametric Timed Reachability Logic

Timed computation tree logic (TCTL) is an extension of computation tree logic for specifying real-time properties [16]. In [8] TCTL was generalised to allow parameters within timing constraints, yielding the logic parametric TCTL. In this paper we consider the fragment of parametric TCTL generated by the reachability modality $\exists\lozenge$, which we call parametric timed reachability logic (PTRL).

Let $AP$ be a set of atomic propositions and $\Theta$ a set of parameters. Formulas of PTRL of the first type are given by the grammar

[TABLE]

where $p\in AP$, ${\sim}\in\{<,\leq,=,\geq,>\}$, and $\alpha\in\mathbb{Q}\cup\Theta$. Formulas of PTRL of the second type are given by grammar

[TABLE]

where $\varphi$ is a formula of the first type, $\theta,\theta^{\prime}\in\Theta$, ${\sim}\in\{<,\leq,=,\geq,>\}$, and $c\in\mathbb{Q}$. In the sequel we use $\forall\boxempty_{\sim\alpha}\varphi$ as abbreviation for $\neg\exists\lozenge_{\sim\alpha}\neg\varphi$.

Formulas of PTRL are interpreted with respect to a timed automaton $\mathcal{A}=\langle L,\mathcal{X},E\rangle$ and labelling function $LB:L\rightarrow 2^{AP}$. A parameter valuation is a function $\xi:\Theta\rightarrow\mathbb{R}_{\geq 0}$. Such a function is extended to the rational numbers by writing $\xi(c)=c$ for $c\in\mathbb{Q}$. Given a parameter valuation $\xi$, we define a satisfaction relation $\models_{\xi}$ between configurations of $\mathcal{A}$ and PTRL formulas by induction over the structure of formulas. The Boolean connectives are handled in the expected way, and we define

• $q\models_{\xi}\theta-\theta^{\prime}\sim c$ iff $\xi(\theta)-\xi(\theta^{\prime})\sim c$.
• $q\models_{\xi}\exists\lozenge_{\sim\alpha}\,\varphi$ iff there exists some infinite non-zeno run $\rho=q_{0}\stackrel{{\scriptstyle d_{1}}}{{\Rightarrow}}q_{1}\stackrel{{\scriptstyle d_{2}}}{{\Rightarrow}}q_{2}\stackrel{{\scriptstyle d_{3}}}{{\Rightarrow}}\ldots$ of $\mathcal{A}$ and $i\in\mathbb{N}$ such that $q_{0}=q$, $d_{1}+\ldots+d_{i}\sim\xi(\alpha)$, and $q_{i}\models\varphi$.
• $q\models_{\xi}\exists\theta\,\psi$ iff there exists a parameter valuation $\xi^{\prime}$ such that $q\models_{\xi^{\prime}}\psi$ and $\xi,\xi^{\prime}$ agree on $\Theta\setminus\{\theta\}$.

Example 3**.**

The ${PTRL}$-formula $\forall\theta(\exists\lozenge_{<\theta}p_{1}\rightarrow\exists\lozenge_{<\theta}p_{2})$ expresses that some $p_{2}$-state is reachable in at most the same time as any $p_{1}$-state is reachable.

The paper [8] considered a semantics for parametric TCTL in which parameters range over naturals $\mathbb{N}$. Here we have given a more general semantics in which parameters range over non-negative real numbers $\mathbb{R}_{\geq 0}$. The following example shows that the satisfaction relation changes under this extension.

Example 4**.**

Consider the timed automaton in Figure 2 with two clocks $x_{1},x_{2}$. Clock valuations $\nu$ are denoted by vectors $\left(\begin{smallmatrix}\nu_{1}\\ \nu_{2}\end{smallmatrix}\right)$. Let $\varphi=\exists\lozenge(p_{1}\wedge\exists\lozenge_{=\theta}\,p_{2})$. All non-zeno infinite runs of the timed automaton, from configuration $\langle\ell_{0},\boldsymbol{0}\rangle$, start with the following prefix

[TABLE]

where $0<t<1$. Now we have that $(\ell_{1},\left(\begin{smallmatrix}0\\ t\end{smallmatrix}\right))\models(p_{1}\wedge\exists\lozenge_{=1-t}\,p_{2})$. As a result, $(\ell_{0},\boldsymbol{0})\models\exists\lozenge(p_{1}\wedge\forall\lozenge_{=\theta}\,p_{2})$ only for $0<\theta<1$. Thus $(\ell_{0},\boldsymbol{0})\models\mathop{\exists\theta}\varphi$ when the parameter $\theta$ ranges over $\mathbb{R}_{\geq 0}$ but not when $\theta$ ranges over $\mathbb{N}$.

Let $\mathcal{A}=\langle L,\mathcal{X},E\rangle$ be a timed automaton augmented with a labelling function $LB:L\rightarrow 2^{AP}$. Let $\varphi$ be a PTRL formula in which all occurrences of parameters are bound. The model checking problem of $\mathcal{A}$ against $\varphi$ asks, given a configuration $\langle\ell,\nu\rangle$ of $\mathcal{A}$, whether $\langle\ell,\nu\rangle\models\varphi$.

The model checking procedure for parametric TCTL with integer-valued parameters, developed in [8], relies on the region abstraction. In particular, formulas in this logic have the same truth value for all configurations in a given region. However, as the following example shows, region invariance fails when parameters range over the set of real numbers.

Example 5**.**

Consider the timed automaton in Figure 2. Let $\varphi=\exists\theta\,\exists\lozenge_{=\theta}(p_{1}\wedge\exists\lozenge_{=\theta}p_{2})$. Then a configuration $(\ell_{0},\left(\begin{smallmatrix}t_{1}\\ t_{2}\end{smallmatrix}\right))$ satisfies $\varphi$ just in case $t_{1},t_{2}<1$ and $2t_{1}-t_{2}<1$, for $\theta=(1-t_{2})/2$.

In Section V we show that model checking PTRL over real-valued parameters is decidable in EXPSPACE and it is NEXPTIME-hard.

III Difference Bound Matrices

III-A Basic Definitions

In this section we review the notions of clock zones and difference bound matrices; see [17, 18] for further details.

Let $\mathcal{X}=\{x_{1},\ldots,x_{n}\}$ be a set of clock variables. A zone $\mathit{Z}\subseteq\mathbb{R}_{\geq 0}^{\mathcal{X}}$ is a set of valuations defined by a conjunction of difference constraints $x_{j}-x_{i}\prec c$ for $c\in\mathbb{R}$ and ${\prec}\in\{<,\leq\}$. Note that we allow real-valued constants in difference constraints.

Zones and operations thereon can be efficiently represented using difference bound matrices (DBMs). A DBM is an $(n+1)\times(n+1)$ matrix $M$ with entries in the set

[TABLE]

A DBM $M=(\prec_{i,j},m_{i,j})$ can be interpreted as a conjunction of constraints $x_{i}-x_{j}\prec_{i,j}m_{i,j}$, where $x_{0}$ is a special clock that symbolically represents zero. Formally, the semantics of DBM $M$ is the zone

[TABLE]

where $\nu_{0}=0$. Figure 2 depicts a zone $\mathit{Z}\subseteq[0,1]^{2}$ containing a line segment and a DBM $M$ with $\llbracket M\rrbracket=\mathit{Z}$ .

An atomic DBM $M^{\prime}$ is one that represents a single constraint $x_{i}-x_{j}\sim c$, where ${\sim}\in\{<,\leq\}$ and $c\in\mathbb{R}$. Note that all but one entry of an atomic DBM is the trivial constraint $(<,\infty)$. We often denote DBMs by the constraints that they represent.

Define a total order $\leq_{\mathbb{V}}$ on $\mathbb{V}$ by writing $(\prec,m)\leq_{\mathbb{V}}(\prec^{\prime},m^{\prime})$ if $m<m^{\prime}$ or if $m=m^{\prime}$ and either ${\prec}=<$ or ${\prec^{\prime}}={\leq}$. Define addition on $\mathbb{V}$ by $(\prec,m)+(\prec^{\prime},m^{\prime})=(\prec^{\prime\prime},m+m^{\prime})$, where

[TABLE]

Here we adopt the convention that $m+\infty=\infty+m=\infty$ for all $m\in\mathbb{R}$. A DBM $M=(M_{i,j})$ is in canonical form if $M_{i,k}\leq_{\mathbb{V}}M_{i,j}+M_{j,k}$ for all $0\leq i,j,k\leq n$. One can transform an arbitrary DBM into an equivalent canonical-form DBM using the Floyd-Warshall algorithm. For all non-empty clock zones $\mathit{Z}$, there is a unique DBM $M$ in canonical form with $\llbracket M\rrbracket=\mathit{Z}$. A DBM $M$ is said to be consistent if $\llbracket M\rrbracket\neq\emptyset$. If $M$ is in canonical form, then it is consistent if and only if $(\leq,0)\leq_{\mathbb{V}}M_{i,i}$ for all $0\leq i\leq n$.

We now define operations on DBMs that correspond to time elapse, projection, and intersection on zones.

Time Elapse. The image of a DBM $M$ under time elapse is the DBM $\overrightarrow{M}$ defined by

[TABLE]

If $M$ is canonical, then $\overrightarrow{M}$ is also canonical and we have $\llbracket\overrightarrow{M}\rrbracket=\{\nu+t:\nu\in\llbracket M\rrbracket\mbox{ and }t\geq 0\}$.\

Reset. The image of a DBM $M$ under resetting clock $x_{\ell}$ is $M[x_{\ell}\leftarrow 0]$, given by $M[x_{\ell}\leftarrow 0]_{i,j}=M_{i_{\ell},j_{\ell}},$ where for any index $k$,

[TABLE]

If $M$ is canonical, then $M[x_{\ell}\leftarrow 0]$ is also canonical and $\llbracket M\rrbracket=\{\nu[x_{\ell}\leftarrow 0]:\nu\in\llbracket M\rrbracket\}$.\

Intersection. Our presentation of intersection of DBMs is slightly non-standard. First, we only consider intersection with atomic DBMs. (Clearly this is without loss of generality since any DBM can be written as an intersection of atomic DBMs.) Under this restriction we combine intersection and canonisation, so that our intersection operation yields a DBM in canonical form if the input DBM is in canonical form. Specifically, let $M^{\prime}$ be an atomic DBM with non-trivial constraint $M^{\prime}_{p,q}$. The DBM $M^{\prime\prime}=M\cap M^{\prime}$ is given by

[TABLE]

for all $i,j$. Then $M^{\prime\prime}$ is canonical and $\llbracket M^{\prime\prime}\rrbracket=\llbracket M\rrbracket\cap\llbracket M^{\prime}\rrbracket$.

III-B Closure of a DBM

We will use zones to represent the fractional parts of clocks in a given set of valuations. For this reason we are solely interested in zones contained in $[0,1]^{n}$. We say that a DBM $M$ is $1$-bounded if for all entries $(\prec,m)$ of $M$ we have $-1\leq m\leq 1$. It is clear that if $M$ is $1$-bounded then $\llbracket M\rrbracket\subseteq[0,1]^{n}$. Conversely the unique DBM in canonical form that represents a zone $Z\subseteq[0,1]^{n}$ is necessarily $1$-bounded since the constraints in a canonical DBM cannot be tightened.

Given a $1$-bounded DBM $M$, define the closure $M$ to be the smallest set $\mathit{closure}(M)$ of DBMs such that $M\in\mathit{closure}(M)$, and if $N\in\mathit{closure}(M)$ then

• •

$N\cap M^{\prime}\in\mathit{closure}(M)$ for all atomic DBMs $M^{\prime}$ with numerical entries in $\mathbb{Z}\cup\{\infty\}$.

• •

$\overrightarrow{N}\cap\bigcap_{i=1}^{n}(x_{i}\leq 1)\in\mathit{closure}(M)$,

• •

$N[x_{i}\leftarrow 0]\in\mathit{closure}(M)$ for $0\leq i\leq n-1$,

• •

$(N\cap(x_{n}=1))[x_{n}\leftarrow 0]\in\mathit{closure}(M)$.

We make three observations about this definition. First, notice that in the first item we only require closure with respect to intersection with constraints with integer constants. Observe also that in the second item the time elapse operation has been relativized to $[0,1]^{n}$. This ensures that every DBM $N\in\mathit{closure}(M)$ denotes a subset of $[0,1]^{n}$. It follows that any consistent DBM in $\mathit{closure}(M)$ is 1-bounded. Finally, note that the clock $x_{n}$ is treated in a special way (in keeping with our assumptions about timed automata in Section II-A): it is only reset when it reaches $1$.

Let $\nu\in[0,1]^{n}$ be a clock valuation, and recall that, by convention, $\nu_{0}=0$. We write $M_{\nu}$ for the 1-bounded DBM $M_{\nu}=(\prec_{i,j},m_{i,j})$, where ${\prec_{i,j}}={\leq}$ and $m_{i,j}=\nu_{j}-\nu_{i}$ for all $0\leq i,j\leq n$. Then $M_{\nu}$ is in canonical form and $\llbracket M_{\nu}\rrbracket=\{\nu\}$.

We say a DBM $M=(\prec_{i,j},m_{i,j})\in\mathit{closure}(M_{\nu})$ is well-supported, if each entry $m_{i,j}$ can be written in the form $c+\nu_{j^{\prime}}-\nu_{i^{\prime}}$ for some $c\in\{-1,0,1\}$ and indices $0\leq i^{\prime},j^{\prime}\leq n$. Clearly $M_{\nu}$ is well-supported.

The following is the main technical result in this section. See Appendix -B for the full proof.

Lemma 3**.**

Let $\nu\in[0,1]^{n}$ be a clock valuation. Then every consistent DBM lying in $\mathit{closure}(M_{\nu})$ is well-supported.

Proof Sketch.

We show by induction on the structure of $\mathit{closure}(M_{\nu})$ that any consistent DBM $M\in\mathit{closure}(M_{\nu})$ is well-supported. The key case is for intersection (see Section III-A), which does not immediately preserve well-supportedness due to the possibility that  $M^{\prime\prime}_{i,j}=M_{i,p}+M^{\prime}_{p,q}+M_{q,j}$. However we show that in this case at least one of $m_{i,p}$ or $m_{q,j}$ lies in $\mathbb{Z}$, which ensures well-supportedness of $M^{\prime\prime}$. ∎

III-C Parametric DBMs

In this subsection we observe that the construction of $\mathit{closure}(M_{\nu})$ can be carried out parametrically, based on the logical type of the clock valuation $\nu\in[0,1]^{n}$ (to be defined below). In particular, if $\nu,\nu^{\prime}\in[0,1]^{n}$ have the same type, then $\mathit{closure}(M_{\nu})$ and $\mathit{closure}(M_{\nu^{\prime}})$ can both be seen as instances of a common parametric construction.

Recall from Subsection II-B the definition of the set of terms $\mathcal{T}_{\mathbb{R}}$ of real arithmetic. Given $n\in\mathbb{N}$, let us further write $\mathcal{T}_{\mathbb{R}}(n)$ for the set of terms in variables $r_{0},\ldots,r_{n}$. A valuation $\nu\in[0,1]^{n}$ extends in a natural way to a function $\nu:\mathcal{T}_{\mathbb{R}}(n)\rightarrow\mathbb{R}$ mapping $r_{i}$ to $\nu_{i}$ (recalling the convention that $\nu_{0}=0$).

Given a clock valuation $\nu\in[0,1]^{n}$, the type of $\nu$ is the set of atomic $\mathcal{L}_{\mathbb{R}}$-formulas $t\leq t^{\prime}$, with $t,t^{\prime}\in\mathcal{T}_{\mathbb{R}}(n)$ that are satisfied by the valuation $\nu$. A collection of atomic formulas $\tau$ is said to be an $n$-type if it is the type of some clock valuation $\nu\in[0,1]^{n}$. Note that every type contains the inequalities $r_{0}\leq 0$ and $0\leq r_{0}$.

Given an $n$-type $\tau$, we define an equivalence relation on the set of terms $\mathcal{T}_{\mathbb{R}}(n)$ that relates terms $t$ and $t^{\prime}$ just in case the formulas $t\leq t^{\prime}$ and $t^{\prime}\leq t$ both lie in $\tau$. We write $[t]$ for the equivalence class of term $t$ and denote by $\mathcal{T}_{\mathbb{R}}(\tau)$ the set of equivalence classes of $\mathcal{T}_{\mathbb{R}}(n)$. We can define a linear order on $\mathcal{T}_{\mathbb{R}}(\tau)$ by writing $[t]\leq[t^{\prime}]$ if and only if formula $t\leq t^{\prime}$ lies in $\tau$. We define an addition operation on $\mathcal{T}_{\mathbb{R}}(\tau)$ by writing $[t]+[t^{\prime}]=[t+t^{\prime}]$.

Given an $n$-type $\tau$, a parametric DBM of dimension $n$ over $\mathcal{T}_{\mathbb{R}}(\tau)$ is an $(n+1)\times(n+1)$ matrix with entries in

[TABLE]

We use letters in calligraphic font to denote parametric DBMs, and roman font for concrete DBMs. Given a parametric DBM $\mathcal{M}$, we obtain a concrete DBM $\nu(\mathcal{M})$ by applying $\nu$ pointwise to the entries of $\mathcal{M}$.

The time elapse and reset operations on DBMs, defined in Section III-A, formally carry over to parametric DBMs. Since the notions of addition and minimum are well-defined on $\mathcal{T}_{\mathbb{R}}(\tau)$, we can also formally carry over the definition of intersection to parametric DBMs.

Proposition 4**.**

Let $\nu\in[0,1]^{n}$ be a clock valuation with type $\tau$ and let $\mathcal{M}$ be a parametric DBM over $\mathcal{T}_{\mathbb{R}}(\tau)$. Then

$\nu(\overrightarrow{\mathcal{M}})=\overrightarrow{\nu(\mathcal{M})}$. 2. 2.

$\nu(\mathcal{M}[x_{i}\leftarrow 0])=\nu(\mathcal{M})[x_{i}\leftarrow 0]$. 3. 3.

$\nu(\mathcal{M}\cap N)=\nu(\mathcal{M})\cap N$* for all atomic DBMs $N$.*

Proof.

Suppose that $\nu$ has type $\tau$. Then $\nu:\mathcal{T}_{\mathbb{R}}(\tau)\rightarrow\mathbb{R}$ is an order embedding ($[t]\leq[t^{\prime}]$ if and only if $\nu(t)\leq\nu(t^{\prime})$) and a homomorphism ($\nu([t]+[t^{\prime}])=\nu([t])+\nu([t])$). In particular, $\nu$ preserves all operations used to define time elapse, projection, and intersection of DBMs. The result follows. ∎

Since the basic operations on DBMs are all defined for parametric DBMs, we can also formally carry over the definition of the closure of a DBM to parametric DBMs. In particular, given an $n$-type $\tau$, we consider the closure of the parametric DBM $\mathcal{M}_{\tau}=(\prec_{i,j},m_{i,j})$ over $\mathcal{T}_{\mathbb{R}}(\tau)$, where ${\prec_{i,j}}={\leq}$ and $m_{i,j}=[r_{i}-r_{j}]$. Note that $\nu(\mathcal{M}_{\tau})=M_{\nu}$ for any clock valuation $\nu\in[0,1]^{n}$. Then, by Proposition 4, we have the following result:

Proposition 5**.**

Let $\nu\in[0,1]^{n}$ be a clock valuation with type $\tau$. Then

[TABLE]

Define the set $\mathcal{DT}_{\mathbb{R}}(n)$ of difference terms to be the subset of $\mathcal{T}_{\mathbb{R}}(n)$ comprising those terms of the form $c+r_{i}-r_{j}$, where $c\in\{-1,0,1\}$ is a constant and $r_{i},r_{j}$ are variables with $0\leq i,j\leq n$. From Lemma 3 and Proposition 5 we now have:

Corollary 6**.**

Fix an $n$-type $\tau$. Then every DBM in $\mathit{closure}(\mathcal{M}_{\tau})$ has all its entries of the form $(\prec,[t])$, where ${\prec}\in\{<,\leq\}$ and $t\in\mathcal{DT}_{\mathbb{R}}(n)$.

The significance of Corollary 6 is that the only part of the type $\tau$ required to determine $\mathit{closure}(\mathcal{M}_{\tau})$ is the finite collection of formulas $t\leq t^{\prime}$ in $\tau$ such that $t,t^{\prime}\in\mathcal{DT}_{\mathbb{R}}(n)$. Thus $\mathit{closure}(\mathcal{M}_{\tau})$ is finite. Indeed it is not hard to see from Corollary 6 that $|\mathit{closure}(\mathcal{M}_{\tau})|\leq 2^{\mathrm{poly}(n)}$.

IV A Family of Region Automata

Let $\mathcal{A}$ be a timed automaton. Our aim in this section is to define a finite collection of counter machines that represents the reachability relation on $\mathcal{A}$. Intuitively the counters in these machines are used to store the integer parts of clock valuations of reachable configurations, while the fractional parts of the clock valuations are aggregated into zones which are represented by difference bound matrices encoded within control states.

IV-A Monotonic Counter Machine

In this subsection we introduce the class of monotonic counter machines and show that the reachability relation for a machine in this class is definable in Presburger arithmetic. The proof is straightforward, and is related to the fact that the reachability relation of every reversal-bounded counter machine is Presburger definable [19].

Let $C=\{c_{1},\ldots,c_{n}\}$ be a finite set of counters. The collection of guards, denoted $\Phi(C)$, is given by the grammar

[TABLE]

where $c\in C$ and $k\in\mathbb{Z}$. The set of counter operations is

[TABLE]

A monotonic counter machine is a tuple $\mathcal{C}=\langle S,C,\Delta\rangle$, where $S$ is a finite set of states, $C$ is a finite set of counters, and $\Delta\subseteq S\times\Phi(C)\times\mathrm{Op}(C)\times S$ is a set of edges.

The set of configurations of $\mathcal{C}$ is $S\times\mathbb{N}^{n}$. A configuration $\langle s,\upsilon\rangle$ consists of a state $s\in S$ and a counter valuation $\upsilon\in\mathbb{N}^{n}$, where $\upsilon_{i}$ represents the value of counter $c_{i}$ for $i=1,\ldots,n$. The satisfaction relation $\models$ between counter valuations and guards is defined in the obvious way. The transition relation

[TABLE]

is specified by writing $\langle s,\upsilon\rangle\rightarrow\langle s^{\prime},\upsilon^{\prime}\rangle$ just in case at least one of the following holds:

• •

there is an edge $\langle s,\varphi,\mathit{nop},s^{\prime}\rangle\in\Delta$ such that $\upsilon\models\varphi$ and $\upsilon=\upsilon^{\prime}$;

• •

there is an edge $\langle s,\varphi,\mathit{reset}(c_{i}),s^{\prime}\rangle\in\Delta$ such that $\upsilon\models\varphi$, $\upsilon^{\prime}_{i}=0$, and $\upsilon^{\prime}_{j}=\upsilon_{j}$ for $i\neq j$;

• •

there is an edge $\langle s,\varphi,\mathit{inc}(c_{i}),s^{\prime}\rangle\in\Delta$ such that $\upsilon\models\varphi$, $\upsilon^{\prime}_{i}=\upsilon_{i}+1$, and $\upsilon^{\prime}_{j}=\upsilon_{j}$ for $i\neq j$.

The reachability relation on $\mathcal{C}$ is the reflexive transitive closure of $\rightarrow$.

The proof of the following result is given in Appendix -C.

Proposition 7**.**

Let $\mathcal{C}$ be a monotonic counter machine with $n$ counters. Given states $s,s^{\prime}$ of $\mathcal{C}$, the reachability relation

[TABLE]

is definable by a formula in the existential fragment of Presburger arithmetic that has size exponential in $\mathcal{C}$.

IV-B Concrete Region Automata

Let $\mathcal{A}=\langle L,\mathcal{X},E\rangle$ be a timed automaton and $\langle\ell,\nu\rangle$ a configuration of $\mathcal{A}$. We define a monotonic counter machine $\mathcal{C}_{\langle\ell,\nu\rangle}$ whose configuration graph represents all configurations of $\mathcal{A}$ that are reachable from $\langle\ell,\nu\rangle$.

Let $\mathcal{X}=\{x_{1},\ldots,x_{n}\}$ be the set of clocks in $\mathcal{A}$. Recall from Section II-A the assumption that clock $x_{n}$ is never reset by the timed automaton. To simplify the construction, we also assume that each transition in $\mathcal{A}$ resets at most one clock. This is without loss of generality with respect to reachability.

Given a clock constraint $\varphi\in\Phi(\mathcal{X})$, we decompose $\varphi$ into an integer constraint $\varphi_{\mathsf{int}}\in\Phi(C)$ and a real constraint $\varphi_{\mathsf{frac}}\in\Phi(\mathcal{X})$ such that for every clock valuation $\nu^{\prime}\in\mathbb{R}_{\geq 0}^{\mathcal{X}}$,

[TABLE]

The definition of $\varphi_{\mathsf{int}}$ and $\varphi_{\mathsf{frac}}$ is by induction on the structure of $\varphi$. The details are given in Figure 4.

The construction of the counter machine $\mathcal{C}_{\langle\ell,\nu\rangle}=\langle S,C,\Delta\rangle$ is such that the set $S$ of states comprises all pairs $\langle\ell^{\prime},M\rangle$ such that $\ell^{\prime}\in L$ is a location of $\mathcal{A}$ and $M\in\mathit{closure}(M_{\mathrm{frac}(\nu)})$ is a consistent DBM. The set of counters is $C=\{c_{1},\ldots,c_{n}\}$, where $n$ is the number of clocks in $\mathcal{A}$. Intuitively the purpose of counter $c_{i}$ is to store the integer part of clock $x_{i}$, for $i=1,\ldots,n$.

We classify the transitions of $\mathcal{C}_{\langle\ell,\nu\rangle}$ into three different types: From all states $\langle\ell_{1},M_{1}\rangle$ to a state $\langle\ell_{1},M_{2}\rangle$, there is

• •

a delay transition if $M_{2}=\overrightarrow{M_{1}}\cap\bigcap_{i=1}^{n}(x_{i}\leq 1)$. Such a transition has guard true and operation $\mathit{nop}$;

• •

a wrapping transition if $M_{2}=(M_{1}\cap(x_{i}=1))[x_{i}\leftarrow 0]$ for some clock $x_{i}$. Such a transition has guard true and operation $\mathit{inc}(c_{i})$.

Suppose that $(\ell,\varphi,\{x_{i}\},\ell^{\prime})$ is a transition of $\mathcal{A}$. Decompose the guard $\varphi$ into $\varphi_{{\sf int}}$ and $\varphi_{{\sf frac}}$. Then from all states $\langle\ell_{1},M_{1}\rangle$ to a state $\langle\ell_{2},M_{2}\rangle$, there is

• •

a discrete transition if $M_{2}=(M_{1}\cap\varphi_{{\sf frac}})[x_{i}\leftarrow 0]$. Such a transition has guard $\varphi_{{\sf int}}$ and operation $\mathit{reset}(c_{i})$.

The following proposition describes how the set of reachable configurations in $\mathcal{C}_{\langle\ell,\nu\rangle}$ represents the set of configurations reachable from $\langle\ell,\nu\rangle$ in the timed automaton $\mathcal{A}$. The proposition is a straightforward variant of the soundness and completeness of the DBM-based forward reachability algorithm for timed automata, as shown, e.g., in [20, Theorem 1]. We give a proof in Appendix -D.

Proposition 8**.**

Configuration $\langle\ell^{\prime},\nu^{\prime}\rangle$ is reachable from $\langle\ell,\nu\rangle$ in $\mathcal{A}$ if and only if there exists some DBM $M^{\prime}\in\mathit{closure}(M_{\mathrm{frac}(\nu)})$ such that the configuration $\langle\langle\ell^{\prime},M^{\prime}\rangle,\lfloor{\nu^{\prime}}\rfloor\rangle$ is reachable from $\langle\langle\ell,M_{\mathrm{frac}(\nu)}\rangle,\lfloor{\nu}\rfloor\rangle$ in the counter machine $\mathcal{C}_{\langle\ell,\nu\rangle}$ and $\mathrm{frac}(\nu^{\prime})\in\llbracket M^{\prime}\rrbracket$.

We illustrate the translation from timed automata to counter machines with the following example.

Example 6**.**

Consider the timed automaton $\mathcal{A}$ in Figure 3 with clocks $\mathcal{X}=\{x_{1},x_{2}\}$, where $x_{2}$ is the reference clock. Let the configuration $\langle\ell_{0},\nu\rangle$ be such that $\nu=\left(\begin{smallmatrix}0.6\\ 0\end{smallmatrix}\right)$. Also shown in Figure 3 is the counter machine $\mathcal{C}_{\langle\ell_{0},\nu\rangle}$ that is constructed from $\mathcal{A}$ and $\langle\ell_{0},\nu\rangle$ in the manner described above. The control states of this machine are pairs $\langle\ell,M\rangle$, where $\ell$ is a location of $\mathcal{A}$ and $M$ is a consistent DBM in $\mathit{closure}(M_{\nu})$. The machine $\mathcal{C}_{\langle\ell_{0},\nu\rangle}$ has two counters, respectively denoted by $c_{1}$ and $c_{2}$.

The initial state of $\mathcal{C}_{\langle\ell_{0},\nu\rangle}$ is $\langle\ell_{0},M_{0}\rangle$, where $M_{0}=M_{\nu}$. Note that $\llbracket M_{0}\rrbracket=\left\{\left(\begin{smallmatrix}0.6\\ 0\end{smallmatrix}\right)\right\}$. The counter-machine state $\langle\ell_{0},M_{0}\rangle$ in tandem with counter valuation $\left(\begin{smallmatrix}0\\ 0\end{smallmatrix}\right)$ represents the configuration $\langle\ell_{0},\nu\rangle$ of $\mathcal{A}$.

There is a delay edge in $\mathcal{C}_{\langle\ell_{0},\nu\rangle}$ from $\langle\ell_{0},M_{0}\rangle$ to $\langle\ell_{0},M_{1}\rangle$, where $M_{1}=\overrightarrow{M_{0}}\cap\bigcap_{i=1}^{2}(x_{i}\leq 1)$. We then have $\llbracket M_{1}\rrbracket=\left\{\left(\begin{smallmatrix}0.6\\ 0\end{smallmatrix}\right)+t:0\leq t\leq 0.4\right\}$.

The single transition of $\mathcal{A}$ yields a discrete edge in $\mathcal{C}_{\langle\ell_{0},\nu\rangle}$ from $\langle\ell_{0},M_{1}\rangle$ to $\langle\ell_{1},M_{2}\rangle$. This transition in $\mathcal{A}$ has guard $\varphi\stackrel{{\scriptstyle\mathrm{def}}}{{=}}0<x_{1}<1$. This decomposes into separate constraints on the integer and fractional parts, respectively given by

[TABLE]

The integer part $\varphi_{\mathsf{int}}$ becomes the guard of the corresponding edge in $\mathcal{C}_{\langle\ell_{0},\nu\rangle}$. The fractional part $\varphi_{\mathsf{frac}}$ is incorporated into the DBM $M_{2}$, which is defined as

[TABLE]

where $\llbracket M_{2}\rrbracket=\left\{\left(\begin{smallmatrix}0\\ y\end{smallmatrix}\right):0\leq y<0.4\right\}$. There is a further delay edge in $\mathcal{C}_{\langle\ell_{0},\nu\rangle}$ from $\langle\ell_{1},M_{2}\rangle$ to $\langle\ell_{1},M_{3}\rangle$.

There is a wrapping edge from $\langle\ell_{1},M_{3}\rangle$ to $\langle\ell_{1},M_{4}\rangle$, where $M_{4}=(M_{3}\cap(x_{2}=1))[x_{2}\leftarrow 0]$. The counter $c_{2}$ is incremented along this edge, corresponding to the integer part of clock $x_{2}$ increasing by $1$ as time progresses.

The remaining states and edges of $\mathcal{C}_{\langle\ell_{0},\nu\rangle}$ are illustrated in Figure 3. Note that we only represent states that are relevant to expressing reachability from $\ell_{0}$ to $\ell_{1}$.

An important fact about the collection of counter machines $\mathcal{C_{\langle\ell,\nu\rangle}}$, as $\mathrm{frac}(\nu)$ varies over $[0,1]^{\mathcal{X}}$, is that there are only finitely many such machines up to isomorphism. This essentially follows from Proposition 5, which shows that $\mathit{closure}(M_{\mathrm{frac}(\nu)})$ is determined by the type of $\mathrm{frac}(\nu)$. In the next section we develop this intuition to build a symbolic counter machine that embodies $\mathcal{C_{\langle\ell,\nu\rangle}}$ for all valuations $\nu$ of the same type.

IV-C *Parametric Region Automata *

Consider a timed automaton $\mathcal{A}$ with $n$ clocks, a location $\ell$ of $\mathcal{A}$, and an $n$-type $\tau$. In this section we define a monotonic counter machine $\mathcal{C}_{\langle\ell,\tau\rangle}$ that can be seen as a parametric version of the counter machine $\mathcal{C}_{\langle\ell,\nu\rangle}$ from the previous section, where valuation $\nu$ has type $\tau$.

First recall that $\mathcal{M}_{\tau}=(\prec_{i,j},m_{i,j})$ is the parametric DBM over $\mathcal{T}_{\mathbb{R}}(\tau)$ such that $\prec_{i,j}=\leq$ and $m_{i,j}=[r_{i}-r_{j}]$ for $0\leq i,j\leq n$.

The construction of the counter machine $\mathcal{C}_{\langle\ell,\tau\rangle}$ is formally very similar to that of $\mathcal{C}_{\langle\ell,\nu\rangle}$. Specifically, the set $S$ of states of $\mathcal{C}_{\langle\ell,\tau\rangle}$ comprises all pairs $\langle\ell^{\prime},\mathcal{M}^{\prime}\rangle$ such that $\ell^{\prime}\in L$ is a location in $\mathcal{A}$ and $\mathcal{M}^{\prime}\in\mathit{closure}(\mathcal{M}_{\tau})$ is a consistent parametric DBM. The set of counters is $C=\{c_{1},\ldots,c_{n}\}$, where $n$ is the number of clocks in $\mathcal{A}$. The transitions of $\mathcal{C}_{\langle\ell,\tau\rangle}$ are defined in a formally identical way to those of $\mathcal{C}_{\langle\ell,\nu\rangle}$; we simply replace operations on concrete DBMs with the corresponding operations on parametric DBMs.

With the above definition, it follows from Proposition 4 that the counter machine $\mathcal{C}_{\langle\ell,\tau\rangle}$ and $\mathcal{C}_{\langle\ell,\nu\rangle}$ are isomorphic via the map sending a control state $\langle\ell,\mathcal{M}\rangle$ of $\mathcal{C}_{\langle\ell,\tau\rangle}$ to the control state $\langle\ell,\nu(\mathcal{M})\rangle$ of $\mathcal{C}_{\langle\ell,\nu\rangle}$. Proposition 8 then yields:

Theorem 9**.**

Consider states $\langle\ell,\nu\rangle$ and $\langle\ell^{\prime},\nu^{\prime}\rangle$ of a timed automaton $\mathcal{A}$ such that $\mathrm{frac}(\nu)$ has type $\tau$. Then $\langle\ell^{\prime},\nu^{\prime}\rangle$ is reachable from $\langle\ell,\nu\rangle$ in $\mathcal{A}$ if and only if there exists some DBM $\mathcal{M}^{\prime}\in\mathit{closure}(\mathcal{M}_{\tau})$ such that the configuration $\langle\langle\ell^{\prime},\mathcal{M}^{\prime}\rangle,\lfloor{\nu^{\prime}}\rfloor\rangle$ is reachable from $\langle\langle\ell,\mathcal{M}_{\tau}\rangle,\lfloor{\nu}\rfloor\rangle$ in the counter machine $\mathcal{C}_{\langle\ell,\tau\rangle}$ and $\mathrm{frac}(\nu^{\prime})\in\llbracket\mathrm{frac}(\nu)(\mathcal{M}^{\prime})\rrbracket$.

IV-D Reachability Formula

We are now in a position to state our main result.

Theorem 10**.**

Given a timed automaton $\mathcal{A}$ with $n$ clocks and locations $\ell,\ell^{\prime}$, we can compute in exponential time a formula

[TABLE]

in the existential fragment111We claim that this result can be strengthened to state that the reachability relation can be expressed by a quantifier-free formula, again computable in exponential time. To do this one can exploit structural properties of the class of monotonic counter machine that arise from timed automata. We omit details. of $\mathcal{L}_{\mathbb{R},\mathbb{Z}}$ such that there is a finite run in $\mathcal{A}$ from state $\langle\ell,\nu\rangle$ to state $\langle\ell^{\prime},\nu^{\prime}\rangle$ just in case

[TABLE]

Proof.

We give the definition of $\varphi_{\ell,\ell^{\prime}}$ below and justify the complexity bound in Appendix -E.

For simplicity we write formula $\varphi_{\ell,\ell^{\prime}}$ as a disjunction over the collection $\mathrm{Tp}_{n}$ of all $n$-types. However each disjunct only depends on the restriction of the type $\tau$ to the (finite) set of atomic formulas $t\leq t^{\prime}$ with $t,t^{\prime}\in\mathcal{DT}_{\mathbb{R}}(n)$; so $\varphi_{\ell,\ell^{\prime}}$ can equivalently be written as a finite disjunction. We define

[TABLE]

where the subformulas $\alpha^{\tau}$ and $\chi_{\ell,\ell^{\prime}}^{\tau}$ are defined below.

The Hintikka formula $\alpha^{\tau}(r_{1},\ldots,r_{n})$222Recall that by convention $[r_{0}]=[0]$, thus we treat variable $r_{0}$ as synonymous with the constant [math]. is defined by

[TABLE]

Given a valuation $\nu\in\mathbb{R}_{\geq 0}^{\mathcal{X}}$, $\mathrm{frac}(\nu)\models\alpha^{\tau}$ just in case the set of difference formulas satisfied by $\mathrm{frac}(\nu)$ is identical to the set of difference formulas in $\tau$.

Formula $\chi^{\tau}_{\ell,\ell^{\prime}}$ is defined by writing

[TABLE]

Here the subformula $\psi_{\langle\ell,\mathcal{M}_{\tau}\rangle,\langle\ell^{\prime},\mathcal{M}\rangle}$, expresses the reachability relation in the counter machine $\mathcal{C}_{\langle\ell,\tau\rangle}$ between control states $\langle\ell,\mathcal{M}_{\tau}\rangle$ and $\langle\ell^{\prime},\mathcal{M}\rangle$, as per Proposition 7. Recall from Corollary 6 that each $m_{i,j}$ is a difference term involving variables $r_{0},\ldots,r_{n}$. The correctness of $\varphi_{\ell,\ell^{\prime}}$ is immediate from Proposition 7 and Theorem 9. ∎

Example 7**.**

Consider the timed automaton $\mathcal{A}$ in Figure 3. Fix the type $\tau_{1}$ for the valuation $\left(\begin{smallmatrix}0.6\\ 0\end{smallmatrix}\right)$. We illustrate the relevant part of the counter machine $\mathcal{C}_{\langle\ell_{0},\tau_{1}\rangle}$ in Figure 5. States $\langle\ell,\mathcal{M}\rangle$ of the machine comprise a location $\ell$ and parametric DBM $\mathcal{M}$. Moreover, $\mathcal{M}_{0}=\mathcal{M}_{\tau_{1}}$. The placement of a transition between $\langle\ell_{1},\mathcal{M}_{5}\rangle$ and $\langle\ell_{1},\mathcal{M}_{2}\rangle$ relies on the fact that terms $-r_{2}$ and [math] are equivalent with respect to the equivalence relation on terms induced by $\tau_{1}$.

Let $\alpha^{\tau_{1}}$ be the Hintikka formula of the type $\tau_{1}$. Clearly, $\langle 0.6,0\rangle\models\alpha^{\tau_{1}}$. We define $\chi^{\tau}_{\ell_{0},\ell_{1}}$ as follows:

[TABLE]

where $\psi_{1}$, $\psi_{2}$, $\psi_{3}$ and $\psi_{4}$ are given in the following:

[TABLE]

The formulae $\psi_{i}$ (with $i\in\{2,3,4,5\}$) summarise the constraints placed on $r^{\prime}_{1}$ and $r^{\prime}_{2}$ by the parametric DBMs $\mathcal{M}_{i}$ in the counter machine $\mathcal{C}_{\langle\ell_{0},\tau_{1}\rangle}$. See Figure 5 for the given constraints in the parametric DBMs $\mathcal{M}_{i}$. Recall that real-valued variables $r_{i},r^{\prime}_{i}$ range over the interval $[0,1]$.

Let $\tau_{2}$ be the type for the valuation $\left(\begin{smallmatrix}0\\ 0.2\end{smallmatrix}\right)$. In comparison with $\mathcal{C}_{\langle\ell_{0},\tau_{1}\rangle}$, we present the counter machine $\mathcal{C}_{\langle\ell_{0},\tau_{2}\rangle}$ in Figure 6 in Appendix -F.

The formula $\varphi_{\ell_{0},\ell_{1}}$, expressing the set of valuations $\nu$ and $\nu^{\prime}$ such that $\langle\ell_{1},\nu^{\prime}\rangle$ is reachable from $\langle\ell_{0},\nu\rangle$, is then the disjunction of all formulas $\alpha^{\tau}\wedge\chi^{\tau}_{\ell_{0},\ell_{1}}$ for types $\tau\in\mathrm{Tp}_{n}$:

[TABLE]

V Parametric Timed Reachability Logic

Let $\mathcal{A}=\langle L,\mathcal{X},E\rangle$ be a timed automaton augmented with a labelling function $LB:L\rightarrow 2^{AP}$. Let $\varphi$ be a sentence of PTRL. Recall that the model checking problem of $\mathcal{A}$ against $\varphi$ asks, given a state $\langle\ell,\nu\rangle$ of $\mathcal{A}$, whether $\langle\ell,\nu\rangle\models\varphi$.

In this section we prove the following result.

Theorem 11**.**

The model-checking problem for PTRL is decidable in EXPSPACE and is NEXPTIME-hard.

For membership in EXPSPACE, given a timed automaton $\mathcal{A}$, a configuration $\langle\ell,\nu\rangle$ of $\mathcal{A}$, and a sentence $\psi$ of PTRL, we construct in exponential time a sentence $\widetilde{\psi}$ of $\mathcal{L}_{\mathbb{R},\mathbb{Z}}^{*}$ that is true if and only if $\langle\ell,\nu\rangle\models\psi$. We thereby obtain an exponential space algorithm for the model checking problem. We then prove NEXPTIME-hardness by a reduction from SUCCINCT 3-SAT.

V-A Reduction of Model Checking to Satisfiability

The model checking procedure for PTRL relies on a “cut-down” version of Theorem 10, concerning the logical definability of the reachability relation. In this version, given as Lemma 12 below, we do not represent the full reachability relation, but instead abstract the integer parts of all clocks except the reference clock $x_{n}$. This abstraction is sufficient for model-checking PTRL, and moreover allows us to obtain a formula that lies in the sub-logic $\mathcal{L}_{\mathbb{R},\mathbb{Z}}^{*}$, which has better complexity bounds than the full logic $\mathcal{L}_{\mathbb{R},\mathbb{Z}}$.

Given $N\in\mathbb{N}$, define the set $\mathcal{R}_{N}$ of regions to be $\mathcal{R}_{N}=\{0,\ldots,N\}\cup\{\infty\}$. A counter valuation $\upsilon\in\mathbb{N}^{n}$ is abstracted to $Reg(\upsilon)\in\mathcal{R}_{N}^{n}$, where

[TABLE]

The following lemma is proved in Appendix -C.

Lemma 12**.**

Let $\mathcal{A}$ be a timed automaton with $n$ clocks and maximum clock constant $N$. Given two locations $\ell,\ell^{\prime}$ of $\mathcal{A}$ and $R,R^{\prime}\in\mathcal{R}_{N}^{n}$, we can compute in exponential time a quantifier-free $\mathcal{L}_{\mathbb{R},\mathbb{Z}}^{*}$-formula

[TABLE]

such that there is a finite run in $\mathcal{A}$ from state $\langle\ell,\nu\rangle$ to state $\langle\ell^{\prime},\nu^{\prime}\rangle$, where $Reg(\lfloor{\nu}\rfloor)=R$ and $Reg(\lfloor{\nu^{\prime}}\rfloor)=R^{\prime}$ , just in case

[TABLE]

Let $\psi$ be a formula of PTRL of the first type, involving the set of parameters $\theta_{1},\ldots,\theta_{k}$, and let $\mathcal{A}$ be a timed automaton with $n$ clocks and maximum clock constant $N$. For each location $\ell$ of $\mathcal{A}$ and $R\in\mathcal{R}^{n}_{N}$ such that $R_{n}=0$, we obtain a $\mathcal{L}_{\mathbb{R},\mathbb{Z}}^{*}$-formula

[TABLE]

in real variables $\boldsymbol{r}=(r_{1},\ldots,r_{n})$ and $\boldsymbol{s}=(s_{1},\ldots,s_{k})$ and integer variables $\boldsymbol{w}=(w_{1},\ldots,w_{k})$ such that

[TABLE]

for all parameter valuations $\xi\in\mathbb{R}_{\geq 0}^{k}$ and all clock valuations $\nu\in\mathbb{R}_{\geq 0}^{n}$ such that $Reg(\lfloor{\nu}\rfloor)=R$ and $\nu_{n}=0$.

To keep things simple, we assume that every configuration of $\mathcal{A}$ can generate an infinite non-zeno run. It is not difficult to drop this assumption since the collection of configurations from which there exists such a run is a union of clock regions and hence is definable in $\mathcal{L}_{\mathbb{R},\mathbb{Z}}^{*}$. We also assume, without loss of generality, that the reference clock $x_{n}$ is not mentioned in any guard of $\mathcal{A}$.

The construction of $\widetilde{\psi}_{\ell,R}$ is by induction on the structure of $\psi$. The induction cases for the Boolean connectives are straightforward and we concentrate on the induction step for the connective $\exists\lozenge_{\sim\theta}$. In fact we only consider the case that $\sim$ is the equality relation $=$, the cases for $<$ and $>$ being very similar.

Suppose that $\psi\equiv\exists\lozenge_{=\theta_{i}}\psi^{\prime}$ for some PTRL-formula $\psi^{\prime}$ and $i\in\{1,\ldots,k\}$. Then we define

[TABLE]

where $\varphi_{\ell,R,\ell^{\prime},R^{\prime}}$ is the reachability formula defined in Lemma 12. Note that this definition relies on the assumption that the clock $x_{n}$ is never reset by the timed automaton and hence can be used to keep track of global time.

This completes the translation of PTRL-formulas of the first type to formulas of $\mathcal{L}_{\mathbb{R},\mathbb{Z}}^{*}$. Extending this inductive translation to PTRL-formulas of the second type is straightforward, bearing in mind that we represent each parameter $\theta_{i}$ by a variable $w_{i}$ for its integer part and a variable $s_{i}$ for its fractional part. Thus, e.g., the PTRL-formula $\exists\theta_{i}\psi$ is translated as $\exists w_{i}\exists s_{i}(0\leq s_{i}<1\wedge\widetilde{\psi})$.

Given a sentence $\psi$ of PTRL, location $\ell$ of $\mathcal{A}$, and $R\in\mathcal{R}_{N}$, our translation yields a formula $\widetilde{\psi}_{\ell,R}(r_{1},\ldots,r_{n})$ such that for any valuation $\nu$ with $Reg(\lfloor{\nu}\rfloor)=R$ we have $\langle\ell,\nu\rangle\models\psi$ if and only if $\mathrm{frac}(\nu)\models\widetilde{\psi}_{\ell,R}$. By Lemma 12, formula $\widetilde{\psi}_{\ell,R}$ has size singly exponential in the size of $\psi$ and $\mathcal{A}$ and quantifier-depth linear in the size of $\psi$.

The model checking problem then reduces to determining the truth of $\widetilde{\psi}_{\ell,R}$ on $\mathrm{frac}(\nu)$, where $Reg(\lfloor{\nu}\rfloor)=R$. Since satisfiability for sentences of $\mathcal{L}_{\mathbb{R},\mathbb{Z}}^{*}$ can be decided in polynomial space in the formula size and exponential space in the number of quantifiers (by Proposition 2), the model checking problem of PTRL lies in EXPSPACE.

V-B NEXPTIME-Hardness

In this section we show that model checking timed automata against the fixed PTRL sentence $\exists\theta\,\forall\boxempty_{=\theta}p$ is NEXPTIME-hard. We remark that, due to the punctual constraint ${=\!\theta}$, the above formula expresses a synchronization property—there exists a duration $\theta$ such that all runs are in a $p$-state after time exactly $\theta$.

Recall that a Boolean circuit is a finite directed acyclic graph, whose nodes are called gates. An input gate is a node with indegree [math]. All other gates have label either $\vee$, $\wedge$, or $\neg$. An output gate is a node with outdegree [math].

We show NEXPTIME-hardness by reduction from the SUCCINCT 3-SAT problem. The input of SUCCINCT 3-SAT is a Boolean circuit $C$, representing a 3-CNF formula $\varphi_{C}$, and the output is whether or not $\varphi_{C}$ is satisfiable. Specifically, $C$ has $2$ output gates, and the input gates are partitioned into two nonempty sets of respective cardinalities $n$ and $m$. The formula $\varphi_{C}$ has $2^{n}$ variables and $2^{m}$ clauses (in particular, the number of variables and clauses in $\varphi_{C}$ can be exponential in the size of $C$). The first $n$ inputs of $C$ represent the binary encoding of the index $i$ of a variable, and the remaining $m$ inputs of $C$ represent the binary encoding of the index $j$ of a clause in $\varphi_{C}$. The output of $C$ indicates whether the $i$-th variable occurs positively, negatively, or not at all in the $j$-th clause of $\varphi_{C}$. The SUCCINCT 3-SAT problem is NEXPTIME-complete [21].

Given an instance of SUCCINCT 3-SAT, that is, a Boolean circuit $C$ as described above, we construct a timed automaton $\mathcal{A}$ augmented with a labelling function $LB$ such that the 3-CNF formula $\varphi_{C}$ encoded by circuit $C$ is satisfiable if and only if $(\ell,\boldsymbol{0})\models\exists\theta\forall\boxempty_{=\theta}p$ for some designated location $\ell$.

There are two ideas behind the reduction. First we construct a linear bounded automaton $\mathcal{B}$ from the circuit $C$ such that, roughly speaking, the 3-CNF formula $\varphi_{C}$ is satisfiable if and only if there exists an integer $N$ such that, starting from an initial configuration, all length-$N$ paths in the configuration graph of $\mathcal{B}$ end in a configuration with label $p$. The second part of the reduction is to simulate encode the configuration graph of $\mathcal{B}$ as the configuration graph of a timed automaton $\mathcal{A}$.

We construct $\mathcal{B}$ such that its number of control states is polynomial in the size of $C$, and we fix an initial tape configuration of $\mathcal{B}$ of length likewise bounded by a polynomial in the size of $C$. We designate certain transitions of $\mathcal{B}$ as $\checkmark$-transitions. In every computation of $\mathcal{B}$, the sequence of steps between the $i$-th and $(i+1)$-st $\checkmark$-transitions, for $i\in\mathbb{N}$, is referred to as the $i$-th phase of the computation. We design $\mathcal{B}$ so that the number of steps in the $i$-th phase is independent of the nondeterministic choices along the run.

The definition of $\mathcal{B}$ is predicated on a numerical encoding of propositional valuations. Suppose that $X_{1},\ldots,X_{2^{n}}$ are the variables occurring in $\varphi_{C}$, and write $p_{1},\ldots,p_{2^{n}}$ for the first $2^{n}$ prime numbers in increasing order. Given a positive integer $N$, we obtain a Boolean valuation of $X_{1},\ldots,X_{2^{n}}$ in which $X_{j}$ is false if, and only if, $N\bmod p_{j}=0$. With this encoding in hand, we proceed to define $\mathcal{B}$:

In the first phase, $\mathcal{B}$ guesses three $n$-bit numbers $1\leq i_{1},i_{2},i_{3}\leq 2^{n}$ and a single $m$-bit number $1\leq j\leq 2^{m}$ and writes them on its tape. 2. 2.

In the second phase, $\mathcal{B}$ computes the three prime numbers $p_{i_{1}},p_{i_{2}},p_{i_{3}}$ and writes them on its tape. 3. 3.

In the third phase, by simulating the circuit $C$, $\mathcal{B}$ determines whether the propositional variables $X_{i_{1}},X_{i_{2}},X_{i_{3}}$ appear in the $j$-th clause of $\varphi_{C}$, henceforth denoted $\psi_{j}$. If one of them does not appear at all, then $\mathcal{B}$ moves into an accepting self-loop. Otherwise, $\mathcal{B}$ remembers in its state whether $X_{i_{1}},X_{i_{2}},X_{i_{3}}$ appear positively or negatively in $\psi_{j}$, and then $\mathcal{B}$ proceeds to the next phase. 4. 4.

From phase four onwards, $\mathcal{B}$ maintains on its tape three counters, respectively counting modulo $p_{i_{1}},p_{i_{2}},p_{i_{3}}$. In every successive phase, each of these counters is incremented by one. At the end of each phase, $\mathcal{B}$ checks whether the values of the counters encode a satisfying valuation of clause $\psi_{j}$. If this is the case, then $\mathcal{B}$ moves into an accepting state. Otherwise $\mathcal{B}$ proceeds to the next phase.

By construction, $N\in\mathbb{N}$ encodes a satisfying valuation of $\varphi_{C}$ if and only if all computation paths of $\mathcal{B}$ reach an accepting state at the end of the $(N+3)$-rd phase.

It remains to explain how from $\mathcal{B}$ one can define a timed automaton $\mathcal{A}$ whose configuration graph embeds the configuration graph of $\mathcal{B}$. The construction is adapted from the PSPACE-hardness proof for reachability in timed automata [1]. We refer to Appendix -G for details of this construction. In the end, the initial configuration $(\ell,\boldsymbol{0})$ of $\mathcal{A}$ satisfies $\exists\theta`,\forall\boxempty_{=\theta}p$ if and only if $\varphi_{C}$ is satisfiable.

VI Conclusion

We have given a new proof of the result of Comon and Jurski that the reachability relation of a timed automaton is definable in linear arithmetic. In addition to making the result more accessible, our main motivations in revisiting this result concerned potential applications and generalisations. With regard to applications, we have already put the new proof to work in deriving complexity bounds for model checking the reachability fragment of parametric TCTL. In future work we would like to see whether ideas from this paper can be applied to give a more fine-grained analysis of extensions of timed automata, such as timed games and priced timed automata.

We claim that a finer analysis of the complexity of our decision procedure for model checking PTRL yields membership of the problem in the complexity class $\mathrm{STA}(*,2^{O(n)},n)$, i.e., the class of languages accepted by alternating Turing machines running in time $2^{O(n)}$ and making at most $n$ alternations on an input of length $n$. This improved upper bound follows from a refinement of the statement of Proposition 2, on the complexity of the decision problem for $\mathcal{L}^{*}_{\mathbb{R},\mathbb{Z}}$, to state that the truth of a prenex-form sentences of size $n$ and with $k$ quantifier alternations can decided by a polynomial time alternating Turing machine, making at most $k$ alternations.

We claim also that our NEXPTIME-hardness result can be strengthened to match the new upper bound. The idea here would be to reduce a version of SUCCINCT 3-SAT with quantifier alternation to model checking ${PTRL}$ formulas of the form $Q_{1}\theta_{1}\ldots Q_{k}\theta_{k}\forall\boxempty_{=\theta_{1}}\ldots\forall\boxempty_{=\theta_{k}}p$ for $Q_{1},\ldots,Q_{k}$ a sequence of quantifiers with $k$ alternations.

Details of the improved upper and lower complexity bound will appear in a subsequent version of this paper.

Acknowledgements. This work was partially supported by the EPSRC through grants EP/M012298/1 and EP/M003795/1 and by the German Research Foundation (DFG), project QU 316/1-2.

-A Proof of Proposition 2

We first recall that the language $\mathcal{L}^{*}_{\mathbb{R},\mathbb{Z}}$ has terms of both real-number sort and integer sort, where the atomic formulas:

• •

if integer sort, have form

[TABLE]

for integer variables $z,z^{\prime}$ and integers $c,d$.

• •

if real-number sort, have form $t\leq t^{\prime}$ where $t,t^{\prime}$ are derived by the grammar

[TABLE]

where $c\in\mathbb{Q}$ is a constant and $r\in\{r_{0},r_{1},\ldots\}$ is a real-valued variable.

One can prove Proposition 2 by combining the quantifier-elimination procedures of Ferante and Rackoff [4, 22] for $\mathcal{L}_{\mathbb{R}}$ and To [5, Section 4] for the fragment of Presburger arithmetic in which atomic formulas have the form shown in (5).

To eliminate quantifiers in formulas of real arithmetic, Ferante and Rackoff [4] define an equivalence relation $\mathrel{\mathcal{R}^{k}_{m}}$ on $k$-tuples of real numbers. The relation is such that $\mathrel{\mathcal{R}^{k}_{m}}$-equivalent $k$-tuples agree on all quantifier-free formulas in which all constants have the largest (absolute) constant at most $m$. We refer the reader to [22] for the definition of $\mathrel{\mathcal{R}^{k}_{m}}$; here we just recall the key results.

Let $A^{k}_{m}$ be the set of all affine functions $f:\mathbb{R}^{k}\to\mathbb{R}$ with integer coefficients, where all constants and coefficients have the largest (absolute) constant at most $m$.

Lemma 13** (Lemma 22.3 and 22.4 from [22]).**

Given two $k$-tuples $\boldsymbol{a}=(a_{1},\cdots,a_{k})$ and $\boldsymbol{b}=(b_{1},\cdots,b_{k})$ of real numbers such that $\boldsymbol{a}\mathrel{\mathcal{R}^{k}_{2m^{2}}}\boldsymbol{b}$ for some $m\in\mathbb{Z}_{>0}$, then for all $c\in\mathbb{R}$ there exists $d\in\mathbb{R}$ such that $(\boldsymbol{a},c)\mathrel{\mathcal{R}^{k+1}_{m}}(\boldsymbol{b},d)$. Moreover, $d$ can be chosen to have the form $f(\boldsymbol{b})/e$ where $f\in A^{k}_{2m^{2}}$ and $\lvert e\rvert\leq 2m^{2}$.

To eliminate quantifiers in formulas of the above fragment of Presburger arithmetic, analogue to the relation ${\mathrel{\mathcal{R}^{k}_{m}}}$, To [5, Definition 6] has defined an equivalence relation $\mathrel{\mathcal{Z}^{k}_{p,m}}$ on $k$-tuples of integers, where $p,m\in\mathbb{Z}_{>0}$. The relation is such that ${\mathrel{\mathcal{Z}^{k}_{p,m}}}$-equivalent $k$-tuples agree on all quantifier-free formulas, where all constants have the largest (absolute) constant at most $m$ and the period of the formula is $p$. The period of the formula is the least common multiple of the periods $e$ of each atomic term ${z-z^{\prime}\equiv c}\pmod{e}$. We refer the reader to [5] for the definition of $\mathrel{\mathcal{Z}^{k}_{p,m}}$; here we just recall the key results.

Lemma 14** (Lemma 7 and 8 from [5]).**

Given two $(k+1)$-tuples $\boldsymbol{a}=(a_{0},\cdots,a_{k})$ and $\boldsymbol{b}=(b_{0},\cdots,b_{k})$ of integers such that $a_{0}=b_{0}=0$ and $\boldsymbol{a}\mathrel{\mathcal{Z}^{k}_{p,3m}}\boldsymbol{b}$ for some $p,m>0$, then for all $c\in\mathbb{N}$ there exists $b\in\mathbb{N}$ such that $(\boldsymbol{a},c)\mathrel{\mathcal{Z}^{k+1}_{p,m}}(\boldsymbol{b},d)$. Moreover, $d$ can be chosen such that $0\leq d\leq max(b_{0},\cdots,b_{k})+pm+p$.

Fix $m\in\mathbb{Z}_{>0}$. For all $n\in\mathbb{N}$, define $g(0,m)\stackrel{{\scriptstyle\mathrm{def}}}{{=}}m$ and $g(n+1,m)\stackrel{{\scriptstyle\mathrm{def}}}{{=}}2g(n,m)^{2}$, moreover, define $h(0,m)\stackrel{{\scriptstyle\mathrm{def}}}{{=}}m$ and $h(n+1,m)\stackrel{{\scriptstyle\mathrm{def}}}{{=}}3h(n,m)$.

Lemma 15**.**

Let $\varphi(r_{1},\cdots,r_{k},z_{0},\cdots,z_{k^{\prime}})$ be a formula in $\mathcal{L}^{*}_{\mathbb{R},\mathbb{Z}}$, with $k$ free real-valued variables $r_{i}$ and $k^{\prime}$ free integer variables $z_{i}$, and with $n$ quantifiers over real-valued variables and $n^{\prime}$ quantifiers over integer-valued variables, where $m$ is the largest (absolute) constant and $p$ is the period of the formula. Suppose $\boldsymbol{a},\boldsymbol{b}\in\mathbb{R}^{k}$ are $k$-tuples of real numbers such that $\boldsymbol{a}\mathrel{\mathcal{R}^{k}_{g(n,m)}}\boldsymbol{b}$. Suppose $\boldsymbol{a^{\prime}},\boldsymbol{b^{\prime}}\in\mathbb{N}^{k^{\prime}}$ are $k^{\prime}$-tuples of integers such that $\boldsymbol{a^{\prime}}\mathrel{\mathcal{Z}^{k^{\prime}}_{p,h(n^{\prime},m)}}\boldsymbol{b^{\prime}}$. Then, we have

[TABLE]

Proof.

The proof is by an induction on the structure of the formula. For atomic formulas, each sort, the result is immediate from the definition of equivalence relations $\mathrel{\mathcal{R}^{k}_{m}}$ and $\mathrel{\mathcal{Z}^{k}_{p,m}}$. For the Boolean connectives, the result is straightforward using the induction hypothesis for each subformula.

• •

For formulas $\exists r\,\varphi(\boldsymbol{a},\boldsymbol{a^{\prime}},r)$, where $r$ is a real-valued variable: suppose $\exists r\,\varphi(\boldsymbol{a},\boldsymbol{a^{\prime}},r)$ holds, and let $c\in R$ be such that $\varphi(\boldsymbol{a},\boldsymbol{a^{\prime}},c)$ holds. Since $\boldsymbol{a}\mathrel{\mathcal{R}^{k}_{g(n,m)}}\boldsymbol{b}$, by Lemma 13, there exists some $d$ such that $(\boldsymbol{a},c)\mathrel{\mathcal{R}^{k+1}_{g(n-1,m)}}(\boldsymbol{b},d)$. Applying the induction hypothesis, $\exists r\,\varphi(\boldsymbol{b},\boldsymbol{b^{\prime}},r)$ holds, too.

• •

For formulas $\exists z\,\varphi(\boldsymbol{a},\boldsymbol{a^{\prime}},z)$, where $z$ is a integer-valued variable: suppose $\exists z\,\varphi(\boldsymbol{a},\boldsymbol{a^{\prime}},z)$ holds, and let $c^{\prime}\in R$ be such that $\varphi(\boldsymbol{a},\boldsymbol{a^{\prime}},c^{\prime})$ holds. Since $\boldsymbol{a^{\prime}}\mathrel{\mathcal{Z}^{k}_{p,h(n^{\prime},m)}}\boldsymbol{b^{\prime}}$, by Lemma 13, there exists some $d^{\prime}$ such that $(\boldsymbol{a^{\prime}},c^{\prime})\mathrel{\mathcal{Z}^{k+1}_{p,h(n^{\prime}-1,m)}}(\boldsymbol{b^{\prime}},d^{\prime})$. Applying the induction hypothesis, $\exists z\,\varphi(\boldsymbol{b},b^{\prime},z)$ holds, too.

The step of induction for formulas $\forall r\,\varphi(\boldsymbol{a},a^{\prime},r)$ and $\forall z\,\varphi(\boldsymbol{a},a^{\prime},z)$ are similar. ∎

Given a prenex-form sentence $\varphi$ of $\mathcal{L}^{*}_{\mathbb{R},\mathbb{Z}}$, using Lemma 15 we derive an equivalent formula in which all quantifiers range over finite domains. Specifically, if $\varphi$ has $n$ quantifiers over real variables and $n^{\prime}$ quantifiers over integer variables, maximum constant $m$, and period $p$, then the real-valued quantifiers can be restricted to range over rationals whose numerator and denominator is at most $g(n,m)=2^{2^{n}-1}m^{2^{n}}=2^{2^{O(n+\log\log m)}}$ and the integer quantifiers can be restricted to range over numbers of the largest (absolute) constant at most $p(n^{\prime}+1)h(n^{\prime},m)+p(n^{\prime}+1)=p(n^{\prime}+1)3^{n^{\prime}}(m+1)=2^{O(n^{\prime}+\log m+\log p)}$. Thus the truth of $\varphi$ can be established by an alternating Turing machine using space exponential in $n+n^{\prime}$ and polynomial in the size of the quantifier-free part of $\varphi$. This concludes the proof of Proposition 2.

-B Proof of Lemma 3

In this section we prove Lemma 3 from Subsection III-B.

Recall that DBMs have entries in $\mathbb{V}=(\{<,\leq\}\times\mathbb{R})\cup\{(<,\infty)\}$. In this section we denote the order $\leq_{\mathbb{V}}$ simply by $\leq$ (and the corresponding strict order by $<$). Recall that a DBM is atomic if all but at most one entry is the trivial constraint $(<,\infty)$. Recall also that DBM $M$ is consistent if $(\leq,0)\leq M_{i,i}$ for all $0\leq i\leq n$. Write $\mathbb{Z}_{\infty}$ for $\mathbb{Z}\cup\{\infty\}$.

-B1 Tightness

In order to prove Lemma 3, we first introduce the concept of tightness for DBMs and prove that, for a clock valuation $\nu\in[0,1]^{n}$, every DBM in $\mathit{closure}(M_{\nu})$ is tight.

Let $M$ be a DBM of dimension $(n+1)\times(n+1)$. We say that $M$ is tight if $M_{i,j}=M_{i,n}+M_{n,j}$ for every pair of indices $i,j$ with $m_{i,j}\not\in\mathbb{Z}_{\infty}$.

Proposition 16**.**

If $M$ is tight, then $\overrightarrow{M}$ is tight.

Proof.

Write $M^{\prime}=\overrightarrow{M}$ and assume that $m^{\prime}_{i,j}\not\in\mathbb{Z}_{\infty}$ for some $0\leq i,j\leq n$. We show that $M^{\prime}_{i,j}=M^{\prime}_{i,n}+M^{\prime}_{n,j}$. Indeed, since $m^{\prime}_{i,j}\not\in\mathbb{Z}_{\infty}$ we have $j\neq 0$ and thus

[TABLE]

∎

Proposition 17**.**

Suppose that $M$ is tight and $M^{\prime}$ is atomic. Then $M^{\prime\prime}=M\cap M^{\prime}$ is tight.

Proof.

Suppose that $m^{\prime\prime}_{i,j}\not\in\mathbb{Z}_{\infty}$. We show that $M^{\prime\prime}_{i,j}=M^{\prime\prime}_{i,n}+M^{\prime\prime}_{n,j}$. There are two main cases. First suppose that $M^{\prime\prime}_{i,j}=M_{i,j}$. Then

[TABLE]

Since we assume that $M^{\prime\prime}_{i,j}=M_{i,j}$, all the inequalities above are tight and we conclude that $M^{\prime\prime}_{i,j}=M^{\prime\prime}_{i,n}+M^{\prime\prime}_{n,j}$.

The second case is that $M^{\prime\prime}_{i,j}<M_{i,j}$. Then by definition of $M^{\prime\prime}$ we have $M^{\prime\prime}_{i,j}=M_{i,p}+M^{\prime}_{p,q}+M_{q,j}$. Since $m^{\prime\prime}_{i,j}\not\in\mathbb{Z}_{\infty}$, we must have either $m_{i,p}\not\in\mathbb{Z}_{\infty}$ or $m_{q,j}\not\in\mathbb{Z}_{\infty}$. We will handle the first of these two subcases; the second follows by symmetric reasoning.

If $m_{i,p}\not\in\mathbb{Z}_{\infty}$ then

[TABLE]

But $M^{\prime\prime}_{i,j}\leq M^{\prime\prime}_{i,n}+M^{\prime\prime}_{n,j}$ by canonicity of $M^{\prime\prime}$. Hence $M^{\prime\prime}_{i,j}=M^{\prime\prime}_{i,n}+M^{\prime\prime}_{n,j}$. ∎

Proposition 18**.**

Suppose that $M$ is tight.

If $\ell\neq n$ then $M[x_{\ell}\leftarrow 0]$ is tight. 2. 2.

$(M\cap(x_{n}=1))[x_{n}\leftarrow 0]$* is tight.*

Proof.

Write $M^{\prime}=M[x_{\ell}\leftarrow 0]$, where $\ell\neq n$, and assume that $m^{\prime}_{i,j}\not\in\mathbb{Z}_{\infty}$. We show that $M^{\prime}_{i,j}=M^{\prime}_{i,n}+M^{\prime}_{n,j}$.

Indeed we have

[TABLE] 2. 2.

Write $M^{\prime}=M\cap(x_{n}=1)$. We know from Proposition 17 that $M^{\prime}$ is tight. Moreover we have $M^{\prime}_{n,0}=(\leq,1)$ and $M^{\prime}_{0,n}=(\leq,-1)$. Now write $M^{\prime\prime}=M^{\prime}[x_{n}\leftarrow 0]$ and assume that $m^{\prime\prime}_{i,j}\not\in\mathbb{Z}_{\infty}$. We show that $M^{\prime\prime}_{i,j}=M^{\prime\prime}_{i,n}+M^{\prime\prime}_{n,j}$. The equality is trivial if $i=n$ or $j=n$, so we may suppose that $i,j\neq n$.

Then we have

[TABLE]

∎

Proposition 19**.**

Let $\nu\in[0,1]^{n}$ be a valuation. Then every DBM $M\in\mathit{closure}(M_{\nu})$ is tight.

Proof.

$M_{\nu}$ is obviously tight. Then by induction, using Propositions 16, 17, and 18, every DBM in $\mathit{closure}(M_{\nu})$ is tight. ∎

-B2 DBM Operators Preserve Well-Supportedness

Proof of Lemma 3.

Assume that $\nu\in[0,1]^{n}$ is a clock valuation. We prove that all consistent DBMs $M\in\mathit{closure}(M_{\nu})$ are well-supported. To this end, define

[TABLE]

It suffices to show that every consistent DBM in $\mathit{closure}(M_{\nu})$ has entries in $\mathrm{Supp}_{\nu}$. Indeed we have already noted that all consistent DBMs in $\mathit{closure}(M_{\nu})$ are $1$-bounded; but an entry of $\mathrm{Supp}_{\nu}$ lies in the interval $[-1,1]$ only if it has the form $c+\nu_{i}-\nu_{j}$ for $c\in\{-1,0,1\}$ and $0\leq i,j\leq n$.

We prove that every consistent DBM in $\mathit{closure}(M_{\nu})$ has entries in $\mathrm{Supp}_{\nu}$ by induction on the sequence of operations producing such a DBM.

Base case. The DBM $M_{\nu}$ is obviously well-supported, since its $(i,j)$-th entry is $\nu_{i}-\nu_{j}\in\mathrm{Supp}_{\nu}$ for all $0\leq i,j\leq n$.

Induction step. Let $M(\prec_{i,j},m_{i,j})\in\mathit{closure}(M_{\nu})$ be a DBM and assume that each entry $m_{i,j}$ lies in $\mathrm{Supp}_{\nu}$. We prove that all entries of the DBMs $\overrightarrow{M}\cap\bigcap_{i=1}^{n}(x_{i}\leq 1)$, $M[x_{\ell}\leftarrow 0]$, and $M\cap M^{\prime}$, for $M^{\prime}$ atomic, also lie in $\mathrm{Supp}_{\nu}$ provided that these DBMs are consistent.

It is clear that each entry of $M[x_{\ell}\leftarrow 0]$ lies in $\mathrm{Supp}_{\nu}$ since reset only permutes the entries of a DBM and introduces [math] as a new entry. Likewise it is clear that each entry of $\overrightarrow{M}$ also lies in $\mathrm{Supp}_{\nu}$. Thus to complete the inductive argument it suffices to show that for any DBM $M$ with entries in $\mathrm{Supp}_{\nu}$ and any atomic DBM $M^{\prime}$, all entries of $M\cap M^{\prime}$ are contained in $\mathrm{Supp}(\nu)$ if $M\cap M^{\prime}$ is consistent.

Let $M^{\prime}=\{(\prec^{\prime}_{i,j},m^{\prime}_{i,j})\}$ be an atomic DBM whose single non-trivial constraint is $M^{\prime}_{p,q}$ for some indices $p,q$ (i.e., all other entries are $(<,\infty)$). Then $m^{\prime}_{p,q}\in\mathbb{Z}$ by definition of atomic DBMs. Recall that the DBM $M^{\prime\prime}=M\cap M^{\prime}$ is given by

[TABLE]

for all indices $i,j$. Suppose $M^{\prime\prime}=M\cap M^{\prime}$ is consistent and recall by Proposition 19 that $M$ is tight.

Fix indices $0\leq i,j\leq n$. We show that $m^{\prime\prime}_{i,j}\in\mathrm{Supp}_{\nu}$. If $M^{\prime\prime}_{i,j}=M_{i,j}$ then $m^{\prime\prime}_{i,j}\in\mathrm{Supp}_{\nu}$ by the induction hypothesis. So we may suppose that

[TABLE]

By the induction hypothesis, $m_{i,p},m_{q,j}\in\mathrm{Supp}_{\nu}$. From (6) we must have $m_{i,p},m_{q,j}<\infty$. We now consider three cases.

Suppose that $m_{i,p}\in\mathbb{Z}$. Then $m^{\prime\prime}_{i,j}$ has the form $d+m_{q,j}$ for some integer $d$, and hence $m^{\prime\prime}_{i,j}\in\mathrm{Supp}_{\nu}$ by the induction hypothesis. 2. 2.

Suppose that $m_{q,j}\in\mathbb{Z}$. Then $m^{\prime\prime}_{i,j}$ has the form $d+m_{i,p}$ for some integer $d$, and hence $m^{\prime\prime}_{i,j}\in\mathrm{Supp}_{\nu}$ by the induction hypothesis. 3. 3.

The final case is that $m_{i,p},m_{q,j}\not\in\mathbb{Z}_{\infty}$. Then

[TABLE]

But this contradicts (6) and so this case cannot hold.

∎

-C Proof of Propositions 7 and Lemma 12

Let $\Sigma=\{a_{1},\ldots,a_{n}\}$ be a finite alphabet. Define a function $\pi:\Sigma^{*}\rightarrow\mathbb{N}^{n}$ such that $\pi(w)_{i}$ is the number of occurrences of letter $a_{i}$ in $w$ for $i=1,\ldots,n$. The image of a language $L\subseteq\Sigma^{*}$ under $\pi$ is called the Parikh image (or commutative image) of $L$. It is well known that the Parikh image of any regular language (indeed any context-free language) is definable in Presburger arithmetic. In particular, the Parikh image of the language of an NFA over a unary alphabet is a union of arithmetic progressions. Chrobak and Martinez [23, 24] show that the Parikh image of the language of an $n$-state NFA $\mathcal{A}$ over a unary alphabet comprises $O(n^{2})$ many arithmetic progressions which can be explicitly computed from $\mathcal{A}$ in polynomial time.

Consider a monotonic counter machine $\mathcal{C}=(S,C,\Delta)$. Let $N$ be the maximum constant appearing in a transition guard. Define the set $\mathcal{R}_{N}$ of regions to be $\mathcal{R}_{N}=\{0,\ldots,N\}\cup\{\infty\}$. A counter valuation $\upsilon\in\mathbb{N}^{n}$ defines a tuple $Reg(\upsilon)\in\mathcal{R}_{N}^{n}$ by

[TABLE]

Intuitively $\infty$ represents any counter value strictly greater than $N$. The satisfaction relation $\models$ between regions and guards is defined in the obvious way. Below we define a finite automaton $[\mathcal{C}]$ that simulates $\mathcal{C}$.

The alphabet of $[\mathcal{C}]$ is $\Sigma=\{\mathit{inc}_{1},\ldots,\mathit{inc}_{n}\}$. Intuitively $[\mathcal{C}]$ performs an $\mathit{inc}_{i}$-transition when simulating an increment on counter $c_{i}$. A state of $[\mathcal{C}]$ is a tuple $\langle s,R,\lambda\rangle$, where $s\in S$, $R\in\mathcal{R}_{N}^{n}$ is a region of $\mathcal{C}$, and $\lambda\subseteq C$. With a configuration $\langle s,\upsilon\rangle$ in a run $\rho$ of $\mathcal{C}$ we associate a state $\langle s,Reg(\upsilon),\lambda\rangle$ of $[\mathcal{C}]$. Intuitively, $\lambda$ represents the set of counters that will be reset along the suffix of the run $\rho$ starting from $\langle s,\upsilon\rangle$.

The transition relation of $[\mathcal{C}]$ is defined as follows:

• •

For each edge $\langle s,\varphi,\mathit{reset}(c_{i}),s^{\prime}\rangle\in\Delta$ we add a transition $\langle s,R,\lambda\rangle\stackrel{{\scriptstyle\varepsilon}}{{\longrightarrow}}\langle s^{\prime},R^{\prime},\lambda^{\prime}\rangle$ if $R\models\varphi$, $R^{\prime}_{i}=0$, $R^{\prime}_{j}=R_{j}$ for $j\neq i$, and $\lambda^{\prime}\cup\{c_{i}\}=\lambda$.

• •

For each edge $\langle s,\varphi,\mathit{nop},s^{\prime}\rangle\in\Delta$ we add a transition $\langle s,R,\lambda\rangle\stackrel{{\scriptstyle\varepsilon}}{{\longrightarrow}}\langle s^{\prime},R,\lambda\rangle$ if $R\models\varphi$.

• •

For each edge $\langle s,\varphi,\mathit{inc}(c_{i}),s^{\prime}\rangle\in\Delta$ we add a transition $\langle s,R,\lambda\rangle\stackrel{{\scriptstyle\sigma}}{{\longrightarrow}}\langle s^{\prime},R^{\prime},\lambda\rangle$ if $R\models\varphi$, $R^{\prime}_{i}=R_{i}+1$, and $R^{\prime}_{j}=R_{j}$ for $j\neq i$. The label $\sigma$ is $\mathrm{inc}_{i}$ if $c_{i}\not\in\lambda$ and otherwise $\sigma$ is $\varepsilon$.

By construction of $[\mathcal{C}]$, there is a run of $\mathcal{C}$ from $\langle s,\upsilon\rangle$ to $\langle s^{\prime},\upsilon^{\prime}\rangle$ along which the collection of counters that are reset is $\lambda=\{c_{1},\ldots,c_{m}\}$ only if there is a run of $[\mathcal{C}]$ from $\langle s,Reg(\upsilon),\lambda\rangle$ to $\langle s^{\prime},Reg(\upsilon^{\prime}),\emptyset\rangle$. If $w\in\Sigma^{*}$ is the word read along such a run then we have

[TABLE]

Fix states $\langle s,R,\lambda\rangle$ and $\langle s^{\prime},R^{\prime},\emptyset\rangle$ of $[\mathcal{C}]$. Let $L_{\langle s,R,\lambda\rangle,\langle s^{\prime},R^{\prime},\emptyset\rangle}$ be the set of words $w$ on which $[\mathcal{C}]$ has a run from $\langle s,R,\lambda\rangle$ to $\langle s^{\prime},R^{\prime},\emptyset\rangle$. Then the Parikh image $\pi(L_{\langle s,R,\lambda\rangle,\langle s^{\prime},R^{\prime},\emptyset\rangle})$ is expressible by a formula $\psi(z_{1},\ldots,z_{n})$ of Presburger arithmetic.

Returning to the counter machine $\mathcal{C}$, we wish to express the reachability relation of $\mathcal{C}$ between two controls states $s$ and $s^{\prime}$. The idea is that for each initial counter valuation $\upsilon$ and each run of $\mathcal{C}$ from $\langle s,\upsilon\rangle$ to $s^{\prime}$, we need to specify the total number of increments for each counter that is never reset along the run and the total number of increments since the last reset for all other counters. With this in mind, using Equation (7), the $\mathcal{L}_{\mathbb{Z}}$-formula

[TABLE]

describes the subset of the reachability relation arising from the runs of $\mathcal{C}$ whose projection on $[\mathcal{C}]$ goes from state $\langle s,R,\lambda\rangle$ to $\langle s^{\prime},R^{\prime},\emptyset\rangle$, for $\lambda=\{c_{1},\ldots,c_{m}\}$. The reachability relation of $\mathcal{C}$ can clearly be described as a finite disjunction of such formulas. This concludes the proof of Proposition 7.

The following specialisation of Proposition 7 is used in the proof of Lemma 12.

Proposition 20**.**

Let $\mathcal{C}$ be a monotonic counter machine with $n$ counters and with $N$ the maximum integer constant appearing in a transition guard. Given states $s,s^{\prime}$ of $\mathcal{C}$ and $R,R^{\prime}\in\mathcal{R}_{N}^{n}$, the set

[TABLE]

is definable by a quantifier-free formula of $\mathcal{L}^{*}_{\mathbb{R},\mathbb{Z}}$ (involving only integer terms) that is computable in time polynomial in (the largest (absolute) constant of) $N$ and the number of states and counters of $\mathcal{C}$.

Proof.

We start by defining an NFA $\mathcal{B}$, over a singleton alphabet $\{\mathit{inc}_{n}\}$. Automaton $\mathcal{B}$ can be seen as a “sub-automaton” of the NFA $[\mathcal{C}]$ from the proof of Proposition 7. Specifically the states of $\mathcal{B}$ are those states $\langle s^{\prime\prime},R^{\prime\prime},\lambda\rangle$ of $[\mathcal{C}]$ such that either $\lambda=C$ or $\lambda=C\setminus\{c_{n}\}$. (This last condition means that all increments of counters other than $c_{n}$ are represented in $\mathcal{B}$ by $\varepsilon$-transitions.) For the fixed states and regions $s,R,s^{\prime},R^{\prime}$, as in the statement of the proposition, the initial states of $\mathcal{B}$ are those of the form $\langle s,R,\lambda\rangle$, where $\lambda=C$ or $\lambda=C\setminus\{c_{n}\}$, and the accepting states those of the form $\langle s^{\prime},R^{\prime},C\setminus\{c_{n}\}\rangle$.

Then the Parikh image of the language of $\mathcal{B}$ is equal to

[TABLE]

We can now appeal to the above-mentioned result of Chrobak and Martinez [23, 24] to get that the set (8) is definable by a quantifier-free formula of Presburger arithmetic that is computable in time polynomial in the number of states of $\mathcal{B}$, that is, polynomial in the largest (absolute) constant of $N$ and the number of states and counters of $\mathcal{C}$. ∎

The proof of Lemma 12 is exactly the same as the proof Theorem 10, except that we replace the use of Proposition 7 by Proposition 20, so as to obtain a quantifier-free formula in $\mathcal{L}^{*}_{\mathbb{R},\mathbb{Z}}$.

-D Proof of Proposition 8

We first give the “soundness” direction of the proof, that is, from runs of the counter machine $\mathcal{C}_{\langle\ell,\nu\rangle}$ to runs of $\mathcal{A}$.

Suppose that

[TABLE]

is a run of $\mathcal{C}_{\langle\ell,\nu\rangle}$ with $\ell_{0}=\ell$, $\upsilon^{0}=\lfloor{\nu}\rfloor$ and $\llbracket M_{0}\rrbracket=\{\mathrm{frac}(\nu)\}$. Given any valuation $\nu^{(k)}\in\llbracket M_{k}\rrbracket$, we construct a sequence of valuations $\nu^{(0)},\ldots,\nu^{(k-1)}$, with $\nu^{(j)}\in\llbracket M_{j}\rrbracket$ for $j=0,\ldots,k-1$, such that

[TABLE]

is a run of $\mathcal{A}$. Note that then we must have $\nu^{(0)}=\mathrm{frac}(\nu)$.

The construction of $\nu^{(j)}$ is by backward induction on $j$. The base step, valuation $\nu^{(k)}$, is given. The induction step divides into three cases according to the nature of the transition $\langle\langle\ell_{j-1},M_{j-1}\rangle,\upsilon^{(j-1)}\rangle\longrightarrow\langle\langle\ell_{j},M_{j}\rangle,\upsilon^{(j)}\rangle$. (Recall the classification of transitions in the definition of $\mathcal{C}_{\langle\ell,\nu\rangle}$.)

• •

$\langle\langle\ell_{j-1},M_{j-1}\rangle,\upsilon^{(j-1)}\rangle\longrightarrow\langle\langle\ell_{j},M_{j}\rangle,\upsilon^{(j)}\rangle$ is a delay transition. Then we have $M_{j}=\overrightarrow{M_{j-1}}\cap[0,1]^{n}$, $\ell_{j}=\ell_{j-1}$, and $\upsilon^{(j)}=\upsilon^{(j-1)}$. Thus we can pick $\nu^{(j-1)}\in\llbracket M_{j-1}\rrbracket$ such that $\nu^{(j)}=\nu^{(j-1)}+d$ for some $d\geq 0$. Thus there is a delay transition

[TABLE]

in $\mathcal{A}$.

• •

$\langle\langle\ell_{j-1},M_{j-1}\rangle,\upsilon^{(j-1)}\rangle\longrightarrow\langle\langle\ell_{j},M_{j}\rangle,\upsilon^{(j)}\rangle$ is a wrapping transition. Then we have $M_{j}=(M_{j-1}\cap(x_{i}=1))[x_{i}\leftarrow 0]$ for some index $i$. Thus we can pick $\nu^{(j-1)}\in\llbracket M_{j-1}\cap(x_{i}=1)\rrbracket$ such that $\nu^{(j)}=\nu^{(j-1)}[x_{i}\leftarrow 0]$. In this case we have

[TABLE]

• •

$\langle\langle\ell_{j-1},M_{j-1}\rangle,\upsilon^{(j-1)}\rangle\longrightarrow\langle\langle\ell_{j},M_{j}\rangle,\upsilon^{(j)}\rangle$ is a discrete transition. Let the corresponding edge of $\mathcal{A}$ be $\langle\ell_{j-1},\varphi,\{x_{i}\},\ell_{j}\rangle$. Then we have $M_{j}=(M_{j-1}\cap\varphi_{\mathsf{frac}})[x_{i}\leftarrow 0]$. Thus we may pick $\nu^{(j-1)}\in\llbracket M_{j-1}\cap\varphi_{\mathsf{frac}}\rrbracket$ such that $\nu^{(j-1)}[x_{i}\leftarrow 0]=\nu^{(j)}$. Since $\upsilon^{(j-1)}\models\varphi_{\mathsf{int}}$ we have that $\upsilon^{(j-1)}+\nu^{(j-1)}\models\varphi$. Thus there is a discrete transition

[TABLE]

in $\mathcal{A}$.

We now give the “completeness” direction of the proof: from runs of the timed automaton $\mathcal{A}$ to runs of the counter machine $\mathcal{C}_{\langle\ell,\nu\rangle}$.

Suppose that we have a run

[TABLE]

of $\mathcal{A}$, where $\langle\ell_{0},\nu^{(0)}\rangle=\langle\ell,\nu\rangle$. We can transform such a run, while keeping the same initial and final configurations, by decomposing each delay step into a sequence of shorter delays, so that for all $0\leq j\leq k-1$ and all $x\in\mathcal{X}$ the open interval $(\nu^{(j)}(x),\nu^{(j+1)}(x))$ contains no integer. In other words, we break a delay step at any point at which some clock crosses an integer boundary. We can now obtain a corresponding run of $\mathcal{C}_{\langle\ell,\nu\rangle}$ that starts from state $\langle\langle\ell_{0},M_{0}\rangle,\upsilon^{(0)}\rangle$, where $\llbracket M_{0}\rrbracket=\{\mathrm{frac}(\nu)\}$ and $\upsilon^{(0)}=\lfloor\nu^{(0)}\rfloor$, and ends in state $\langle\langle\ell_{k},M_{k}\rangle,\upsilon^{(k)}\rangle$ such that $\nu^{(k)}\in\upsilon^{(k)}+\llbracket M_{k}\rrbracket$.

We build such a run of $\mathcal{C}_{\langle\ell,\nu\rangle}$ by forward induction. In particular, we construct a sequence of intermediate states $\langle\langle\ell_{i},M_{i}\rangle,\upsilon^{(i)}\rangle$, $0\leq i\leq k$, such that $\nu^{(i)}\in\upsilon^{(i)}+\llbracket M_{i}\rrbracket$ for each such $i$. Each discrete transition of $\mathcal{A}$ is simulated by a discrete transition of $\mathcal{C}_{\langle\ell,\nu\rangle}$. A delay transition of $\mathcal{A}$ that ends with set of clocks $\lambda\subseteq\{x_{1},\ldots,x_{n}\}$ being integer valued is simulated by a delay transition of $\mathcal{C}_{\langle\ell,\nu\rangle}$, followed by wrapping transitions for all counters $c_{i}$ for which $x_{i}\in\lambda$.

-E Proof of Theorem 10

Let $\mathcal{A}=\langle L,\mathcal{X},E\rangle$ be a timed automaton with maximum clock constant $N$. We first transform $\mathcal{A}$ so that all guards are conjunctions of atoms of the type appearing in Figure 4. This transformation may lead to an exponential blow-up in the number of edges. In any case, it can be accomplished in time at most $2^{\mathrm{poly}(n)}\cdot\mathrm{poly}(L)$.

Let $\tau$ be an $n$-type. Following Corollary 6 we have observed that $|\mathit{closure}(\mathcal{M}_{\tau})|\leq 2^{\mathrm{poly}(n)}$. It follows that for a location $\ell\in L$ and $n$-type $\tau$, the monotonic counter automaton $\mathcal{C}_{\langle\ell,\tau\rangle}$ can be computed in time at most $2^{\mathrm{poly}(n)}\cdot\mathrm{poly}(|L|)$.

Applying Proposition 7, we get that the formula $\chi^{\tau}_{\ell,\ell^{\prime}}$ can be computed in time at most $2^{\mathrm{poly}(n)}\cdot\mathrm{poly}(|L|,N^{n})$. Furthermore, given $\tau$, the formula $\alpha^{\tau}$ can be computed in time $\mathrm{poly}(n)$.

Finally, the number of disjuncts in (4), i.e., the number of different $n$-types when restricting to formulas $t\leq t^{\prime}$ for $t,t^{\prime}\in\mathcal{DT}_{\mathbb{R}}(n)$, is bounded by $2^{\mathrm{poly}(n)}$.

Putting everything together, the formula $\varphi_{\ell,\ell^{\prime}}$ can be computed in time at most $2^{\mathrm{poly}(n)}\cdot\mathrm{poly}(|L|,N^{n})$, that is, exponential in the size of the original timed automaton $\mathcal{A}$.

-F Symbolic Counter Machines

In this section we illustrate Figure 6 used in Example 7.

-G Proof of Theorem 11

This section we continue the argument of Section V-B showing that model checking parametric timed reachablity logic is NEXPTIME-hard.

It remains to explain how from linear bounded automaton $\mathcal{B}$ one can define a timed automaton $\mathcal{A}$ whose configuration graph embeds the configuration graph of $\mathcal{B}$. The construction is adapted from the PSPACE-hardness proof for reachability in timed automata [1]. We assume that $\mathcal{B}$ uses a binary input alphabet and a fixed tape length of $k$. The main idea is as follows: $\mathcal{A}$ uses $2k+1$ clocks: one clock $y_{i}$ and $z_{i}$ for each tape cell $i$, and one extra clock $x$. The clocks $y_{i}$ and $z_{i}$, respectively, are used to encode the current tape content and the position of the pointer of $\mathcal{B}$, respectively. The clock $x$ is an auxiliary clock that helps to encode this information correctly into the other clocks. Technically, $x$ is used to measure out cycles of two time units, i.e., $x$ is reset to [math] whenever it reaches $2$. The construction is such that the values of $y_{i}$ and $z_{i}$ obey the following policy: whenever $x$ takes value [math], $y_{i}$ takes value $1$ ([math], respectively) if there is a $1$ ([math], respectively) in the $i$-th cell of the tape; and $z_{i}$ takes value $1$ if the position of the pointer is the $i$-th cell, otherwise, $z_{i}$ takes value [math]. We can set these bits appropriately by resetting clocks $y_{i}$ and $z_{i}$ either when $x=1$ or $x=2$, and we can preserve the values of a clock $y_{i}$ or $z_{i}$ between successive cycles by resetting it when it reaches value $2$, see below for more details. Using this idea, $\mathcal{A}$ can be defined such that it only takes transitions at integer times and such that a configuration of $\mathcal{A}$ after $2t$ time steps encodes a configuration of $\mathcal{B}$ after $t$ computation steps for each $t\in\mathbb{N}$.

More formally, the set of locations of $\mathcal{A}$ contains one copy location $q$ for each state $q$ of $\mathcal{B}$, plus some additional auxiliary locations, one of which being an initial location $\ell_{0}$. In the initialization phase, we encode the initial configuration $(q_{0},\sigma_{1})\sigma_{2}\dots\sigma_{k}$ of $\mathcal{B}$, where $q_{0}$ is the initial state of $\mathcal{B}$, and $\sigma_{i}\in\{0,1\}$. For this, we define a transition from $\ell_{0}$ to $q_{0}$, with guard $x=1$, and resetting $x$, $z_{2},\dots,z_{k}$, and we further reset clock $y_{i}$ iff $\sigma_{i}=0$. One can easily observe that if $\mathcal{A}$ reaches $q_{0}$ with clock value $x=0$, then $z_{1}=1$, and $y_{i}=1$ iff the $i$-th cell contains a $1$, while all other clocks have value [math]. This correctly encodes the initial configuration of $\mathcal{B}$. We now proceed with the simulation phase. From locations $q$ that correspond to states of $\mathcal{B}$, we simulate the computation steps from $\mathcal{B}$. Assume, for instance, that the transition relation of $\mathcal{B}$ contains the tuple $(q,0,q^{\prime},0,R)$, i.e., when reading letter [math] in state $q$, $\mathcal{B}$ goes to state $q^{\prime}$, leaves the symbol on the tape as it is, and moves the pointer one position to the right. According to the encoding described above, this means that if $\mathcal{A}$ reaches $q$ with $x=0$, we need to test whether $y_{i}=0$ for the unique $1\leq i\leq k$ such that $z_{i}=1$, and whether $i<k$ (because we want to move the position of the pointer one cell to the right). If this is the case, $\mathcal{A}$ should go to location $q^{\prime}$ and the bit of $z_{i}$ should be reset to $z_{i+1}$. We thus define for every $1\leq i<k$ a transition as shown in the following, where the loops in the auxiliary location in the middle are defined for every $1\leq j\leq k$.

Transitions of $\mathcal{B}$ of other forms can be simulated in a similar way. We finally augment $\mathcal{A}$ with a label function $LB$ that assigns $p$ to a location $q$ iff $q$ is an accepting state of $\mathcal{B}$.

This finishes the proof for NEXPTIME-hardness.