*OPTIONAL comment concerning the title, e. g.,, if a variant or an extended abstract of the paper has appeared elsewhere.

# Reachability and liveness in parametric timed automata

Étienne André  Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy,
France https://lipn.univ-paris13.fr/~andre/ ,  Didier Lime  École Centrale de
Nantes, LS2N UMR CNRS 6004, Nantes, France<EMAIL_ADDRESS>http://pagesperso.ls2n.fr/~lime-d/ and  Olivier H. Roux  École Centrale de
Nantes, LS2N UMR CNRS 6004, Nantes, France<EMAIL_ADDRESS>http://pagesperso.ls2n.fr/~roux-o/

###### Abstract.

We study timed systems in which some timing features are unknown parameters.
Parametric timed automata (PTAs) are a classical formalism for such systems
but for which most interesting problems are undecidable. Notably, the
parametric reachability emptiness problem, i. e., whether at least one
parameter valuation allows to reach some given discrete state, is undecidable.
Lower-bound/upper-bound parametric timed automata (L/U-PTAs) achieve
decidability for reachability properties by enforcing a separation of
parameters used as upper bounds in the automaton constraints, and those used
as lower bounds.

In this paper, we first study reachability. We exhibit a subclass of PTAs
(namely integer-points PTAs) with bounded rational-valued parameters for which
the parametric reachability emptiness problem is decidable. Using this class,
we present further results improving the boundary between decidability and
undecidability for PTAs and their subclasses such as L/U-PTAs.

We then study liveness. We prove that: (1) the existence of at least one
parameter valuation for which there exists an infinite run in an L/U-PTA is
PSPACE-complete; (2) the existence of a parameter valuation such that the
system has a deadlock is however undecidable; (3) the problem of the existence
of a valuation for which a run remains in a given set of locations exhibits a
very thin border between decidability and undecidability.

###### Key words and phrases:

Parametric timed automata, L/U-PTA, reachability, liveness, deadlock-freeness

##  1\. Introduction

Timed automata (TAs) [AD94] are a powerful formalism that extends finite-state
automata with clocks (real-valued variables evolving linearly) that can be
compared with integer constants in locations (“invariants”) and along
transitions (“guards”); additionally, some clocks can be reset to 0 along
transitions. Many interesting problems for TAs (including the reachability of
a location) are decidable. However, the classical definition of TAs is not
tailored to verify systems only partially specified, especially when the value
of some timing constants is not yet known.

We study here behaviors in the context of parametric timed systems, in which
some timing features (e. g., the duration of a task, a transmission delay in a
network, the delay to trigger a watchdog, etc.) are not known and replaced by
symbolic constants, called _parameters_. The objective of verification on such
partially defined systems, is then to synthesize the possible valuations of
parameters such that some properties are satisfied. _Parametric timed
automata_ (PTAs) [AHV93] lift the limitation of timed automata by allowing the
specification and the verification of systems where some of the timing
constants are parametric. PTAs extend TAs through the use of integer- or
rational-valued parameters in place of timing constants in guards and
invariants. PTAs were used to model and verify a variety of case studies, from
hardware circuits to communication protocols.

###  1.1. Related work

####  1.1.1. Decision problems for PTAs

The expressive power of PTAs comes at the price of the undecidability of most
interesting problems. The EF-emptiness problem (“is the set of parameter
valuations such that a given location is reachable empty?”) is undecidable in
general [AHV93], even when parameters are bounded [Mil00], even when only
strict inequalities are used [Doy07], or with a single integer-valued
parameter [BBLS15]. However, bounding the number of parametric clocks and of
parameters may yield decidability. The smallest known numbers of parametric
clocks (i. e., clocks compared with parameters), non-parametric clocks and
parameters leading to undecidability are: three parametric clocks and one
integer-valued parameter [BBLS15] or three parametric clocks and only one
rational-valued parameter [Mil00], or only one parametric clock, three non-
parametric clocks and one rational-valued parameter [Mil00]. Conversely, some
limitations on the numbers of clocks and parameters allow to retrieve
decidability [AHV93, BO14, BBLS15] (see [And19] for a survey).

##### Logics and PTAs

In [Wan96], an approach is proposed for the verification of Parametric TCTL
(PTCTL) formulas, where the problem is decidable. In [BR07], parameters are
allowed both in the model and in the property (a PTCTL formula), and model
checking is decidable with one parametric clock over discrete time, provided
no equality appears in the formula. In [Qua14], it is shown that the MTL-Model
Checking problem is undecidable for PTAs even with a single clock.

####  1.1.2. Decision problems for L/U-PTAs

In [HRSV02], L/U-PTAs are introduced as a subclass of PTAs where each
parameter is either always compared to a clock as a lower bound in guards and
invariants, or always as an upper bound. The EF-emptiness problem is decidable
for L/U-PTAs [HRSV02]. In [BLT09], further results are proved for L/U-PTAs
with integer-valued parameters: emptiness, finiteness and universality of the
set of parameter valuations for which there exists an infinite accepting run
are decidable. The AF-emptiness problem (“is the set of parameter valuations
for which a given location is eventually reached for any run empty?”) is
undecidable for L/U-PTAs [JLR15]. It is also shown in [JLR15] that the
synthesis of the parameters reaching a given location in an L/U-PTA is
intractable in practice. Two further subclasses have been defined in [BLT09]:
L-PTAs and U-PTAs, where all parameters are always lower bounds and always
upper bounds respectively. However, although synthesis algorithms for
reachability properties are dedicated to L-PTAs and U-PTAs in [BLT09], it is
shown in [ALR18] that the full TCTL-emptiness problem is undecidable even for
U-PTAs. The untimed language preservation problem (“given a parameter
valuation, does there exist another valuation with the same untimed
language?”) is undecidable for both PTAs and L/U-PTAs [ALM20].

####  1.1.3. The power of integer points

In [JLR15], PTAs with bounded integer-valued parameters are considered. The
problem of finding parameter valuations such that a given location is
reachable or unavoidable becomes decidable, and two algorithms are provided
that compute the exact such sets of integer valuations in a symbolic manner,
i. e., without performing an exhaustive enumeration. In [ALR15], it is shown
that computing a parametric extrapolation of the integer hull of symbolic
states allows one to synthesize (rational-valued) parameter valuations for
bounded PTAs, guaranteeing the synthesis of at least all integer-valued
valuations, but also sometimes most or even all rational-valued valuations.

###  1.2. Contribution

Following Lamport, properties of systems are often characterized as safety
properties (“something bad will never happen”) and liveness properties
(“something good will eventually happen”) [Lam77]. Safety generally reduces to
reachability. In this paper, we contribute to the study of both reachability
and liveness for PTAs and their subclasses.

####  1.2.1. Reachability

L/U-PTAs is the only non-trivial111The bounded integer PTAs of [JLR15] are
arguably a trivial such subclass (even though the associated analysis
techniques are not).  subclass of PTAs for which the EF-emptiness problem is
decidable for an arbitrary number of clocks and parameters. However, other
results are disappointing: undecidability of AF-emptiness, intractability of
the synthesis [JLR15]. It is hence important to look for further subclasses of
PTAs for which problems may be decidable. It is shown in [JLR15, ALR15] that
integer points play a key role in decidability. Hence, our first contribution
here is to investigate integer-points PTAs (IP-PTAs), that are PTAs where each
symbolic state contains at least one integer point (i. e., an integer
valuation of the clocks and the parameters). We prove that the EF-emptiness
problem is decidable for bounded IP-PTAs (i. e., with a bounded parameter
domain), even when parameters are rational-valued. Although we show that it
cannot be decided whether a bounded PTA is a (bounded) IP-PTA, we give two
sufficient syntactic conditions: we show that bounded L/U-PTAs with non-strict
inequalities are IP-PTAs and, more interestingly, we introduce a new subclass
of “reset-PTAs”, that are also IP-PTAs, and for which, when bounded, the EF-
emptiness problem is hence decidable too. This class is only the second
syntactic subclass of PTAs (after L/U-PTAs) for which this problem is
decidable.

Our second main contribution to reachability is to study several open problems
for PTAs and several known subclasses (as well as the new class of IP-PTAs):
we study here the emptiness and universality of reachability (EF), as well as
unavoidability emptiness (AF). Emptiness is of utmost importance as, without
decidability of the emptiness, exact synthesis is practically ruled out.
Universality checks whether all parameter valuations satisfy a property, which
is important for applications where the designer has no power on some
valuations; this is the case of networks, where some latencies (e. g., the
transmission time of some packets) may be totally arbitrary. Among our
results, we prove in particular that AF-emptiness is undecidable for both
bounded IP-PTAs and bounded L/U-PTAs. Overall, we significantly enhance the
knowledge we have of decidability problems for PTAs and subclasses.

####  1.2.2. Liveness

When a “good” behavior is not always eventually reached, it can be for two
main reasons: either there is a deadlock, a state in which the system cannot
evolve anymore, or there is a livelock, an infinite path never reaching the
“good” behavior. Both situations are captured by the CTL operator EG [CES86].

With the notable exception of [JLR15, ALR18], and to some extent of [BLT09]
which addresses the existence of cycles, all the works cited above focus on
safety properties, through the basic problem of reachability. This is maybe
not so surprising given that most results related to this simpler problem are
already negative.

We nonetheless address here the problem of liveness in PTAs, and more
precisely, with the negative result of [JLR15] on AF-emptiness in mind, we
start from L/U-PTAs with rational-valued parameters and further refine both
the model and the properties. We prove that:

  1. (1)

deciding the existence of at least one parameter valuation for which there
exists an infinite run (discrete cycle) in the automaton is PSPACE-complete;

  2. (2)

deciding the existence of a parameter valuation such that the system has a
deadlock is however undecidable;

  3. (3)

the problem of the existence of a valuation for which a run remains in a given
set of locations exhibits a very thin border between decidability and
undecidability: while this problem is decidable for L/U-PTAs with a bounded
parameter domain with closed bounds, it becomes undecidable if either the
assumption of boundedness or of closed bounds is lifted. This result confirms
that L/U-PTAs stand at the border between decidability and undecidability.

Differently from [BLT09], we use here no accepting locations. In addition, our
parameters are not restricted to be integer-valued, and can be rational-
valued.

###  1.3. About this manuscript

This manuscript is an extended version of [ALR16a, AL17]. In addition to
merging notations and preliminary concepts, and adding all proofs missing in
[ALR16a, AL17], we extended these manuscripts as follows:

  * •

we added more explanations on the technical parts;

  * •

we modified the proof of Theorem 1 (our former version used a “block”
statement in the 2-counter machine, as in [AHV93], which some readers might
find objectionable), impacting all subsequent proofs of Section 4.

###  1.4. Outline

We recall the necessary preliminaries in Section 2. We introduce integer-point
PTAs (IP-PTAs) in Section 3 and study their relationship with existing
results. We then study reachability problems in Section 4 and liveness in
Section 5 for PTAs, L/U-PTAs and various other subclasses. We summarize our
results in Section 6 and discuss perspectives in Section 7.

##  2\. Preliminaries

###  2.1. Clocks, parameters and constraints

Let ${\mathbb{N}}$, ${\mathbb{Z}}$, ${\mathbb{Q}}_{+}$ and ${\mathbb{R}}_{+}$
denote the sets of non-negative integers, integers, non-negative rational
numbers and non-negative real numbers respectively. Let
$\mathcal{I}({\mathbb{N}})$ denote the set of non-necessarily closed intervals
on ${\mathbb{N}}$, i. e., the set of intervals of the form $[a,b]$, $(a,b]$,
$[a,b)$ or $(a,b)$ where $a,b\in{\mathbb{N}}$ and $a\leq b$.

Throughout this paper, we assume a set $X=\\{x_{1},\dots,x_{H}\\}$ of _clocks_
, i. e., real-valued variables that evolve at the same rate. A clock valuation
is a function $w:X\rightarrow{\mathbb{R}}_{+}$. We identify a clock valuation
$w$ with the point $(w(x_{1}),\dots,w(x_{H}))$ of ${\mathbb{R}}_{+}^{H}$. We
write $\vec{0}$ for the clock valuation that assigns $0$ to all clocks. Given
$d\in{\mathbb{R}}_{+}$, $w+d$ denotes the valuation such that
$(w+d)(x)=w(x)+d$, for all $x\in X$. Given $R\subseteq X$, we define the
_reset_ of a valuation $w$, denoted by $[w]_{R}$, as follows: $[w]_{R}(x)=0$
if $x\in R$, and $[w]_{R}(x)=w(x)$ otherwise.

We assume a set $P=\\{p_{1},\dots,p_{M}\\}$ of _parameters_ , i. e., unknown
constants. A parameter valuation $v$ is a function
$v:P\rightarrow{\mathbb{Q}}_{+}$. We identify a valuation $v$ with the point
$(v(p_{1}),\dots,v(p_{M}))$ of ${\mathbb{Q}}_{+}^{M}$. An _integer_ parameter
valuation is a valuation $v$ such that $\forall p\in P,v(p)\in{\mathbb{N}}$.

In the following, we assume ${\bowtie}\in\\{<,\leq,\geq,>\\}$. Throughout this
paper, $\mathit{lt}$ denotes a linear term over $X\cup P$ of the form
$\sum_{1\leq i\leq H}\alpha_{i}x_{i}+\sum_{1\leq j\leq M}\beta_{j}p_{j}+d$,
with $x_{i}\in X$, $p_{j}\in P$, and $\alpha_{i},\beta_{j},d\in{\mathbb{Z}}$.
A _constraint_ $C$ over $X\cup P$ is a conjunction of inequalities of the form
$\mathit{lt}\bowtie 0$. Given a parameter valuation $v$, $v(C)$ denotes the
constraint over $X$ obtained by replacing each parameter $p$ in $C$ with
$v(p)$. Likewise, given a clock valuation $w$, $w(v(C))$ denotes the
expression obtained by replacing each clock $x$ in $v(C)$ with $w(x)$. We say
that $v$ _satisfies_ $C$, denoted by $v\models C$, if the set of clock
valuations satisfying $v(C)$ is nonempty. Given a parameter valuation $v$ and
a clock valuation $w$, we denote by $w|v$ the valuation over $X\cup P$ such
that for all clocks $x$, $w|v(x)=w(x)$ and for all parameters $p$,
$w|v(p)=v(p)$. We use the notation $w|v\models C$ to indicate that $w(v(C))$
evaluates to true. We say that $C$ is _satisfiable_ if $\exists w,v\text{
s.t.\ }w|v\models C$.

A _(parametric) guard_ $g$ is a constraint over $X\cup P$ defined by
inequalities of the form $x\bowtie\sum_{1\leq j\leq M}\beta_{j}p_{j}+d$, with
$\beta_{j}\in\\{0,1\\}$ and $d\in{\mathbb{Z}}$.

Given an arbitrary order on $X\cup P$, valuations can be seen as points in the
real coordinate space of dimension $|X\cup P|$, using $|A|$ to denote the
cardinality of set $A$. Then the set of valuations satisying constraint $C$
can be seen as a convex polyhedron in that vector space. In the sequel, we
will often make the small abuse of using constraint and polyhedron
indifferently.

###  2.2. Parametric timed automata

####  2.2.1. Syntax

Parametric timed automata (PTA) extend timed automata with parameters within
guards and invariants in place of integer constants [AHV93].

######  Definition 1.

A PTA $\mathcal{A}$ is a tuple $\mathcal{A}=(\Sigma,L,\ell_{0},X,P,I,E)$,
where:

  1. (1)

$\Sigma$ is a finite set of actions,

  2. (2)

$L$ is a finite set of locations,

  3. (3)

$\ell_{0}\in L$ is the initial location,

  4. (4)

$X$ is a finite set of clocks,

  5. (5)

$P$ is a finite set of parameters,

  6. (6)

$I$ is the invariant, assigning to every $\ell\in L$ a parametric guard
$I(\ell)$,

  7. (7)

$E$ is a finite set of edges $e=(\ell,g,\sigma,R,\ell^{\prime})$ where
$\ell,\ell^{\prime}\in L$ are the source and target locations,
$\sigma\in\Sigma$, $R\subseteq X$ is a set of clocks to be reset, and $g$ (the
transition guard) is a parametric guard.

Given a parameter valuation $v$, we denote by $v(\mathcal{A})$ the non-
parametric timed automaton where all occurrences of a parameter $p_{i}$ have
been replaced by $v(p_{i})$. In the following, we may denote as a _timed
automaton_ any structure $v(\mathcal{A})$, by assuming a rescaling of the
constants: by multiplying all constants in $v(\mathcal{A})$ by their least
common denominator, we obtain an equivalent timed automaton (with integer
constants, as in [AD94]).

####  2.2.2. Concrete semantics

Let us first recall the concrete semantics of TA.

######  Definition 2 (Concrete semantics of a TA).

Given a PTA $\mathcal{A}=(\Sigma,L,\ell_{0},X,P,I,E)$, and a parameter
valuation $v$, the concrete semantics of $v(\mathcal{A})$ is given by the
timed transition system $(S,s_{0},{\rightarrow})$, with

  * •

$S=\\{(\ell,w)\in L\times{\mathbb{R}}_{+}^{H}\mid w|v\models I(\ell)\\}$

  * •

$s_{0}=(\ell_{0},\vec{0})$

  * •

${\rightarrow}$ consists of the discrete and (continuous) delay transition
relations:

    * –

discrete transitions: $(\ell,w)\stackrel{{\scriptstyle
e}}{{\rightarrow}}(\ell^{\prime},w^{\prime})$, if
$(\ell,w),(\ell^{\prime},w^{\prime})\in S$, there exists
$e=(\ell,g,\sigma,R,\ell^{\prime})\in E$, $w^{\prime}=[w]_{R}$, and
$w|v\models g$.

    * –

delay transitions: $(\ell,w)\stackrel{{\scriptstyle
d}}{{\rightarrow}}(\ell,w+d)$, with $d\in{\mathbb{R}}_{+}$, if $\forall
d^{\prime}\in[0,d],(\ell,w+d^{\prime})\in S$.

Moreover we write $(\ell,w)\stackrel{{\scriptstyle
e}}{{\mapsto}}(\ell^{\prime},w^{\prime})$ for a combination of a delay and
discrete transition where
$((\ell,w),e,(\ell^{\prime},w^{\prime}))\in{\mapsto}$ if $\exists
d,w^{\prime\prime}:(\ell,w)\stackrel{{\scriptstyle
d}}{{\rightarrow}}(\ell,w^{\prime\prime})\stackrel{{\scriptstyle
e}}{{\rightarrow}}(\ell^{\prime},w^{\prime})$.

Given a TA $v(\mathcal{A})$ with concrete semantics $(S,s_{0},{\rightarrow})$,
we refer to the states of $S$ as the _concrete states_ of $v(\mathcal{A})$. A
(concrete) _run_ of $v(\mathcal{A})$ is a possibly infinite alternating
sequence of concrete states of $v(\mathcal{A})$ and edges starting from the
initial concrete state $s_{0}$ of the form $s_{0}\stackrel{{\scriptstyle
e_{0}}}{{\mapsto}}s_{1}\stackrel{{\scriptstyle
e_{1}}}{{\mapsto}}\cdots\stackrel{{\scriptstyle
e_{m-1}}}{{\mapsto}}s_{m}\stackrel{{\scriptstyle e_{m}}}{{\mapsto}}\cdots$,
such that for all $i=0,1,\dots$, $e_{i}\in E$, and
$(s_{i},e_{i},s_{i+1})\in{\mapsto}$. Given a state $s=(\ell,w)$, we say that
$s$ is reachable (or that $v(\mathcal{A})$ reaches $s$) if $s$ belongs to a
run of $v(\mathcal{A})$. By extension, we say that $\ell$ is reachable in
$v(\mathcal{A})$, if there exists a state $(l,w)$ that is reachable. For any
run $\rho$, we note ${\sf Locs}$ the set of locations reached by $\rho$. A
maximal run is a run that is either infinite (i. e., contains an infinite
number of discrete transitions), or that cannot be extended by a discrete
transition. A maximal run is deadlocked if it is finite, i. e., contains a
finite number of discrete transitions. By extension, we say that a TA is
deadlocked if it contains at least one deadlocked run.

####  2.2.3. Symbolic semantics

We now recall the symbolic semantics of parametric timed automata (see e. g.,
[HRSV02, ACEF09, JLR15]).

We first define the _time elapsing_ of a constraint $C$, denoted by
$C^{\nearrow}$, as the constraint over $X$ and $P$ obtained from $C$ by
delaying all clocks by an arbitrary amount of time. That is,
$C^{\nearrow}=\\{w^{\prime}|v\mid w\models v(C)\land\forall x\in
X:w^{\prime}(x)=w(x)+d,d\in{\mathbb{R}}_{+}\\}$. Dually, we define the _past_
of $C$, denoted by $C^{\swarrow}$, as the constraint over $X$ and $P$ obtained
from $C$ by letting time pass backward by an arbitrary amount of time. That
is, $C^{\swarrow}=\\{w^{\prime}|v\mid w\models v(C)\land\forall x\in
X:w^{\prime}(x)+d=w(x),d\in{\mathbb{R}}_{+}\\}$. Given $R\subseteq X$, we
define the _reset_ of $C$, denoted by $[C]_{R}$, as the constraint obtained
from $C$ by resetting the clocks in $R$, and keeping the other clocks
unchanged. We denote by $C{\downarrow_{P}}$ the projection of $C$ onto $P$, i.
e., obtained by eliminating the clock variables (e. g., using Fourier-
Motzkin).

The (sets of clock valuations satisfying the) constraints generated by PTA can
be represented by subsets of ${\mathbb{R}}_{+}^{|X|}$ with a special form
called _parametric zone_ [HRSV02]. A parametric zone is a convex polyhedron
over $X\cup P$ in which all constraints on variables are of the form
$x\bowtie\mathit{plt}$ (parametric rectangular constraints), or
$x_{i}-x_{j}\bowtie\mathit{plt}$ (parametric diagonal constraints), where
$x_{i}\in X$, $x_{j}\in X$ and $\mathit{plt}$ is a parametric linear term over
$P$, i. e., a linear term without clocks ($\alpha_{i}=0$ for all $i$).

A symbolic state is a pair $\mathbf{s}=(\ell,C)$ where $\ell\in L$ is a
location, and $C$ its associated parametric zone. The initial symbolic state
of $\mathcal{A}$ is $\mathbf{s}_{0}=\big{(}\ell_{0},(\\{\vec{0}\\}\land
I(\ell_{0}))^{\nearrow}\land I(\ell_{0})\big{)}$.

The symbolic semantics relies on the $\mathsf{Succ}$ operation. Given a
symbolic state $\mathbf{s}=(\ell,C)$ and an edge
$e=(\ell,g,\sigma,R,\ell^{\prime})$,
$\mathsf{Succ}(\mathbf{s},e)=(\ell^{\prime},C^{\prime})$, with
$C^{\prime}=\big{(}[(C\land g)]_{R}\land
I(\ell^{\prime})\big{)}^{\nearrow}\land I(\ell^{\prime})$. The $\mathsf{Succ}$
operation is effectively computable, using polyhedral operations: note that
the successor of a parametric zone $C$ is a parametric zone (see e. g.,
[JLR15]).

A symbolic run of a PTA is an alternating sequence of symbolic states and
edges starting from the initial symbolic state, of the form
$\mathbf{s}_{0}\stackrel{{\scriptstyle
e_{0}}}{{\Rightarrow}}\mathbf{s}_{1}\stackrel{{\scriptstyle
e_{1}}}{{\Rightarrow}}\cdots\stackrel{{\scriptstyle
e_{m-1}}}{{\Rightarrow}}\mathbf{s}_{m}$, such that for all $i=0,\dots,m-1$, we
have $e_{i}\in E$, and $\mathbf{s}_{i+1}=\mathsf{Succ}(\mathbf{s}_{i},e_{i})$.
In the following, we simply refer to symbolic states belonging to a run of
$\mathcal{A}$ as symbolic states of $\mathcal{A}$.

###  2.3. Subclasses of PTAs

L/U-PTAs [HRSV02] constrain the use of parameters: parameters must be
partitioned between lower-bound parameters (only compared to clocks in
parametric guards as a lower bound) and upper-bound parameters. L/U-PTAs were
notably studied in [HRSV02, BLT09, AL17, ALR18].

######  Definition 3 (L/U-PTA).

An L/U-PTA is a PTA where the set of parameters is partitioned into lower-
bound parameters and upper-bound parameters, where an upper-bound (resp.
lower-bound) parameter $p_{i}$ is such that, for every guard or invariant
constraint $x\bowtie\sum_{1\leq j\leq M}\beta_{j}p_{j}+d$, we have:
$\beta_{i}=1$ implies ${\bowtie}\in\\{\leq,<\\}$ (resp.
${\bowtie}\in\\{\geq,>\\}$).

Recall from our definition of guard that $\beta_{i}$ can only be 0 or 1.

L/U-PTAs enjoy a well-known monotonicity property recalled in the following
lemma (that corresponds to a reformulation of [HRSV02, Prop 4.2]), stating
that increasing upper-bound parameters or decreasing lower-bound parameters
can only add behaviors.

######  Lemma 1.

Let $\mathcal{A}$ be an L/U-PTA and $v$ be a parameter valuation. Let
$v^{\prime}$ be a valuation such that for each upper-bound parameter $p^{+}$,
$v^{\prime}(p^{+})\geq v(p^{+})$ and for each lower-bound parameter $p^{-}$,
$v^{\prime}(p^{-})\leq v(p^{-})$. Then any run of $v(\mathcal{A})$ is a run of
$v^{\prime}(\mathcal{A})$.

In this paper, we will also consider _bounded_ PTAs, i. e., PTAs with a
bounded parameter domain that assigns to each parameter an infimum and a
supremum, both integers.

######  Definition 4 (bounded PTA).

A _bounded PTA_ is $\mathcal{A}_{|\mathit{bounds}}$, where $\mathcal{A}$ is a
PTA, and $\mathit{bounds}:P\rightarrow\mathcal{I}({\mathbb{N}})$ assigns to
each parameter $p$ an interval $[\mathrm{inf},\mathrm{sup}]$,
$(\mathrm{inf},\mathrm{sup}]$, $[\mathrm{inf},\mathrm{sup})$, or
$(\mathrm{inf},\mathrm{sup})$, with
$\mathrm{inf},\mathrm{sup}\in{\mathbb{N}}$. We use
$\mathrm{inf}(p,\mathit{bounds})$ and $\mathrm{sup}(p,\mathit{bounds})$ to
denote the infimum and the supremum of $p$, respectively. Note that we rule
out $\infty$ as a supremum.

We say that a bounded PTA is a _closed bounded PTA_ if, for each parameter
$p$, its ranging interval $\mathit{bounds}(p)$ is of the form
$[\mathrm{inf},\mathrm{sup}]$; otherwise it is an _open bounded PTA_.

We define similarly bounded L/U-PTAs.

Whereas bounded PTAs are naturally a subclass of PTAs, we showed in [ALR16b]
that bounded L/U-PTAs are _incomparable_ with L/U-PTAs: a consequence is that
undecidability results for bounded L/U-PTAs cannot be automatically extended
to L/U-PTAs; conversely, decidability results for L/U-PTAs cannot be
automatically extended to bounded L/U-PTAs.

###  2.4. Decision problems

Let $\mathcal{P}$ be a given a class of decision problems (reachability,
unavoidability, etc.).

$\mathcal{P}$-emptiness problem:
Input: A PTA $\mathcal{A}$ and an instance $\phi$ of $\mathcal{P}$ Problem: Is
the set of parameter valuations $v$ such that $v(\mathcal{A})$ satisfies
$\phi$ empty?

$\mathcal{P}$-universality problem:
Input: A PTA $\mathcal{A}$ and an instance $\phi$ of $\mathcal{P}$ Problem:
Are all parameter valuations $v$ such that $v(\mathcal{A})$ satisfies $\phi$?

Emptiness is the most basic parametric question: is the set of parameter
valuations such that the property holds empty? Universality gives a robustness
quality to the property and permits to effectively abstract an infinite number
of verifications with concrete values.

In this paper, we mainly focus on safety and liveness properties expressed as
basic (non-nested) Computation Tree Locgic (CTL, [CES86]) properties. Given a
TA $\mathcal{A}$ and a subset of its locations $T$:

  * •

Reachability (EF): does there exist a run $\rho$ such that ${\sf
Locs}(\rho)\cap T\neq\emptyset$?

  * •

Safety (AG): for all runs $\rho$, does ${\sf Locs}(\rho)\subseteq T$?

  * •

Unavoidability (AF): for all maximal runs $\rho$, does ${\sf Locs}(\rho)\cap
T\neq\emptyset$?

  * •

Preservability (EG): does there exist a maximal run $\rho$ such that ${\sf
Locs}(\rho)\subseteq T$?

We also consider two variants of EG:

  * •

Deadlock-existence (denoted here by ED): does there exist a finite maximal
run?

  * •

Cycle-existence (denoted here by EC): does there exists an _infinite_ maximal
run?

Finally, note that EF and AG are dual properties, and so are AF and EG. In our
parametric setting this implies means that, for instance, EF-emptiness and AG-
universality are dual, and so are AF-emptiness and EG-universality.

Note that ED-emptiness is equivalent to AC-universality, where AC-universality
asks whether all parameter valuations are such that all maximal runs are
infinite. Conversely, EC-emptiness is equivalent to AD-universality (for all
valuations, all maximal runs are finite).

##  3\. Integer-points parametric timed automata

In this section, we introduce integer-points parametric timed automata (IP-
PTAs for short), i. e., a semantic subclass of PTAs in which any symbolic
state contains at least one integer point.

First, we compare in this section IP-PTAs with L/U-PTAs and show that the
class of bounded IP-PTAs is strictly larger than bounded L/U-PTAs with non-
strict inequalities. Then, our main result regarding this class will be to
prove the decidability of the EF-emptiness problem for bounded IP-PTAs
(Section 4.3). We will also show that synthesis is intractable in practice,
and that the same holds for bounded L/U-PTAs (Section 4.4). Finally, although
we prove that the membership problem is undecidable for IP-PTAs, we will
exhibit a syntactic sufficient condition, that provides a new subclass of PTAs
for which the EF-emptiness problem is decidable (Section 4.5).

######  Definition 5.

A PTA $\mathcal{A}$ is said to be an _integer points PTA_ (in short _IP-PTA_)
if, in any reachable symbolic state $(\ell,C)$ of $\mathcal{A}$, $C$ contains
at least one integer point.

Let us now compare IP-PTAs and L/U-PTAs. We first need the following lemma,
stating that any reachable symbolic state of an L/U-PTA contains an integer
parameter valuation.

######  Lemma 2.

Let $(\ell,C)$ be a reachable symbolic state of an L/U-PTA. Then
$C{\downarrow_{P}}$ contains at least one integer point.

###### Proof.

Consider a (non-empty) reachable symbolic state $(\ell,C)$ of an L/U-PTA. Let
$v\models C{\downarrow_{P}}$. From the well-known monotonicity property of
L/U-PTAs (recalled in Lemma 1), any parameter valuation such that the lower-
bound parameters $p_{i}^{-}$ are lower or equal to $v(p_{i}^{-})$ and upper-
bound parameters $p_{j}^{+}$ are greater than or equal to $v(p_{j}^{+})$ also
belong to $C{\downarrow_{P}}$. In particular, this is the case of the integer
parameter valuation assigning 0 to all lower-bound parameters, and assigning
to upper-bound parameters $p_{j}^{+}$ the smallest integer greater than or
equal to $v(p_{j}^{+})$. ∎

The previous lemma that ensures the presence of an integer parameter valuation
in any symbolic state does not guarantee that an L/U-PTA is an IP-PTA, because
clocks may have non-integer values.

######  Proposition 1.

The class of IP-PTAs is incomparable with the class of L/U-PTAs.

###### Proof.

  * •

Consider an L/U-PTA with a transition guarded by $x>0$ and resetting no clock,
followed by a second location with invariant $x<1$; then, necessarily, the
symbolic state associated with this second location contains no integer point
(as $x\in(0,1)$ in that symbolic state).

  * •

It is easy to exhibit an IP-PTA that is not an L/U-PTA. This is for example
the case of a simple PTA with only one location, one clock $x$ and one
parameter $p$ with a self-loop with guard $x=p$ and resetting $x$.

∎

However, we can prove that any _closed_ L/U-PTA, i. e., with only non-strict
inequalities, is an IP-PTA. In order to show that the class of closed L/U-PTAs
is included in IP-PTAs, we need the following lemma.

######  Lemma 3.

Let $\mathcal{A}$ be a PTA with only non-strict inequalities. Let
$\mathbf{s}=(\ell,C)$ be a symbolic state of $\mathcal{A}$. Then if
$C{\downarrow_{P}}$ contains at least one integer parameter valuation, then
$C$ contains an integer point.

###### Proof.

Since there is at least one integer parameter valuation $v$ in
$C{\downarrow_{P}}$, then $v(C)$ is not empty. Since $v$ is an integer
valuation, $v(C)$ is a zone of a timed automaton with integer constants, so
the vertices of $v(C)$ are integer points. Finally, there is at least one
vertex in $v(C)$ because all clocks are nonnegative (and hence are bounded
from below by $0$), and this vertex does belong to $v(C)$ because it is
topologically closed due to the non-strict constraints. So $C$ contains at
least one integer point. ∎

######  Proposition 2.

The class of IP-PTAs is strictly larger than the class of closed L/U-PTAs.

###### Proof.

From Lemmas 2 and 3, and Proposition 1 ($\Leftarrow$). ∎

The previous result also holds for bounded PTAs:

######  Corollary 1.

The class of bounded IP-PTAs is strictly larger than the class of closed
bounded L/U-PTAs.

###### Proof.

Lemma 2 extends to bounded L/U-PTAs, since the bounds are integers (this would
not hold otherwise). Then, the proof of Proposition 1 ($\Leftarrow$) holds
with bounded IP-PTAs and closed bounded L/U-PTAs. Applying Lemma 3 concludes
the proof. ∎

######  Corollary 2.

The class of bounded IP-PTAs is incomparable with the class of bounded
L/U-PTAs. The class of bounded IP-PTAs is incomparable with the class of
L/U-PTAs.

###### Proof.

The proof of Proposition 1 can be applied with bounded PTAs on either side. ∎

##  4\. Reachability properties

In this section, we prove results for IP-PTAs. While we present one key
decidability result for this subclass (decidability of EF-emptiness), the
subsequent undecidability results can then be lifted to more general
subclasses, including general PTAs.

##### Outline

We first provide a new proof for the undecidability of the EF-emptiness
problem for general PTAs (Section 4.1). We then show that this proof can be
modified to prove the undecidability of the EF-emptiness problem for closed
bounded PTAs (Section 4.2). We then prove decidability of this problem for
bounded IP-PTAs (Section 4.3). We then prove that EF-synthesis for IP-PTAs is
intractable in practice (Section 4.4), and that the membership problem for IP-
PTAs is undecidable (Section 4.5). We finally prove the undecidability of EF-
universality for IP-PTAs (Section 4.6).

###  4.1. A new proof for the undecidability of EF-emptiness

Historically, the EF-emptiness problem has been the most studied problem of
those we have stated in Section 2.4. In the general setting of PTAs, several
undecidability proofs are available, all based on reductions from the
2-counter machines halting problem [AHV93, Mil00, Doy07, BBLS15, ALM20].

We first propose yet another such construction that will be then modified to
establish many of the results in this paper.

######  Theorem 1.

The EF-emptiness problem is undecidable for bounded PTAs.

###### Proof.

We reduce from the halting problem of a 2-counter machine (2CM), which is
undecidable [Min67].

Recall that a deterministic 2-counter machine has two non-negative counters
$C_{1}$ and $C_{2}$, a finite number of states and a finite number of
transitions, which can be of the form:

  * •

when in state $\mathtt{q}_{i}$, increment $C_{k}$ and go to $\mathtt{q}_{j}$;

  * •

when in state $\mathtt{q}_{i}$, if $C_{k}=0$ then go to $\mathtt{q}_{k}$,
otherwise go to $\mathtt{q}_{j}$.

The machine starts in state $\mathtt{q}_{0}$ with the counters set to 0; by
definition, it halts when it reaches a specific state called
$\mathtt{q}_{\textrm{halt}}$. The halting problem for such machines is
undecidable [Min67].

Given a machine $\mathcal{M}$, we encode it as a PTA
$\mathcal{A}(\mathcal{M})$. Let us describe this encoding in details, as we
will modify it in the subsequent proofs.

Each state $\mathtt{q}_{i}$ of the machine is encoded as a location of the
automaton, which we call $q_{i}$. The counters are encoded using clocks $x$,
$y$ and $z$ and one parameter $a$, with the following relations with the
values $c_{1}$ and $c_{2}$ of counters $C_{1}$ and $C_{2}$: when $x=0$, we
have $y=1-ac_{1}$ and $z=1-ac_{2}$. All three clocks are parametric, i. e.,
are compared with $a$ in some guard or invariant of the encoding. We will see
that $a$ is a rational-valued bounded parameter, typically in $[0,1]$
(although not bounding $a$ has no impact on the proof).

We initialize the clocks with the gadget in Fig. 1(a) (that also blocks the
case where $a=0$). Note that, throughout the paper, we highlight in thick
green the locations of the PTA corresponding to a state of the 2CM (in
contrast with other locations added in the encoding to maintain the matching
between the clock values and the counter values). Since all clocks are
initially 0, in Fig. 1(a) clearly, when in $q_{0}$ with $x=0$, we have
$y=z=1$, which indeed corresponds to counter values $0$.

$l_{0}$$l_{1}$$q_{0}$ $x=a\land x>0$
---
$x=1$
---
$x:=0$

(a) Initial gadget

$q_{i}$$l_{i1}$$l_{i2}$$l^{\prime}_{i2}$$l_{i3}$$q_{j}$$x=0$$\begin{array}[]{l}z=1\\\
z:=0\end{array}$$\begin{array}[]{l}y=a+1\\\
y:=0\end{array}$$\begin{array}[]{l}y=a+1\\\
y:=0\end{array}$$\begin{array}[]{l}z=1\\\
z:=0\end{array}$$\begin{array}[]{l}x=1\\\ x:=0\end{array}$

(b) Increment gadget ($C_{1}$)

$q_{i}$$l_{i1}$$l_{i2}$$l^{\prime}_{i2}$$l_{i3}$$q_{j}$$q_{k}$$x=0$$y<1$$\begin{array}[]{l}z=a+1\\\
z:=0\end{array}$$\begin{array}[]{l}y=1\\\
y:=0\end{array}$$\begin{array}[]{l}y=1\\\
y:=0\end{array}$$\begin{array}[]{l}z=a+1\\\
z:=0\end{array}$$\begin{array}[]{c}x=a+1\\\
x:=0\end{array}$$\begin{array}[]{l}x=0\\\ y=1\end{array}$

(c) 0-test and decrement gadget ($C_{1}$)

Figure 1. EF-emptiness: gadgets

We now present the gadget encoding the increment instruction of $C_{1}$ in
Fig. 1(b). The transition from $q_{i}$ to $l_{i1}$ only serves to clearly
indicate the entry in the increment gadget and is done in $0$ time unit. Since
every edge is guarded by one equality, there are really only two paths that go
through the gadget: one going through $l_{i2}$ and one through
$l^{\prime}_{i2}$. Let us begin with the former. We start from some encoding
configuration: $x=0$, $y=1-ac_{1}$ and $z=1-ac_{2}$ in $q_{i}$ (and therefore
the same in $l_{i1}$). We can enter $l_{i2}$ (after elapsing enough time) if
$1-ac_{2}\leq 1$, i. e., $ac_{2}\geq 0$, which implies that $a\geq 0$, and
when entering $l_{i2}$ we have $x=ac_{2}$, $y=1-ac_{1}+ac_{2}$ and $z=0$. Then
we can enter $l_{i3}$ if $1-ac_{1}+ac_{2}\leq 1+a$, i. e., $a(c_{1}+1)\geq
ac_{2}$. When entering $l_{i3}$, we then have $x=a(c_{1}+1)$, $y=0$ and
$z=a(c_{1}+1)-ac_{2}$. Finally, we can go to $q_{j}$ if $a(c_{1}+1)\leq 1$ and
when entering $q_{j}$ we have $x=0$, $y=1-a(c_{1}+1)$ and $z=1-ac_{2}$, as
expected.

We now examine the second path. We can enter $l^{\prime}_{i2}$ if
$1-ac_{1}\leq a+1$, i. e., $a(c_{1}+1)\geq 0$, and when entering
$l^{\prime}_{i2}$ we have $x=a(c_{1}+1)$, $y=0$ and $z=1-ac_{2}+a(c_{1}+1)$.
Then we can go to $l_{i3}$ if $1-ac_{2}+a(c_{1}+1)\leq 1+a$, i. e.,
$a(c_{1}+1)\leq ac_{2}$. When entering $l_{i3}$, we then have $x=ac_{2}$,
$y=ac_{2}-a(c_{1}+1)$ and $z=0$. Finally, we can go to $q_{j}$ if $ac_{2}\leq
1$ and when entering $q_{j}$ we have $x=0$, $y=1-a(c_{1}+1)$ and $z=1-ac_{2}$,
as expected.

Remark that exactly one path can be taken depending on the respective order of
$c_{1}+1$ and $c_{2}$, except when both are equal or $a=0$, in which cases
both paths lead to the same configuration anyway (and the case $a=0$ is
excluded by Fig. 1(a) anyway).

Decrement is done similarly by replacing guards $y=a+1$ with $y=1$, and guards
$x=1$ and $z=1$ with $x=a+1$ and $z=a+1$, respectively, as shown in Fig. 1(c).
In addition, the 0-test is obtained by simply adding a transition from $q_{i}$
to $q_{k}$ with guard $y=1\land x=0$, which ensures that $C_{1}=0$. Similarly,
the guard from $q_{i}$ to $l_{i1}$ ensures that decrement is done only when
the counter is not null.

All those gadgets also work for $C_{2}$ by swapping $y$ and $z$.

The actions associated with the transitions do not matter; we can assume a
single action $\sigma$ on all transitions (omitted in all figures).

We now prove that the machine halts iff there exists a parameter valuation $v$
such that $v(\mathcal{A})$ reaches location $q_{\mathtt{halt}}$. First note
that if $a=0$ the initial gadget cannot be passed, and so the machine does not
halt. Assume $a>0$. Consider two cases:

  1. (1)

either the value of the counters is not bounded. Then, for any parameter
valuation, at some point during an incrementation of, say, $C_{1}$ we will
have $a(c_{1}+1)>1$ when taking the transition from $l_{i2}$ to $l_{i3}$ and
the PTA will be blocked. Therefore, there exists no parameter valuation for
which the PTA can reach $q_{\mathtt{halt}}$.

  2. (2)

or the value of the counters remains bounded. Let $c$ be their maximal value.
Let us consider two subcases:

    1. (a)

either the machine reaches $\mathtt{q}_{\textrm{halt}}$: in that case, if
$c=0$ and $0<a\leq 1$ or $c>0$ and $ca<1$, then the PTA valuated with such
parameter valuations correctly simulates the machine, yielding a (unique) run
reaching location $q_{\mathtt{halt}}$. The set of such valuations for $a$ is
certainly non-empty: $a=\frac{1}{2}$ belongs to it if $c=0$ and
$a=\frac{1}{c}$ does otherwise.

    2. (b)

or the machine does not halt. Then again, for a sufficiently small parameter
valuation (i. e., $a<1$ if $c=0$ and $a\leq\frac{1}{c}$ otherwise), the
machine is properly simulated, and since the machine does not halt, then the
PTA never reaches $q_{\mathtt{halt}}$. For other values of $a$, the machine
will block at some point in an increment gadget, because $a$ is not small
enough and the guard to $q_{j}$ cannot be satisfied.

Hence the machine halts iff there exists a parameter valuation $v$ such that
$v(\mathcal{A})$ reaches $q_{\mathtt{halt}}$. ∎

######  Remark 1.

In this paper, we allow guards and invariants of the form $x\bowtie\sum_{1\leq
j\leq M}\beta_{j}p_{j}+d$, which is more restrictive than [BLT09] (that allows
parametric coefficients different from 0 and 1, as well as diagonal
constraints), but more permissive than [AHV93], that only allows a syntax
$x\bowtie p$. In fact, most papers in the literature define their own syntax
(see [And19] for a survey). We can adapt our proof to fit in the most
restrictive syntax ($x\bowtie p$) as follows: transitions with $y=a+1$ guards
and $y:=0$ reset can be equivalently replaced by one transition with a “$y=1$”
guard and a reset of some additional clock $w$, followed by a transition with
a $w=a$ guard and the $y:=0$ reset (and similarly for $x$ and $z$ is the
decrement gadget). This also allows the proof to work without complex
parametric expressions in guards, using three additional clocks (we conjecture
that a smarter encoding can be exhibited to factor these additional clocks, so
as to use a single additional clock). A similar modification can be applied to
all subsequent undecidability proofs.

###  4.2. Undecidability for closed bounded PTAs

Now, by reusing the previous proof, we can show that the EF-emptiness problem
is undecidable for closed bounded PTAs. This is an original result, as all
existing results with bounded PTAs (e. g., [Mil00, Doy07, ALM20]) require (at
least some) strict inequalities. This result can also be seen as a complement
to [Doy07], that proves the same result by using _only_ strict inequalities.

######  Theorem 2.

The EF-emptiness problem is undecidable for closed bounded PTAs.

###### Proof.

First, recall that the (unique) parameter $a$ in the proof of Theorem 1 can be
bounded by $[0,1]$, hence the PTA in the proof of Theorem 1 is a bounded PTA.

The encoding of the instructions of the 2-counter-machine used in the proof of
Theorem 1 is almost a closed PTA, as mostly non-strict inequalities are used,
with two exceptions:

  1. (1)

the initial gadget (Fig. 1(a)) requires a strict inequality to ensure $a>0$;

  2. (2)

the 0-test and decrement gadget (Fig. 1(c)) uses an inequality $y<1$ to ensure
the counter is not 0.

We will remove these strict inequalities as follows:

  1. (1)

we remove the guard between $\ell_{0}$ and $\ell_{1}$ in the initial gadget
(Fig. 1(a)), that is we allow (so far) the valuation $a=0$ that does not
correctly simulate the machine;

  2. (2)

we remove the strict inequality $y<1$ in the decrement gadget (Fig. 1(c)) as
follows. Instead of testing $y<1$ when $x=0$, it is equivalent to test $x>0$
when $y=1$ on the subsequent transitions. And testing $x>0$ is equivalent to
testing $x\geq a$ provided $a>0$ (we will take care of this later on). The new
gadget is given in Fig. 2(a) and, provided $a>0$, it is equivalent to the
former gadget in Fig. 1(c).

Now, with these new gadgets, the behavior of the encoding is the same as in
the proof of Theorem 1, provided $a>0$. Removing $a=0$ is necessary, as this
valuation does not correctly encode the machine. We will therefore forbid
$a=0$ in a new final gadget, given in Fig. 2(b), with a transition from
$q_{\mathtt{halt}}$ to a new location $q^{\prime}_{\mathtt{halt}}$ (via an
intermediate location). This gadget allows us to ensure $a>0$, without using
strict inequalities; we believe this is the cornerstone of this proof of
Theorem 2.

$q_{i}$$l_{i1}$$l_{i2}$$l^{\prime}_{i2}$$l_{i3}$$q_{j}$$q_{k}$$x=0$$\begin{array}[]{l}z=a+1\\\
z:=0\end{array}$$\begin{array}[]{l}y=1\\\ x\geq a\\\
y:=0\end{array}$$\begin{array}[]{l}y=1\\\ x\geq a\\\
y:=0\end{array}$$\begin{array}[]{l}z=a+1\\\
z:=0\end{array}$$\begin{array}[]{c}x=a+1\\\
x:=0\end{array}$$\begin{array}[]{l}x=0\\\ y=1\end{array}$

(a) 0-test and decrement gadget ($C_{1}$)

$q_{\mathtt{halt}}$$q_{\mathtt{halt}}^{1}$$q^{\prime}_{\mathtt{halt}}$
$x,y:=0$
---
$x=a$
---
$x:=0$
$x=0\land y\geq 1$
---

(b) Last transition of the 2CM encoding with non-strict inequalities

Figure 2. Rewriting gadgets for EF-emptiness for closed bounded PTAs

Clearly, if $a=0$, taking the self-loop on $q_{\mathtt{halt}}^{1}$ will not
allow time to elapse; and then there will be no way to leave
$q_{\mathtt{halt}}^{1}$ with $x=0$ and $y\geq 1$; hence
$q^{\prime}_{\mathtt{halt}}$ is not reachable for $a=0$. In contrast, if
$0<a\leq 1$, since $a$ is a rational number, then by taking an appropriate
number of times the self-loop on $q_{\mathtt{halt}}^{1}$, we will eventually
have $x=0$, just after the last loop, and $y\geq 1$; hence
$q^{\prime}_{\mathtt{halt}}$ will eventually be reached. To summarize:

  * •

if $a=0$, the machine is not correctly encoded, but there is no way to reach
$q^{\prime}_{\mathtt{halt}}$;

  * •

if $0<a\leq 1$, the machine is correctly encoded, and from Theorem 1 we know
that $q_{\mathtt{halt}}$ is reachable iff the machine halts. Since
$q^{\prime}_{\mathtt{halt}}$ is reachable from $q_{\mathtt{halt}}$, then
$q^{\prime}_{\mathtt{halt}}$ is reachable iff the machine halts.

Hence there exists a parameter valuation such that
$q^{\prime}_{\mathtt{halt}}$ is reachable iff the machine halts. Finally, note
that all our gadgets use non-strict inequalities, and therefore the built PTA
is a closed bounded PTA. ∎

###  4.3. A decidability result for bounded IP-PTAs

Our main positive result in this section is that the EF-emptiness problem is
decidable for bounded IP-PTAs.

######  Theorem 3.

The EF-emptiness problem is decidable (and PSPACE-complete) for bounded IP-
PTAs.

###### Proof.

We first need to recall two lemmas relating symbolic and concrete runs (proved
in [HRSV02, ACEF09]).

Given a concrete (respectively symbolic) run
$(\ell_{0},\vec{0})\stackrel{{\scriptstyle
e_{0}}}{{\mapsto}}(\ell_{1},w_{1})\stackrel{{\scriptstyle
e_{1}}}{{\mapsto}}\cdots\stackrel{{\scriptstyle
e_{m-1}}}{{\mapsto}}(\ell_{m},w_{m})$ (respectively
$(\ell_{0},C_{0})\stackrel{{\scriptstyle
e_{0}}}{{\Rightarrow}}(\ell_{1},C_{1})\stackrel{{\scriptstyle
e_{1}}}{{\Rightarrow}}\cdots\stackrel{{\scriptstyle
e_{m-1}}}{{\Rightarrow}}(\ell_{m},C_{m})$), we define the corresponding
discrete sequence as $\ell_{0}\stackrel{{\scriptstyle
e_{0}}}{{\Rightarrow}}\ell_{1}\stackrel{{\scriptstyle
e_{1}}}{{\Rightarrow}}\cdots\stackrel{{\scriptstyle
e_{m-1}}}{{\Rightarrow}}\ell_{m}$. Two runs (concrete or symbolic) are said to
be equivalent if their associated discrete sequences are equal.

######  Lemma 4.

Let $\mathcal{A}$ be a PTA, and $v$ be a parameter valuation. Let $\rho$ be a
run of $\mathcal{A}$ reaching a symbolic state $(\ell,C)$. Then, there exists
an equivalent run in the TA $v(\mathcal{A})$ reaching a concrete state
$(\ell,w)$ (for some $w$) iff $v\models C{\downarrow_{P}}$.

######  Lemma 5.

Let $\mathcal{A}$ be a PTA, and $v$ be a parameter valuation. Let $\rho$ be a
run of the TA $v(\mathcal{A})$ reaching a concrete state $(\ell,w)$. Then
there exists an equivalent run in $\mathcal{A}$ reaching a symbolic state
$(\ell,C)$, for some $C$ such that $v\models C{\downarrow_{P}}$.

Let $\mathcal{A}$ be a bounded IP-PTA. EF-emptiness is false for $\mathcal{A}$
iff there exists a valuation $v$ such that a run of $v(\mathcal{A})$ reaches a
location in some predefined set $T$. Assume there exists a valuation $v$ such
that a run of $v(\mathcal{A})$ reaches $\ell$, with $\ell\in T$. From Lemma 5,
there exists a symbolic run of $\mathcal{A}$ reaching a symbolic state
$(\ell,C)$, for some $C$. Since $\mathcal{A}$ is an IP-PTA, $C$ contains at
least one integer point. Hence there exists an integer parameter valuation
$v^{\prime}\models C{\downarrow_{P}}$; hence from Lemma 4, there exists a
concrete run of $v^{\prime}(\mathcal{A})$ reaching $\ell$. This gives that EF-
emptiness is false for $\mathcal{A}$ iff there exists an integer valuation
$v^{\prime}$ such that a run of $v^{\prime}(\mathcal{A})$ reaches a location
in $T$.

Hence, deciding whether some valuation permits to reach $\ell$ reduces to
deciding whether some _integer_ valuation permits to do so, which, for bounded
PTAs, is PSPACE-complete [JLR15]. ∎

Since bounded IP-PTAs are incomparable with L/U-PTAs (for which the EF-
emptiness problem is known to be decidable), and since L/U-PTAs are the only
non-trivial subclass of PTAs for which this problem is known to be decidable,
then Theorem 3 strictly extends the subclass of PTAs for which this problem is
decidable.

In practice, [JLR15] proposes efficient symbolic algorithms to synthesize all
the integer parameter valuations that permit to reach some given location, and
thus to solve EF-emptiness for IP-PTAs.

###  4.4. Intractability of the synthesis

Although the EF-emptiness problem is decidable for L/U-PTAs [HRSV02], the
synthesis seems to pose practical problems: it was shown in [JLR15] that the
solution to the EF-synthesis problem for L/U-automata, if it can be computed,
cannot be represented using any formalism for which emptiness of the
intersection with equality constraints is decidable. In particular, this rules
out the possibility of computing the solution set as a finite union of
polyhedra.

We reuse the intuition of this result and extend it to closed bounded
L/U-PTAs.

######  Theorem 4.

If it can be computed, the solution to the EF-synthesis problem for closed
bounded L/U-automata cannot be represented using any formalism for which
emptiness of the intersection with equality constraints is decidable.

###### Proof.

We reuse the idea of [BLT09] used for proving that constrained emptiness for
infinite runs acceptance properties is undecidable, and reused in [JLR15,
Theorem 2]. Suppose that the solution to the EF-synthesis problem for closed
bounded L/U-PTAs can be represented using a formalism for which emptiness of
the intersection with equality constraints is decidable. Assume a closed
bounded PTA $\mathcal{A}$; for each parameter $p_{i}$ of $\mathcal{A}$ that is
used both as an upper bound and a lower bound, replace its occurrences as
upper bounds by a fresh parameter $p_{i}^{u}$ and its occurrences as lower
bounds by a fresh parameter $p_{i}^{l}$. We therefore obtain a closed bounded
L/U-PTA. Assume we can derive a solution to the EF-synthesis problem for this
closed bounded L/U-PTA, and let $K$ be that solution. Then, by hypothesis, we
can decide whether $K\land\bigwedge_{i}p_{i}^{l}=p_{i}^{u}$ is empty or not;
hence, we can solve the EF-emptiness for $\mathcal{A}$, which contradicts the
undecidability of EF-emptiness for closed bounded PTAs (from Theorem 2). ∎

######  Corollary 3.

If it can be computed, the solution to the EF-synthesis problem for IP-PTAs
cannot be represented using any formalism for which emptiness of the
intersection with equality constraints is decidable.

###### Proof.

From the fact that a closed bounded L/U-PTA is an IP-PTA (Corollary 1). ∎

###  4.5. Membership

We first show that it cannot be decided in general whether a PTA is a
(bounded) IP-PTA.

######  Theorem 5 (undecidability of membership).

It is undecidable whether a PTA is an IP-PTA, even when bounded.

###### Proof.

Let us consider again the PTA $\mathcal{A}(\mathcal{M})$ encoding the
2-counter machine $\mathcal{M}$ proposed in our proof of Theorem 2. We make
the following modification to the final gadget (Fig. 2(b)): we forbid $a=1$ in
the final location $q^{\prime}_{\mathtt{halt}}$, by adding $y>a$ on the final
transition to $q^{\prime}_{\mathtt{halt}}$.

The PTA $\mathcal{A}(\mathcal{M})$ has only one parameter $a$ and all the
symbolic states of $\mathcal{A}(\mathcal{M})$ contain the integer value $a=0$
except the states corresponding to location $q^{\prime}_{\mathtt{halt}}$.
Since all constraints are non-strict (except on the final transition to
$q^{\prime}_{\mathtt{halt}}$), all reachable symbolic states except those
associated with $q^{\prime}_{\mathtt{halt}}$ contain an integer point from
Lemma 3. Conversely, since $q^{\prime}_{\mathtt{halt}}$ can only be reached
provided $0<a<1$, then the reachable symbolic states associated with
$q^{\prime}_{\mathtt{halt}}$ contain _no_ integer point.

Then the PTA ${\mathcal{A}}({\mathcal{M}})$ reaches the location
$q^{\prime}_{\mathtt{halt}}$ if and only if ${\mathcal{A}}({\mathcal{M}})$ is
not an IP-PTA. As a consequence, this PTA is an IP-PTA iff the 2-counter
machine does not halt. Finally, note that this PTA can be bounded by imposing
$0\leq a\leq 1$, without any change in the reasoning above. ∎

Nevertheless, Proposition 2 provides a sufficient syntactic membership
condition, since any closed L/U-PTA is an IP-PTA. In addition, we now define
another new non-trivial set of restrictions leading to IP-PTAs:

######  Definition 6 (Reset-PTA).

A _reset-PTA_ is a PTA where:

  * •

all guards and invariants are conjunctions of constraints of the form $x\leq
p+k$, $x\geq p+k$, $x\leq k$, or $x\geq k$, with $x$ a clock, $p$ a parameter,
and $k$ an integer;

  * •

and all clocks are reset to 0 on any transition with a guard or a source
location invariant in which a parameter appears.

This kind of restriction is somewhat reminiscent of those enforced by
_initialized_ hybrid automata [HKPV98] to obtain decidability. We now prove
that reset-PTAs are IP-PTAs, which in turn means that the EF-emptiness problem
is decidable for bounded reset-PTAs. It is worth noting that, to the best our
knowledge, bounded reset-PTAs and L/U-PTAs are the only non-trivial sets of
syntactic restrictions of PTAs making the reachability emptiness problem
decidable.

######  Theorem 6.

Any reset-PTA is an IP-PTA.

###### Proof.

We prove by induction that the symbolic states generated by reset-PTAs are
zones with only non-strict constraints over the set of variables defined by
the union of clocks and parameters. To simplify the proof a bit we omit
invariants but including them would raise no theoretical difficulty. We then
additionally prove as part of the induction that there is no inequality
involving two variables $x$ and $y$ in which $x$ and $y$ would not be of the
same type (clock or parameter).

The property clearly holds for the initial symbolic state: parameters are
unconstrained, all clocks are equal and their common value is greater than or
equal to $0$.

Now suppose this holds for some symbolic state and consider the successor of
that symbolic state by some transition. Recall from the $\mathsf{Succ}$
definition in Section 2.2.3 that this successor is computed by the following
operations: intersection with the guard of the transition, reset of the clocks
designated in the reset set of the transition, and finally time elapsing.

Due to the restriction on constraints, all guards are themselves zones, and it
is well-known that the intersection of two zones is again a zone. Similarly,
the reset operation on some of the variables of a zone again leads to a zone.
The time elapsing of a proper subset of the variables in a zone however is not
a zone in general (the same situation arises, e. g., in stopwatch automata).
We therefore need to examine more closely the zone on which the time elapsing
operates. Two cases arise:

  1. (1)

the guard did not involve any parameter. Then, with the induction hypothesis,
we still do not have any constraint between clocks and parameters after the
intersection with the guard. A fortiori, we do not have any after the resets
either. The time elapsing operation can be carried out by introducing a fresh
non-negative variable $t$, performing variable substitutions $x\leftarrow x+t$
for each clock $x$, and finally eliminating $t$. This elimination can be done
with the Fourier-Motzkin procedure (see e. g., [Sch86]) which produces all the
constraints not involving $t$ plus those obtained by writing all the
combinations of a minorant of $t$ less or equal to a majorant of $t$. After
the variable substitutions, $t$ does not appear in constraints between
parameters, nor in diagonal clock constraints ($x-y\leq k$ gives
$(x+t)-(y+t)\leq k$, i. e., again $x-y\leq k$). Since there is no constraint
between clocks and parameters, $t$ only appears in rectangular constraints
that become of the form $y+t\leq k_{1}$ or $x+t\geq k_{2}$. Through the
elimination procedure this gives constraints of the form $x-y\leq
k_{2}-k_{1}$, and the expected result holds.

  2. (2)

the guard involves some parameters. Then before the reset we do have
constraints between clocks and parameters. But then, from the definition of
reset-PTAs, all clocks are reset along this transition, so these constraints
are removed (as part of the elimination of clock variables) and replaced by
constraints restricting the reintroduced clock variables to zero. Then, after
the reset we do not have constraints between clocks and parameters anymore and
the previous reasoning is again valid.

We conclude the proof by noting that in any non-empty zone with integer
coefficients all vertices are integer (see the discussion in [JLR15]). And
following the proof of Lemma 3, since all variables are non-negative, there is
at least one such vertex, which does belong to the zone because all
constraints are non-strict. This zone therefore contains at least an integer
point. ∎

Recall that the synthesis is intractable for bounded IP-PTAs (from Corollary
3) and for bounded L/U-PTAs. In contrast, and although studying reset-PTAs in
detail goes beyond the scope of this work, we showed in [ALR19] that exact
synthesis can be computed for bounded reset-PTAs as defined here, even when
resets are done to (rational-valued) parameters.

###  4.6. Undecidability of EF-Universality

We show below that, unlike L/U-PTAs, the EF-universality problem is
undecidable for IP-PTAs even bounded. This result differentiates the classes
of (bounded) L/U-PTAs and bounded IP-PTAs, and helps to understand better the
boundary between decidability and undecidability for subclasses of PTAs.

######  Theorem 7.

The EF-universality problem is undecidable for bounded IP-PTAs with 3
parametric clocks and 2 rational-valued parameters.

###### Proof.

We start from the encoding in our proofs of Theorems 1 and 2. The main idea
is, for all valuations of the parameter $a$ that are not small enough to
properly encode the counters (i. e., for some value $c$ of a counter,
$1-ac<0$), to allow the PTA to directly go to a $q_{\mathtt{error}}$ location.
In order for our encoding to be an IP-PTA (in particular the symbolic states
with location $q_{\mathtt{error}}$), we add a new parameter $b$, the value of
which can be typically in $[0,1]$.

We then reduce the problem of knowing whether the counters of the machine grow
unbounded along its execution, which is undecidable [Min67], to the
universality of the set of parameters that allow the encoding PTA to reach
$q_{\mathtt{error}}$.

Let us summarize our construction before going into details.

  1. (1)

We reuse the increment gadget from Theorems 1 and 2 (Fig. 1(b)) and extend it
with a new location $q_{\mathtt{error}}$ (details will follow);

  2. (2)

We reuse the 0-test and decrement gadget from Theorem 2 (Fig. 2(a)) as it is;

  3. (3)

We do not use the final gadget from $q_{\mathtt{halt}}$ to
$q^{\prime}_{\mathtt{halt}}$ (Fig. 2(b)), i. e., the last location is
$q_{\mathtt{halt}}$. (Recall that our target location is $q_{\mathtt{error}}$
anyway.)

Let us now go into details. First, we add a fresh location
$q_{\mathtt{error}}$ to our PTA encoding, and we add two transitions from
$l_{0}$ (the initial location of the PTA) to the $q_{\mathtt{error}}$
location:

  * •

one with guard $x=0\land x=a$, that can only be taken when $a=0$ and serves to
“eliminate” this special case that does not correctly encode the counters.

  * •

and one with guard $0\leq x<1\land x=b$, that can only be taken when
$b\in[0,1)$.222This case may not be necessary in the proof; however, it makes
the explanation simpler, as we can now discard from our reasoning valuations
such that $b\in[0,1)$.

So, whenever $a=0$ and $b\in[0,1)$, the system can eventually reach
$q_{\mathtt{error}}$. Hence, in the following, we only need to focus on the
case where $a\in(0,1]$ and $b=1$.

Let us now change the increment gadget of Fig. 1(b) (when decrementing, there
is no upper bound constraint on $a$). More specifically, remark that, when
incrementing $C_{1}$, the constraint that implies $a\leq\frac{1}{c_{1}+1}$
comes from the last transition in the path going through $l_{i2}$. In the
other path, $c_{2}$ is already greater than or equal to $c_{1}+1$ and
therefore $a$ is already small enough to properly encode $c_{1}+1$ since it is
small enough to encode $c_{2}$. Our modified increment gadget is given in Fig.
3.

$q_{i}$$l_{i1}$$l_{i2}$$l^{\prime}_{i2}$$q_{\mathtt{error}}$$l_{i3}$$q_{j}$$x=0$$\begin{array}[]{l}z=1,\\\
z:=0\end{array}$$\begin{array}[]{l}y=a+1,\\\
y:=0\end{array}$$\begin{array}[]{l}y=a+1\land x\leq 1,\\\
y:=0\end{array}$$\begin{array}[]{l}y=a+1\land x\geq b,\\\
y:=0\end{array}$$\begin{array}[]{l}z=1,\\\
z:=0\end{array}$$\begin{array}[]{l}x=1,\\\ x:=0\end{array}$

Figure 3. EF-universality for bounded IP-PTAs: increment gadget

In the transition from $l_{i2}$ to $l_{i3}$, if $a$ is not small enough then
$x=a(c_{1}+1)$ will be greater than one and the final transition to $q_{j}$
will not be fireable. We therefore add a direct transition from $l_{i2}$ to
$q_{\mathtt{error}}{}$ when $x\geq b$. Recall that we only care about the case
where $b=1$, hence this transition can be understood as $x\geq 1$; now the
case where $x=1$ is problematic, as the value of $a$ is just small enough to
encode the counters, and we still can reach $q_{\mathtt{error}}$, and the
2-counter machine is not properly encoded. However, since we are interested in
universality, it suffices to take a valuation of $a$ slightly smaller to
properly encode the machine, as we explain more precisely below.

We now prove that the counters of the machine grow unbounded along its
execution iff for all values of $a$ and $b$, the encoding PTA can reach
$q_{\mathtt{error}}$. First recall that for $a=0$ or $b\in[0,1)$, it is always
possible to reach $q_{\mathtt{error}}$ (from the initial state). When $a>0$
and $b=1$, we have two cases:

  * •

either the counters grow unbounded (say $C_{1}$ does), then whatever the value
of $a>0$, at some point we have $ac_{1}>1$. More specifically, there is an
incrementation of $C_{1}$ such that $ac_{1}\leq 1$ and $a(c_{1}+1)>1$, which
also implies $a(c_{1}+1)\geq b$ (since $b=1$). Then, when executing the
corresponding increment gadget, $q_{\mathtt{error}}$ can be reached from
$l_{i2}$;

  * •

or the counters stay bounded. Let $c$ be the maximal value of the counters.
Recall that when entering $l_{i2}$ we have $x=ac_{2}$, $y=1-ac_{1}+ac_{2}$ and
$z=0$. Then, when $y=a+1$, we have $x=a(c_{1}+1)$. If $c_{1}+1=c$, then $x=ca$
is the largest value that $x$ can have in $l_{i2}$ when $y=a+1$. Observe that,
due to the non-strict inequality $x\geq b$ in the guard from $l_{i2}$ to
$q_{\mathtt{error}}$, one might still reach $q_{\mathtt{error}}$ for a
valuation of $a$ such that $ca=1$. Consequently, consider the parameter
valuation $a=\frac{1}{c+1}$ and $b=1$. Then $ca<1=b$ and since $x$ is in
$l_{i2}$ always at most equal to $ca$ when $y=a+1$, the guard to
$q_{\mathtt{error}}{}$ is never true and the of valuations for which the
automaton can reach $q_{\mathtt{error}}$ is not universal.

It remains to show that the constructed PTA is an IP-PTA. With the exception
of $q_{\mathtt{error}}$, the result is clear: $a=0$ and $b=0$ belongs to every
reachable symbolic state, hence each symbolic state contains an integer
parameter valuation, and hence from Lemma 3, all symbolic states (except those
with location $q_{\mathtt{error}}$) contain at least one integer point. In
addition, the two symbolic states taken by taking the two special transitions
from the initial state to $q_{\mathtt{error}}$ to handle $a=0$ or $b\in[0,1)$
also contain the integer point $x=y=a=b=0$. Now, let us consider the other
symbolic states with location $q_{\mathtt{error}}$ (and reachable from some
location $l_{i2}$ due to an increment). The projection onto the parameters of
the associated constraint is $0\leq b\leq 1\land\frac{b}{i+1}\leq
a\leq\frac{1}{i}$, with $i\in{\mathbb{N}}$ denotes the current maximum
valuation of the counter. Clearly, $a=b=0$ is a parametric integer point in
this symbolic state; hence from Lemma 3 this symbolic state contains an
integer point (in clocks and parameters dimensions). Hence this PTA is a
(bounded) IP-PTA. ∎

######  Corollary 4.

The EF-universality problem is undecidable for IP-PTAs, for bounded PTAs, and
for PTAs.

###### Proof.

From Theorem 7 and from the fact that a bounded IP-PTA is an IP-PTA, is a
bounded PTA, and is a PTA. ∎

We now show that, in contrast to _bounded_ IP-PTAs, the EF-emptiness problem
is undecidable for (unbounded) IP-PTAs. This result emphasizes the fact that
the boundedness of IP-PTAs is crucial to ensure decidability.

######  Theorem 8.

The EF-emptiness problem is undecidable for IP-PTAs.

###### Proof.

The proof of the undecidability of the EF-emptiness problem for general PTAs
in [AHV93] can be interpreted over integer parameter valuations. Any symbolic
state contains at least one integer parameter valuation (the one that is large
enough to correctly encode the value of the two counters), as well as all
larger parameter valuations. Furthermore, since the proof only uses non-strict
inequalities (in fact only equalities), from Lemma 3, all symbolic states
contain at least one integer point. Hence the PTA used in [AHV93] to encode
the 2-counter machine is an IP-PTA. ∎

Finally, we show below (without surprise) that the EF-emptiness problem (shown
to be decidable for L/U-PTAs [HRSV02]) and the EF-universality problem (shown
to be decidable for integer-valued L/U-PTAs [BLT09]) are also decidable for
bounded L/U-PTAs.

######  Theorem 9.

The EF-emptiness and EF-universality problems are decidable for bounded
L/U-PTAs.

###### Proof.

In [HRSV02, BLT09], it is shown that decreasing a lower-bound parameter
$p_{i}^{-}$ or increasing an upper-bound parameter $p_{j}^{+}$ in an L/U-PTA
$\mathcal{A}$ can only add behaviors. Hence, deciding EF-emptiness can be done
by testing the reachability of the location in the TA obtained from
$\mathcal{A}$ by instantiating all $p_{i}^{-}$s with $0$ and all $p_{j}^{+}$s
with $\infty$. (Recall that testing the reachability of a location in a TA is
decidable [AD94].) For a bounded L/U-PTA, this can be done in a similar
manner, by testing the reachability of the location in the TA obtained from
$\mathcal{A}$ by instantiating all $p_{i}^{-}$s with their minimal value and
all $p_{j}^{+}$s with their maximal value in the (closed) bounded parameter
domain.

EF-universality can be solved similarly, except that $p_{i}^{-}$s are replaced
with their upper bound and $p_{j}^{+}$s are replaced with their lower bound. ∎

##  5\. Liveness properties

In this section, we consider liveness properties. More specifically, we
consider the problems of the emptiness of the parameter valuations set for
which all runs eventually reach a given location (Section 5.1), for which
there exists an infinite run (Section 5.2), for which there exists a deadlock
(Section 5.3), and for which a run remains in a given set of locations
(Section 5.4).

###  5.1. Undecidability of AF-emptiness

It is known that AF-emptiness is undecidable for L/U-PTAs [JLR15]; reusing the
encoding of the 2-counter machine proposed in our proof of Theorem 1, we now
show that this result holds even for bounded L/U-PTAs.

######  Theorem 10.

The AF-emptiness problem is undecidable for bounded L/U-PTAs with 3 clocks and
2 rational-valued parameters.

###### Proof.

Let us consider the PTA $\mathcal{A}(\mathcal{M})$ encoding the 2-counter
machine $\mathcal{M}$ proposed in our proof of Theorem 2. The PTA
$\mathcal{A}(\mathcal{M})$ has only one parameter $a$ which is used both as an
upper bound and a lower bound. In our modified encoding, we replace $a$ with
two fresh parameters $a^{-}$ and $a^{+}$. Then, in both the increment gadget
(Fig. 1(b)) and the 0-test and decrement gadget (Fig. 2(a)), we replace the
guard $y=1+a$ by a guard $1+a^{-}\leq y$ and an invariant $y\leq 1+a^{+}$; we
do the same for the guard $z=1+a$. We give the modified increment gadget in
Fig. 4(b).

$l_{0}$$y\leq a^{+}$$l_{1}$$y\leq a^{+}$$q_{0}$$x\leq 0$$\ell_{\mathtt{sink}}$
$y\geq a^{-}$
---
$x:=0$
$y:=0$
---
$a^{-}\leq x\leq 0$
---

(a) Initial gadget

$q_{i}$$l_{i1}$$l_{i2}$$l^{\prime}_{i2}$$l_{i3}$$q_{j}$$\begin{array}[]{l}z\leq
1\wedge\\\ y\leq a^{+}+1\end{array}$$y\leq a^{+}+1$$x\leq 1$$z\leq
1$$x=0$$\begin{array}[]{l}z=1,\\\
z:=0\end{array}$$\begin{array}[]{l}a^{-}+1\leq y,\\\
y:=0\end{array}$$\begin{array}[]{l}a^{-}+1\leq y,\\\
y:=0\end{array}$$\begin{array}[]{l}z=1,\\\
z:=0\end{array}$$\begin{array}[]{l}x=1,\\\ x:=0\end{array}$

(b) Increment gadget

Figure 4. AF-emptiness for bounded L/U-PTAs

We initialize the parameters $a^{-}$ and $a^{+}$ with the gadget in Fig. 4(a)
(adapted from [JLR15]) leading to the location $q_{0}$. Clearly, starting from
$l_{0}$, we have ${\sf AF}(q_{0})$ if and only if $a^{-}=a^{+}>0$, because

  1. (1)

if $a^{-}=0$ then it is possible to reach $\ell_{\mathtt{sink}}$ and therefore
we do not have ${\sf AF}(q_{0})$, and

  2. (2)

any run that reaches $l_{1}$ before $y$ is equal to $a^{+}$ can be extended by
delaying a non-null amount of time into a run that will be blocked by the
invariant of $q_{0}$.

So all runs should enter $l_{1}$ with $y=a^{+}$, which is the case if and only
if $a^{-}=a^{+}$. We therefore obtain an L/U-automaton with $a^{-}=a^{+}$ and
$a^{+}>0$.

Let us now go back to the increment gadget of Fig. 4(b). As in the proof of
Theorem 2, when $a^{-}=a^{+}>0$, exactly one path can be taken depending on
the respective order of $c_{1}+1$ and $c_{2}$. The invariants allow to avoid
infinite delays in locations and since $a^{-}=a^{+}$, no run can be blocked
inside the gadget. The same reasoning can be made for the decrement and zero-
testing gadgets. Moreover we can bound the PTA by $a^{-},a^{+}\in[0,1]$
without loss of behavior.

Hence we reduce the halting problem of 2-counter machine to the AF-emptiness
problem for bounded L/U-PTAs: the machine halts iff there exists a value of
$a^{-}=a^{+}>0$, such that the location $q_{\mathtt{halt}}{}$ is unavoidable
in our bounded L/U-automaton. ∎

######  Corollary 5.

The AF-emptiness problem is undecidable for bounded IP-PTAs, for IP-PTAs and
for bounded PTAs.

###### Proof.

The AF-emptiness problem is undecidable for bounded L/U-PTAs (Theorem 10),
which immediately gives the undecidability for bounded PTAs.

Furthermore, the PTA used in the proof of Theorem 10 only uses non-strict
inequalities; furthermore, $a^{-}=0$ and $a^{+}=1$ is a parameter valuation
solution of any symbolic state. Hence, from Lemma 3, this PTA is a bounded IP-
PTA, which gives the result for bounded IP-PTAs. As a consequence, the result
also holds for general IP-PTAs. ∎

###  5.2. Cycle-Existence-Emptiness

######  Theorem 11.

The cycle-existence-emptiness problem is decidable for closed bounded
L/U-PTAs.

###### Proof.

Recall that, thanks to the monotonicity property of L/U-PTAs (recalled in
Lemma 1), any run possible for a valuation $v$ of the parameters is also
possible for any valuation of the parameters for which the upper-bound (resp.
lower-bound) parameters are larger (resp. smaller) than or equal to that of
$v$.

Let $\mathcal{A}_{|\mathit{bounds}}$ be a closed bounded L/U-PTA. Let
$v_{\mathrm{inf}/\mathrm{sup}}$ be the valuation such that, for each lower-
bound parameter $p^{-}$,
$v_{\mathrm{inf}/\mathrm{sup}}(p^{-})=\mathrm{inf}(p^{-},\mathit{bounds})$
and, for each upper-bound parameter $p^{+}$,
$v_{\mathrm{inf}/\mathrm{sup}}(p^{+})=\mathrm{sup}(p^{+},\mathit{bounds})$.

  1. (1)

If $v_{\mathrm{inf}/\mathrm{sup}}(\mathcal{A})$ contains an infinite run
(which can be checked in PSPACE [AD94], and can be performed efficiently in
practice using, e. g., the zone graph [BY03]), then since
$\mathcal{A}_{|\mathit{bounds}}$ is closed, $v_{\mathrm{inf}/\mathrm{sup}}$
belongs to $\mathit{bounds}$, and hence the set of parameter valuations that
yield an infinite run is not empty.

  2. (2)

On the contrary, if $v_{\mathrm{inf}/\mathrm{sup}}(\mathcal{A})$ contains no
infinite run, then from the monotonicity property of L/U-PTAs (Lemma 1), no
other valuation in $\mathit{bounds}$ gives a TA with an infinite run, as such
a TA could only contain less runs. Hence the set of parameter valuations that
yield an infinite run is empty.

∎

$\ell_{0}$ | $0<x<1$
---|---
$\land$ | $x=p$

(a)

$\ell_{0}$$y\leq p$$\ell_{1}$ $x=1$
---
$x:=0$
$x=0\land y\leq p$
---

(b)

$\ell_{0}$ $x=1\wedge y\leq p$
---
$x:=0$

(c)

$\ell_{0}$ $x\geq p\wedge y\leq 1$
---
$x:=0$

(d)

Figure 5. Examples of PTA (a) and L/U-PTAs (b–d)

The above result cannot be used as such for non-bounded L/U-PTAs as a cycle
that exists for an infinite parameter valuation may not exist for any finite
parameter valuation: consider the L/U-PTA in Fig. 5(b). This L/U-PTA has an
infinite run for $p=\infty$, but for any parameter valuation (i. e., different
from $\infty$), the number of self-loops in $\ell_{0}$ is bounded by $p$, and
hence finite. However, extending to rational-valued parameters a result from
[BLT09], we can still prove decidability.

######  Lemma 6.

Given an L/U-PTA $\mathcal{A}$ and a subset of its locations $T$, the problem
of the existence of at least one parameter valuation $v$ such that
$v(\mathcal{A})$ has a run passing infinitely often through $T$ is PSPACE-
complete.

###### Proof.

Let us prove that there exists a rational-valued valuation satisfying the
property iff there exists an integer-valued valuation doing so.

  * $\Leftarrow$

Considering an integer valuation is also a rational-valued valuation, the
result trivially holds.

  * $\Rightarrow$

Assume there exists a rational-valued parameter valuation $v$ for which
$v(\mathcal{A})$ contains an infinite run passing infinitely often through
locations of $T$. Let $v^{\prime}$ be the integer parameter valuation obtained
from $v$ as follows:

$v^{\prime}(p)=\begin{cases}v(p)&\text{if }v(p)\in{\mathbb{N}}\\\ \lceil
v(p)\rceil&\text{if }p\text{ is an upper-bound parameter}\\\ \lfloor
v(p)\rfloor&\text{if }p\text{ is a lower-bound parameter}\\\ \end{cases}$

From the monotonicity property of L/U-PTAs (Lemma 1), if $v(\mathcal{A})$
yields an infinite run passing infinitely often through locations of $T$, then
$v^{\prime}(\mathcal{A})$ does too.

Observe that this is not true for general PTAs: in Fig. 5(a), there is an
infinite run passing infinitely often through $\ell_{0}$ iff $0<p<1$;
therefore, there exist rational-valued valuations satisfying the property, but
no integer-valued valuation.

Now, in [BLT09, Theorem 8], it is proved that the problem of the emptiness of
the set of integer parameter valuations for which there exists an infinite run
passing infinitely often through $T$ is PSPACE-complete. This concludes the
proof. ∎

######  Theorem 12.

The cycle-existence-emptiness problem is decidable and PSPACE-complete for
L/U-PTAs.

###### Proof.

Let $\mathcal{A}$ be an L/U-PTA. The set of parameter valuations for which
$\mathcal{A}$ has an infinite run is empty iff the set of parameter valuations
for which $\mathcal{A}$ has an infinite run passing infinitely often through
$L$ (where $L$ denotes all locations of $\mathcal{A}$) is empty. Hence we can
directly apply our intermediate Lemma 6 to conclude that this problem is
decidable and PSPACE-complete. ∎

Without surprise (with the rule of thumb that any non-trivial problem for PTAs
is undecidable), this problem becomes undecidable for general PTAs, even when
bounded.

######  Theorem 13.

The cycle-existence-emptiness problem is undecidable for (bounded) PTAs with 3
clocks and 1 parameter.

###### Proof.

We reduce from the boundedness problem of a 2-counter machine, which is
undecidable [Min67].

We start from the construction in the proof of Theorem 1 and add a self-loop
(with no guard) on the location $q_{\mathtt{halt}}$ (encoding the machine
state $\mathtt{q}_{\textrm{halt}}$), ensuring that whenever
$q_{\mathtt{halt}}$ is reachable then there exists an infinite run in the PTA.

Then by examining exactly the same cases as before we see that the value of
the counters remains bounded iff there exists a parameter valuation $v$ such
that $v(\mathcal{A})$ yields an infinite run. Indeed the only two cases for
which we do not have an infinite run correspond to

  1. (1)

$a=0$ (blocked by the initial gadget of Fig. 1(a)), or

  2. (2)

$a>0$ and the counters of the machine are unbounded.

In the latter case, the PTA will block in the increment gadget when taking the
transition from $l_{i2}$ to $l_{i3}$. ∎

Finally note that the EC-emptiness problem for the class of open bounded
L/U-PTAs (that does not fit in Theorems 11 and 12) remains an open problem. We
conjecture that this is decidable using techniques derived from the robustness
results of [San11] but the adaptation appears to require rather lengthy
developments, with techniques quite different from those presented here, and
is thus left to future work.

###  5.3. Deadlock-Existence-Emptiness

######  Theorem 14.

The deadlock-existence-emptiness problem is undecidable for closed bounded
L/U-PTAs, with 3 clocks and 2 parameters.

###### Proof.

We will use a reduction from the halting problem of a 2-counter machine. Let
us consider the encoding used in the proof of Theorem 13, that we transform
into an L/U-PTA by replacing any comparison of a clock with $a$ (say $x=a$)
into $x\leq a^{+}\land x\geq a^{-}$, where $a^{-}$ (resp. $a^{+}$) is a lower-
bound (resp. upper-bound) parameter. The crux of the proof is in the original
enforcement of constraints in the encoding (in particular with location
$q^{\prime}_{\mathtt{halt}}$) such that the deadlock property ensures that
$a^{-}=a^{+}$.

We give the modified increment gadget in Fig. 6(c) (the decrement gadget is
modified in a similar fashion). We replace the initial gadget (Fig. 1(a)) with
the new one in Fig. 6(a). Before initializing the values of the counters, this
gadget first ensures that $a^{-}\leq a^{+}$.

$l_{0}$$l_{1}$$q_{0}$ $a^{-}\leq x\leq a^{+}$
---
$x,y,z:=0$
$x=1$
---
$x:=0$

(a) Initial gadget

$q_{\mathtt{halt}}$$q^{\prime}_{\mathtt{halt}}$$a^{-}\leq x<a^{+}$$a^{-}\leq
x\land x=0$

(b) Final gadget

$q_{i}$$l_{i1}$$l_{i2}$$l^{\prime}_{i2}$$l_{i3}$$q_{j}$$x=0$$\begin{array}[]{l}z=1\\\
z:=0\end{array}$$\begin{array}[]{l}a^{-}+1\leq y\leq a^{+}+1\\\
y:=0\end{array}$$\begin{array}[]{l}a^{-}+1\leq y\leq a^{+}+1\\\
y:=0\end{array}$$\begin{array}[]{l}z=1\\\
z:=0\end{array}$$\begin{array}[]{l}x=1\\\ x:=0\end{array}$

(c) Increment gadget

Figure 6. ED-emptiness for bounded L/U-PTAs

We also add a new location $q^{\prime}_{\mathtt{halt}}$ reachable from
$q_{\mathtt{halt}}$ as shown in the final gadget in Fig. 6(b). Finally, we add
an unguarded transition (i. e., a transition the guard of which is true) from
any location of the encoding (including that of the initial gadget, but
excluding $q_{\mathtt{halt}}$) to location $q^{\prime}_{\mathtt{halt}}$. That
is, it is always possible to reach $q^{\prime}_{\mathtt{halt}}$ from any
location without condition, except from $q_{\mathtt{halt}}$. From that
particular location, $q^{\prime}_{\mathtt{halt}}$ is reachable if and only if
$a^{-}<a^{+}$ or $a^{-}=0$.

We assume the following bounds for the parameters: $a^{-},a^{+}\in[0,1]$.

Let us show that there exists a parameter valuation for which the system
contains at least one deadlock iff the 2-counter machine halts, which is
undecidable [Min67]. Let us reason by cases on the valuations of $a^{-}$ and
$a^{+}$.

  1. (1)

If $a^{-}>a^{+}$, the initial gadget cannot be passed, but thanks to the
unguarded transitions to $q^{\prime}_{\mathtt{halt}}$, all runs eventually end
in $q^{\prime}_{\mathtt{halt}}$, from which the absence of deadlock is
guaranteed by the unguarded self-loop.

  2. (2)

If $a^{-}<a^{+}$, the machine may not be properly simulated because some
transitions do not occur at the right time and some run could reach
$q_{\mathtt{halt}}$ while the machine does not halt. Let us consider a run in
the TA obtained with such a parameter valuation.

    1. (a)

either this run is infinite and remains in the machine (e. g., it loops
infinitely through the increment, decrement and 0-test gadgets of our
encoding). Then there is no deadlock.

    2. (b)

or this run would block in a gadget; in that case, thanks to the unguarded
transitions to $q^{\prime}_{\mathtt{halt}}$, this run can go to
$q^{\prime}_{\mathtt{halt}}$, from which it is deadlock-free.

    3. (c)

or this run reaches $q_{\mathtt{halt}}$ (recall that the value of $x$ is
necessarily 0 when entering $q_{\mathtt{halt}}$); from there, thanks to the
upper transition in Fig. 6(b), it can reach $q^{\prime}_{\mathtt{halt}}$, from
which it is again deadlock-free.

  3. (3)

If $a^{-}=a^{+}=0$, the machine may again not be properly simulated: again we
could reach $q_{\mathtt{halt}}$ while the machine does not halt. The situation
is similar to the previous case ($a^{-}<a^{+}$) except that in
$q_{\mathtt{halt}}$ a run has to take the lower transition in Fig. 6(b) to
reach $q^{\prime}_{\mathtt{halt}}$, from which it is again deadlock-free.

  4. (4)

If $a^{-}=a^{+}>0$:

    1. (a)

Either the machine does not halt:

      1. (i)

…and the counters remain bounded: for some parameter valuations small enough
to encode the value of the counters (typically $a^{-}=a^{+}\leq\frac{1}{c}$,
where $c$ is the maximum value of both $C_{1}$ and $C_{2}$) then the PTA
correctly simulates the infinite execution of the machine, and the system is
deadlock-free. (Note that such valuations can also lead to
$q^{\prime}_{\mathtt{halt}}$ anytime, but this is harmless since this location
guarantees the absence of deadlocks.) For other valuations, at some point we
have $a^{-}c_{1}>1$; more specifically, there is an incrementation of $C_{1}$
such that $a^{-}c_{1}\leq 1$ and $a^{-}(c_{1}+1)>1$. Hence, the run cannot
continue in the encoding, but can reach $q^{\prime}_{\mathtt{halt}}$, from
where the run is non-blocking.

      2. (ii)

…and the counters are unbounded. Then whatever the value of $a^{-}>0$, at some
point we have $a^{-}c_{1}>1$. Then, when executing the corresponding increment
gadget, $q^{\prime}_{\mathtt{halt}}$ can be reached from $l_{i2}$, from where
the run is non-blocking.

Hence if the machine does not halt, the system is deadlock-free for all
parameter valuations.

    2. (b)

Or the machine halts. In this case, if $c$ is the maximum value of both
$C_{1}$ and $C_{2}$ over the (necessarily finite) halting execution of the
machine, and if $c>0$, then for valuations such that
$a^{-}=a^{+}\leq\frac{1}{c}$, then there exists one run that correctly
simulates the machine (beside plenty of runs that will go to
$q^{\prime}_{\mathtt{halt}}$ due to the unguarded transitions from all
locations except $q_{\mathtt{halt}}$); this run that correctly simulates the
machine eventually reaches $q_{\mathtt{halt}}$. From $q_{\mathtt{halt}}$, for
such valuations, the system is deadlocked: indeed, the transitions from
$q_{\mathtt{halt}}$ to $q^{\prime}_{\mathtt{halt}}$ can only be taken if
$a^{-}<a^{+}$ or $a^{-}=0$. And there is no unguarded transition from
$q_{\mathtt{halt}}$ to $q^{\prime}_{\mathtt{halt}}$, which is crucial for the
correctness of our encoding. The set of such valuations for which there exists
a run that correctly simulates the machine is certainly non-empty:
$a^{-}=a^{+}=\frac{1}{c}$ belongs to it (if $c=0$ then we choose, e. g.,
$a^{-}=a^{+}=\frac{1}{2}$). Hence, if the 2-counter machine halts, there exist
parameter valuations for which a run has no discrete successor, and hence the
system is not deadlock-free.

Hence the 2-counter machine halts iff the set of valuations for which the
automaton has at least one deadlock is not empty. ∎

######  Corollary 6.

The deadlock-existence-emptiness problem is undecidable for open bounded
L/U-PTAs, for L/U-PTAs, for bounded PTAs and for PTAs, with 3 clocks and 2
parameters.

###### Proof.

Let us consider each formalism:

open bounded L/U-PTAs:

In the above construction, we can assume, e. g., $a^{-}\in(0,1]$, which does
not impact the proof.

L/U-PTAs:

The bounds on the parameters are not required in the above construction: for
valuations larger than 1 (that necessarily do not simulate correctly the
machine), a gadget may block, therefore leading to
$q^{\prime}_{\mathtt{halt}}$, from which the system is deadlock-free, hence
without impacting the spirit of the proof.

bounded PTAs:

From the fact that a bounded L/U-PTA is a bounded PTA.

PTAs:

From the fact that an L/U-PTA is a PTA.

Observe that the number of parameters can be reduced to 1 for (possibly
bounded) PTAs by merging $a^{-}$ and $a^{+}$ into a single parameter $a$. ∎

###  5.4. EG-Emptiness

We finally prove that the EG-emptiness problem is decidable for closed bounded
L/U-PTAs, and that lifting either closedness or boundedness leads to
undecidability.

######  Theorem 15.

The EG-emptiness problem is decidable for closed bounded L/U-PTAs.

We will use Lemma 1 to deal with infinite paths but it is of no use for
deadlocks: by decreasing lower-bounds or increasing upper-bounds, some
deadlocks can actually be removed.

###### Proof.

Let $\mathcal{A}_{|\mathit{bounds}}$ be a closed bounded L/U-PTA and $T$ be a
subset of its locations. Since $\mathcal{A}$ is closed and bounded, for each
parameter $p$, $\mathit{bounds}(p)$ is a closed interval
$[m^{-}(p),m^{+}(p)]$.

The basic monotonicity property of L/U-PTAs (Lemma 1) ensures that the TA
$v_{\mathrm{inf}/\mathrm{sup}}(\mathcal{A})$, where
$v_{\mathrm{inf}/\mathrm{sup}}$ is obtained by valuating lower-bound
parameters $p^{-}$ by $m^{-}(p)$ and upper-bound parameters $p^{+}$ by
$m^{+}(p)$, includes all the runs that could be produced with other parameter
valuations. Consequently, if there is an infinite path for some valuation,
there is one for $v_{\mathrm{inf}/\mathrm{sup}}$ (note that, as emphasized
above, this is not true for deadlocks).

In $v_{\mathrm{inf}/\mathrm{sup}}(\mathcal{A})$, it is decidable to find an
infinite path staying in $T$, or conclude that none exist: this can be encoded
into the CTL formula $EG(T\land XG)$, to be verified on the (finite) region
graph of $\mathcal{A}$ [AD94]. Since the region equivalence is a time-abstract
bisimulation [TY01], this means for $\mathcal{A}$ “there exists a path that
remains in $T$ and in which every state has a discrete successor (possibly
after letting some time elapse) in $T$”. That path therefore has an infinite
number of discrete actions. If we do find such a path, we can then terminate
by answering yes to the EG-emptiness problem. If we do not, then in
$v_{\mathrm{inf}/\mathrm{sup}}(\mathcal{A})$, all paths staying in $T$ are
finite. If we keep only discrete actions and locations, which are in finite
number, the resulting paths therefore form a finite tree. Let us recall again
that, thanks to Lemma 1, all the discrete paths that stay in $T$ and can be
obtained with any parameter valuation, belong to that tree.

We can now explicitly compute the symbolic states (following the symbolic
semantics recalled in Section 2.2.3) for all the paths in the finite tree (not
only those that are maximal). Recall that each symbolic state $\mathbf{s}$ is
a pair $(\ell,C)$, where $\ell$ is a location and $C$ a convex polyhedron
representing all parameter valuations and clock valuations that can be reached
by the given discrete path. In each of these polyhedra, we can explicitly
check for the existence of a deadlock:

  1. (1)

remove all parts that are in the past of the guard of an outgoing transition
in $\mathcal{A}$ (using operation $C^{\swarrow}$), and that would satisfy the
target location invariant;

  2. (2)

test for emptiness.

If the result is not empty then there exists a point in the tested set which
can be decomposed into a parameter valuation and clock valuation such that, by
any time elapsing from the clock valuation, none of the guards can become
true. We therefore have a deadlock. If the result is empty, by the same
reasoning, we can take a transition (possibly by first letting some time
elapse) from all states of $C$, so none of them are deadlocked. Note that both
operations can be performed using classical polyhedral operations.

If we find a deadlock, then we can terminate and answer yes to the EG-
emptiness problem. Otherwise, we can terminate and answer no, because we have
checked all the potential discrete paths staying in $T$ for any parameter
valuation. ∎

Note that this proof fails when the L/U-PTA is not bounded or closed. In
particular, the closedness plays a key role in the sense that we are able to
test the valuation $v_{\mathrm{inf}/\mathrm{sup}}$. Consider first the L/U-PTA
in Fig. 5(c) made of a single location and a single loop with guard $x=1\wedge
y\leq p$ and a reset of $x$, where $x,y$ are clocks and $p$ a parameter. This
is clearly an L/U-PTA. As $p$ grows, there are more and more discrete
behaviors, but there is no cycle for any parameter valuation. In [BLT09], the
authors provide a finite upper bound $N_{\mathcal{A}}$ for the upper-bound
parameters such that if there exists a valuation such that the valuated
L/U-PTA has an accepting run, then the valuation giving $0$ to lower bound
parameters and $N_{\mathcal{A}}$ to upper-bound parameters also ensures the
existence of an accepting run. That bound used in this example would indeed
prove the non-existence of a cycle for any parameter value, but it does not in
turn allow us to derive a finite tree containing all the discrete behaviors,
for any possible parameter value (a larger bound would still give more runs).

Similarly, now consider the L/U-PTA in Fig. 5(d). If $0$ is excluded from the
domain of $p$, we have a behavior similar to the previous example: as $p$ gets
closer and closer to $0$, we have more and more discrete behaviors. And even
if we could derive a lower bound _à la_ [BLT09] ensuring the non-existence of
a cycle here, it would not give a finite tree of all the possible discrete
behaviors, for any parameter value.

We can actually exhibit a very thin border between decidability and
undecidability of L/U-PTAs by proving that, given a bounded L/U-PTA
$\mathcal{A}_{|\mathit{bounds}}$ with a single open bound in $\mathit{bounds}$
or an unbounded L/U-PTA, the EG-emptiness problem becomes undecidable.

######  Theorem 16.

The EG-emptiness problem is undecidable for open bounded L/U-PTAs, with 4
clocks and 4 parameters.

###### Proof.

We will use a reduction from the halting problem of a 2-counter machine.

$l_{0}$$l_{1}$$q_{0}$ $a^{-}\leq x\leq a^{+}$
---
$x,y,z,w:=0$
$b^{-}\leq x\leq b^{+}$
---
$x,w:=0$

(a) Initial gadget

$q_{\mathtt{halt}}$$w\leq 1$$q^{\prime}_{\mathtt{halt}}$$a^{-}\leq
x<a^{+}$$b^{-}\leq x<b^{+}$

(b) Final gadget

$q_{i}$$l_{i1}$$l_{i2}$$l^{\prime}_{i2}$$l_{i3}$$q_{j}$$x=0$$\begin{array}[]{l}b^{-}\leq
z\leq b^{+}\\\ z:=0\end{array}$$\begin{array}[]{l}a^{-}+b^{-}\leq y\\\
y:=0\end{array}$$\begin{array}[]{l}a^{-}+b^{-}\leq y\\\
y:=0\end{array}$$\begin{array}[]{l}b^{-}\leq z\leq b^{+}\\\
z:=0\end{array}$$\begin{array}[]{l}b^{-}\leq x\leq b^{+}\\\ x:=0\end{array}$

(c) Increment gadget

$q_{i}$$l_{i4}$$l_{i5}$$q_{k}$$l_{i1}$$l_{i2}$$l^{\prime}_{i2}$$l_{i3}$$q_{j}$pt$x=0\land
y<b^{+}$$\begin{array}[]{l}a^{-}+b^{-}\leq z\\\
z:=0\end{array}$$\begin{array}[]{l}b^{-}\leq y\leq b^{+}\\\
y:=0\end{array}$$\begin{array}[]{l}b^{-}\leq y\leq b^{+}\\\
y:=0\end{array}$$\begin{array}[]{l}a^{-}+b^{-}\leq z\\\
z:=0\end{array}$$\begin{array}[]{c}x\leq a^{+}+b^{+}\\\ x:=0\end{array}$
$b^{-}\leq y\leq b^{+}\land x=0$
---
$y:=0$
$b^{-}\leq z\leq b^{+}$
---
$z:=0$
$b^{-}\leq x\leq b^{+}$
---
$x:=0$

(d) Decrement and 0-test gadget

Figure 7. EG-emptiness for bounded L/U-PTAs

Let us consider the encoding used in the proof of Theorem 14, to which we will
perform several modifications.

First, we force the 2-counter machine to execute in a constant 1-time unit
duration as follows:

  1. (1)

We replace any occurrence of “1” in the encoding with a parameter, either
$b^{-}$ or $b^{+}$ (depending on whether the occurrence of 1 occurs as a
lower-bound or an upper-bound); hence the duration of an increment or
decrement gadget is now at least $b^{-}$ and at most $b^{+}$. We give the
increment gadget in Fig. 7(c). The encoding of a counter is as follows: when
$x=0$, then $y=b-ac_{1}$ and $z=b-ac_{2}$, where $a=a^{-}=a^{+}$ and
$b=b^{-}=b^{+}$ (for other parameter valuations, the machine is not properly
simulated). Typically, $b$ will need to be sufficiently small compared to 1 to
encode the required number of steps of the machine, and $a$ will need to be
sufficiently small compared to $b$ to encode the maximum value of the
counters. The decrement part of the “test and decrement” instruction is
modified similarly.

  2. (2)

We modify the zero-test part of the “test and decrement” instruction so that
its duration is within $[b^{-},b^{+}]$, as in Fig. 7(d): only the first
transition from $q_{i}$ to $\ell_{i4}$ encodes the zero-test, the two other
transitions from $\ell_{i4}$ to $\ell_{i5}$ and from $\ell_{i5}$ to $q_{k}$
forcing $[b^{-},b^{+}]$ time units to elapse while keeping the values of the
clocks unchanged, assuming $a^{-}=a^{+}$ and $b^{-}=b^{+}$ (we will see later
that other valuations do not matter). Let $a=a^{-}=a^{+}$ and $b=b^{-}=b^{+}$.
The zero-test requires here that $b=y\land x=0$; in addition, $z$ encodes
$c_{2}$ as follows: $z=b-ac_{2}$. After reaching $l_{i4}$ and waiting enough
time to take the transition to $l_{i5}$ (i. e., a duration in $ac_{2}$) we
have: $z=b$ and $x=y=ac_{2}$. After reaching $l_{i5}$ and waiting enough time
to take the transition to $q_{k}$ (i. e., a duration in $b-ac_{2}$) we have:
$z=b-ac_{2}$ and $x=y=b$. Resetting $x$ gives $x=0$, $y=b$ and $z=b-ac_{2}$,
which was the value when performing the 0-test. So the value of the clocks
remains unchanged when $b^{-}=b^{+}$, and $[b^{-},b^{+}]$ time units have
elapsed in any case.

  3. (3)

We add to any location in the entire system an invariant $w\leq 1$, where $w$
is a fresh clock that is never reset in the increment/decrement/zero-test
gadgets. (These invariants are omitted in Fig. 7.)

Hence, the duration of any gadget is at least $b^{-}$ and therefore for any
valuation $b^{-}>0$ the number of operations the machine can perform is finite
due to the global invariant $w\leq 1$.

Then, before starting the 2-counter machine encoding, we add an initial gadget
given in Fig. 7(a). This gadget constrains $a^{-}\leq a^{+}$, $b^{-}\leq
b^{+}$, and is such that when leaving the gadget then $y,z\in[b^{-}\leq
b^{+}]$ while $x,w$ are 0. When $b^{-}=b^{+}$, this correctly encodes that the
value of both counters is 0.

Then, we add a new $q^{\prime}_{\mathtt{halt}}$ location (without any
invariant, i. e., not requiring $w\leq 1$), with two transitions from
$q_{\mathtt{halt}}$ as depicted in Fig. 7(b). We then add a transition (with
no guard) from any location of the encoding (except $q_{\mathtt{halt}}$) to
$q^{\prime}_{\mathtt{halt}}$. That is, for any increment gadget, if the value
of the parameters is not small enough to correctly simulate the machine, then
the system is not deadlocked, and can lead instead to
$q^{\prime}_{\mathtt{halt}}$. (If the value is small enough, the system can
either lead to $q^{\prime}_{\mathtt{halt}}$ or continue in the 2-counter
machine encoding.) We also add a transition to $q^{\prime}_{\mathtt{halt}}$
(with no guard) from all locations in the initial gadget in Fig. 7(a).

We assume the following bounds for the parameters: $a^{-},a^{+},b^{+}\in[0,1]$
and $b^{-}\in(0,1]$.

Let us show that the 2-counter machine halts iff the set of valuations
satisfying $\mathrm{EG}(L\setminus\\{q^{\prime}_{\mathtt{halt}}{}\\})$ is not
empty.

  1. (1)

If $a^{-}>a^{+}$ or $b^{-}>b^{+}$, the initial gadget cannot be passed, and
thanks to the transitions to $q^{\prime}_{\mathtt{halt}}$, all runs eventually
reach $q^{\prime}_{\mathtt{halt}}$, hence
$\mathrm{EG}(L\setminus\\{q^{\prime}_{\mathtt{halt}}{}\\})$ does not hold.

  2. (2)

If $a^{-}<a^{+}$ and $b^{-}\leq b^{+}$, then the machine may not be correctly
simulated: a given run will either reach $q_{\mathtt{halt}}$, in which case it
will also reach $q^{\prime}_{\mathtt{halt}}$ (as the guard from
$q_{\mathtt{halt}}$ to $q^{\prime}_{\mathtt{halt}}$ does not forbid this run),
or it will loop in the machine until it eventually gets “blocked” (since
$b^{-}>0$ and because of the invariant $w\leq 1$, for any value of $b^{-}$,
the maximal number of steps is $\frac{1}{b^{-}}$); when being blocked, it has
no other option than going to $q^{\prime}_{\mathtt{halt}}$, thanks to the
unguarded transitions from any location to $q^{\prime}_{\mathtt{halt}}$. Hence
if $a^{-}<a^{+}$, $\mathrm{EG}(L\setminus\\{q^{\prime}_{\mathtt{halt}}{}\\})$
does not hold.

  3. (3)

If $b^{-}<b^{+}$ (and $a^{-}\leq a^{+}$), again the machine may not be
correctly simulated, and following a similar reasoning,
$\mathrm{EG}(L\setminus\\{q^{\prime}_{\mathtt{halt}}{}\\})$ again does not
hold.

  4. (4)

If $a^{-}=a^{+}$ and $b^{-}=b^{+}>0$:

    1. (a)

Either the machine does not halt: in this case, after a maximum number of
steps (typically $\frac{1}{b^{-}}$), a gadget will be blocked due to the
invariant $w\leq 1$, and the run will end in $q^{\prime}_{\mathtt{halt}}$.
Hence if the 2-counter machine does not halt,
$\mathrm{EG}(L\setminus\\{q^{\prime}_{\mathtt{halt}}{}\\})$ does not hold.

    2. (b)

Or the machine halts: in this case, if $c$ is the maximum value of both
$C_{1}$ and $C_{2}$ over the (necessarily finite) halting execution of the
machine, and if $m$ is the length of this execution, and if $c>0$, then for
valuations such that $a^{-}=a^{+}\leq\frac{b^{-}}{c}$ and
$b^{-}=b^{+}\leq\frac{1}{m}$, then there exists one run that correctly
simulates the machine (beside plenty of runs that will go to
$q^{\prime}_{\mathtt{halt}}$ due to the unguarded transitions); this run that
correctly simulates the machine eventually reaches $q_{\mathtt{halt}}$. From
$q_{\mathtt{halt}}$, for such valuations, the system is deadlocked: indeed,
the transitions from $q_{\mathtt{halt}}$ to $q^{\prime}_{\mathtt{halt}}$ can
only be taken if $a^{-}<a^{+}$ or $b^{-}<b^{+}$. Hence
$\mathrm{EG}(L\setminus\\{q^{\prime}_{\mathtt{halt}}{}\\})$ holds. The set of
such valuations is certainly non-empty: $a^{-}=a^{+}=\frac{1}{m\times c}$ and
$b^{-}=b^{+}=\frac{1}{m}$ belongs to it (if $c=0$ then we choose, e. g.,
$b^{-}=b^{+}=1$ and $a^{-}=a^{+}=\frac{1}{2}$). Hence, if the 2-counter
machine halts, there exist parameter valuations for which
$\mathrm{EG}(L\setminus\\{q^{\prime}_{\mathtt{halt}}{}\\})$ holds.

Hence the 2-counter machine halts iff the set of valuations for which
$\mathrm{EG}(L\setminus\\{q^{\prime}_{\mathtt{halt}}{}\\})$ holds is not
empty. ∎

######  Remark 2.

The above construction works over 1 time unit (an invariant can be added to
$q^{\prime}_{\mathtt{halt}}{}$ too), so this gives an undecidability result
over bounded time as well.

We now prove that EG-emptiness is also undecidable for unbounded L/U-PTAs.
When not considering L/U-PTAs, proving an undecidability result for bounded
PTAs gives the undecidability for unbounded PTAs, as a bounded PTA can be
simulated using a PTA (by, e. g., adding the bounds as a guard between a fresh
location prior to the initial location and the initial location, e. g.,
$p\in[\mathrm{inf},\mathrm{sup}]$ becomes $\mathrm{inf}\leq
x\leq\mathrm{sup}\land p=x$). Recall that this is not true for L/U-PTAs, as
such a construction requires to compare the clock and the parameter using an
equality; in addition, L/U-PTAs are incomparable with bounded L/U-PTAs
[ALR16b]. In addition, our proof for unbounded L/U-PTAs uses one parameter
less than for open bounded L/U-PTAs.

######  Theorem 17.

The EG-emptiness problem is undecidable for L/U-PTAs with 4 clocks and 3
parameters.

###### Proof.

We will again use a reduction from the halting problem of a 2-counter machine.
Our proof essentially relies on a mechanism similar to the proof of Theorem
16; however, we must use a different PTA encoding (the encoding used in the
proof of Theorem 16 does not work for unbounded L/U-PTAs, as it strongly
relies on the fact that $b^{-}$ be strictly positive), which prevents us to
factor the proof as much as we would have wished.

We propose here an encoding inspired by that of a 2-counter machine proposed
in [BBLS15] to prove the undecidability of the EF-emptiness problem for PTAs
with a single integer-valued parameter used to encode the maximum value of the
two counters (although not considered in [BBLS15], the proof also works
identically with a rational-valued parameter). Two different instructions are
considered:

  * •

when in state $\mathtt{q}_{i}$, increment $C_{k}$ and go to $\mathtt{q}_{j}$;

  * •

when in state $\mathtt{q}_{i}$, if $C_{k}=0$ then go to $\mathtt{q}_{k}$,
otherwise decrement $C_{k}$ and go to $\mathtt{q}_{j}$;

Starting from the initial configuration $(\mathtt{q}_{0},C_{1}=0,C_{2}=0)$ the
machine either reaches $q_{\mathtt{halt}}$ and halts, or loops forever.
Knowing whether the machine halts is undecidable [Min67].

The encoding uses a single parameter $a$. Two clocks $x$ and $y$ are used to
encode the value of the counters, while a third clock $z$ is used as an
auxiliary clock. Whenever $z=0$, then $x=c_{1}$ and $y=c_{2}$.

We modify this encoding by splitting the single parameter $a$ into a lower-
bound parameter $a^{-}$ and an upper-bound parameter $a^{+}$, in the spirit of
previous undecidability results for L/U-PTAs in this paper (Theorems 14 and
16).

In addition, we request that the entire execution takes a time less than
$b^{+}$, where $b^{+}$ is a fresh upper-bound parameter; this is achieved by
adding an invariant $w\leq b^{+}$ to all locations (with $w$ a fresh clock
never reset after the initial gadget).

We give the modified increment gadget for the first counter in Fig. 8(c)
(invariants are omitted). Note that, if $z=0$ when entering $q_{i}$ then the
time to pass this gadget is in $[a^{-}+1,a^{+}+1]$.

$l_{0}$$l_{1}$$q_{0}$ $a^{-}\leq x\leq a^{+}$
---
$x:=0$
$0<x\leq b^{+}$
---
$x,y,z,w:=0$

(a) Initial gadget

$q_{\mathtt{halt}}$$w\leq b^{+}$$q^{\prime}_{\mathtt{halt}}$$a^{-}\leq
x<a^{+}$

(b) Final gadget

$q_{i}$$l_{i1}$$l_{i4}$$l_{i2}$$l_{i2^{\prime}}$$l_{i3}$$l_{i3^{\prime}}$$q_{j}$
$z=1$
---
$z:=0$
$a^{-}\leq x\leq a^{+}$
---
$x:=0$
$a^{-}\leq y\leq a^{+}$
---
$y:=0$
$y=1$
---
$y:=0$
$a^{-}\leq y\leq a^{+}$
---
$y:=0$
$y=1$
---
$y:=0$
$a^{-}\leq x\leq a^{+}$
---
$x:=0$
$a^{-}\leq z\leq a^{+}$
---
$z:=0$

(c) Increment gadget

$q_{i}$$l_{i1}$$l_{i4}$$l_{i2}$$l_{i2^{\prime}}$$l_{i3}$$l_{i3^{\prime}}$$q_{j}$$l_{i1^{\prime\prime}}$$l_{i2^{\prime\prime}}$$q_{k}$
$z=0\land x>0$
---
$a^{-}\leq x\leq a^{+}$
---
$x:=0$
$x=1$
---
$x:=0$
$a^{-}\leq y\leq a^{+}$
---
$y:=0$
$a^{-}\leq y\leq a^{+}$
---
$y:=0$
$a^{-}\leq x\leq a^{+}$
---
$x:=0$
$x=1$
---
$x:=0$
$a^{-}\leq z\leq a^{+}$
---
$z:=0$
$z=0\land x=0$
---
$a^{-}+1\leq y\leq a^{+}+1$
---
$y:=0$
$a^{-}+1\leq x\leq a^{+}+1$
---
$x,z:=0$

(d) 0-test and decrement gadget

Figure 8. EG-emptiness for L/U-PTAs

The test and decrement gadget is similar, and given in Fig. 8(d). We performed
a slight modification to the zero-test of [BBLS15], that was executed in
0-time; we require in our construction that each gadget takes at least one
time unit. Hence, we rewrote it in Fig. 8(d) so as to force at least one time
unit to elapse after the clocks are tested, and so that the final value of the
clock is not changed, when $a^{-}=a^{+}$ (in the spirit of the same operation
in the proof of Theorem 16): when performing the zero-test, we have $x=z=0$
and $y=c_{2}$. Then after $a-c_{2}+1$ time units (with $a=a^{+}=a^{-}$), we
have $x=z=a+1-c_{2}$ and $y=a+1$, and we can take the transition to
$l_{i2^{\prime\prime}}$, resetting $y$. Then after $c_{2}$ time units, we have
$x=z=a+1$ and $y=c_{2}$ and we can take the transition to
$l_{i2^{\prime\prime}}$, resetting $x$ and $z$. This gives finally $x=z=0$ and
$y=c_{2}$ and the time spent in the gadget is in $[a^{-}+1,a^{+}+1]$, and
therefore is more than one time unit. Gadgets for the second counter are
symmetric.

We add before the first instruction the initial gadget given in Fig. 8(a),
constraining $a^{-}\leq a^{+}$ and $b^{+}>0$, and resetting all clocks.

In addition, just as in Theorem 16, we add unguarded transitions from any
location (including that of the initial gadget, but excluding
$q_{\mathtt{halt}}$) to a new location $q^{\prime}_{\mathtt{halt}}$. We also
add two transitions from $q_{\mathtt{halt}}$ to $q^{\prime}_{\mathtt{halt}}$
given in the final gadget in Fig. 8(b).

Let us show that the 2-counter machine halts iff the set of valuations for
which $\mathrm{EG}(L\setminus\\{q^{\prime}_{\mathtt{halt}}{}\\})$ holds is not
empty. We reason on the parameter valuations.

  1. (1)

If $a^{-}>a^{+}$ or $b^{+}=0$, the initial gadget cannot be passed: any run is
sent to $q^{\prime}_{\mathtt{halt}}$ because of the transitions to
$q^{\prime}_{\mathtt{halt}}$, and therefore
$\mathrm{EG}(L\setminus\\{q^{\prime}_{\mathtt{halt}}{}\\})$ does not hold.

  2. (2)

If $a^{-}<a^{+}$ and $b^{+}>0$, then the machine may not be correctly
simulated: a given run will either reach $q_{\mathtt{halt}}$, in which case it
will also reach $q^{\prime}_{\mathtt{halt}}$ (as the guard from
$q_{\mathtt{halt}}$ to $q^{\prime}_{\mathtt{halt}}$ in Fig. 8(b) does not
forbid this run), or it will loop in the machine until it eventually gets
blocked: since $b^{+}>0$, since all gadgets require at least 1 time unit, for
any value of $b^{+}$ the invariant $z\leq b^{+}$ will eventually block a
transition after at most $b^{+}$ steps. When being blocked, a run has no other
option than going to $q^{\prime}_{\mathtt{halt}}$, because of the unguarded
transitions from any location to $q^{\prime}_{\mathtt{halt}}$. Hence if
$a^{-}<a^{+}$ and $b^{+}>0$,
$\mathrm{EG}(L\setminus\\{q^{\prime}_{\mathtt{halt}}{}\\})$ does not hold.

  3. (3)

Now, assume $a^{-}=a^{+}$ and $b^{+}>0$.

    1. (a)

Either the machine does not halt: in this case, after a maximum number of
steps (typically at most $b^{+}$), a gadget will be blocked due to the
invariant $z\leq b^{+}$, and the run will end in $q^{\prime}_{\mathtt{halt}}$
because of the unguarded transitions from any location to
$q^{\prime}_{\mathtt{halt}}$. Hence if the 2-counter machine does not halt,
$\mathrm{EG}(L\setminus\\{q^{\prime}_{\mathtt{halt}}{}\\})$ does not hold.

    2. (b)

Or the machine halts: in this case, if $c$ is the maximum value of both
$C_{1}$ and $C_{2}$ over the (necessarily finite) halting execution of the
machine, and if $m$ is the length of this execution, and if $c>0$, then for
valuations such that $a^{-}=a^{+}\leq c$ and sufficiently large valuations of
$b^{+}$ (typically $b^{+}\geq m\times(a^{+}+1)$ as a gadget can take up to
$a^{+}+1$ time units), then there exists one run that correctly simulates the
machine; this run eventually reaches $q_{\mathtt{halt}}$. From
$q_{\mathtt{halt}}$, for such values, the system is deadlocked. Hence, if the
2-counter machine halts, there exist parameter valuations for which a run does
not reach $q^{\prime}_{\mathtt{halt}}$, i. e., for which
$\mathrm{EG}(L\setminus\\{q^{\prime}_{\mathtt{halt}}{}\\})$ holds.

Hence the 2-counter machine halts iff the set of valuations for which
$\mathrm{EG}(L\setminus\\{q^{\prime}_{\mathtt{halt}}{}\\})$ holds is not
empty. ∎

######  Remark 3.

The above construction works also for integer-valued parameters, so this gives
an undecidability result for integer-valued parameters too. The proof also
works over discrete time (with integer-valued parameters).

Finally, using a single parameter $a$ instead of both $a^{-}$ and $a^{+}$ in
the above proof, we obtain a PTA (not L/U) with two parameters. Hence:

######  Corollary 7.

The EG-emptiness problem is undecidable for PTAs with 4 clocks and 2
parameters.

##  6\. Summary

Class | bL/U-PTAs | bIP-PTAs | L/U-PTAs | IP-PTAs | bPTAs | PTAs
---|---|---|---|---|---|---
EF-empt. |  Theorem 9 |  Theorem 3 | [HRSV02] |  Theorem 8 | [Mil00] | [AHV93]
EF-univ. |  Theorem 9 |  Theorem 7 | [BLT09] |  Corollary 4 |  Corollary 4 |  Corollary 4
AF-empt. |  Theorem 10 |  Corollary 5 | [JLR15] |  Corollary 5 |  Corollary 5 | [JLR15]
Table 1. Decidability results for PTAs and some subclasses

We give a summary of our results concerning EF-emptiness, EF-universality and
AF-emptiness in Table 1. We give from left to right the (un)decidability for
bounded L/U-PTAs, bounded IP-PTAs, L/U-PTAs, IP-PTAs, bounded PTAs, and PTAs.
Decidability is given in bold green, whereas undecidability is given in italic
red. Our contributions are depicted using a plain background, whereas existing
results are depicted using a light background.

bounded L/UL/UIP-PTAclosed L/Ubounded PTAsPTAs

(a) EF-emptiness

bounded L/UL/UIP-PTAclosed L/Ubounded PTAsPTAs

(b) EF-universality

bounded L/UL/UIP-PTAclosed L/Ubounded PTAsPTAs

(c) AF-emptiness

Figure 9. Decidability results for PTAs and subclasses

We give another summary in Fig. 9. Note that bounded L/U-PTAs and L/U-PTAs are
in fact incomparable of terms of expressiveness [ALR16b]; they are therefore
not included into each other in the figures. Decidability (resp.
undecidability) is depicted in plain green (resp. dashed red); open problems
are depicted in dotted black. Our contributions are depicted in thick.

Class | PTAs | L/U-PTAs | bo L/U-PTAs | bc L/U-PTAs
---|---|---|---|---
EC-emptiness |  Theorem 13 |  Theorem 11 | Open |  Theorem 12
ED-emptiness |  Corollary 6 |  Corollary 6 |  Theorem 14 |  Corollary 6
EG-emptiness |  Corollary 7 |  Theorem 17 |  Theorem 16 |  Theorem 15
Table 2. Decidability of EG for L/U-PTAs

We then review our results concerning EG-emptiness, ED-emptiness and EC-
emptiness in Table 2, where “bo L/U-PTAs” and “bc L/U-PTAs” denote bounded
open and bounded closed L/U-PTAs respectively. Again, bold green denotes
decidability and red denotes undecidability.

##  7\. Conclusion

Despite the vast number of undecidability results linked to the formalism of
parametric timed automata, and to which we also contribute in this paper, we
exhibited a new subclass of PTAs (namely bounded IP-PTAs) for which the EF-
emptiness problem is decidable. By showing that bounded IP-PTAs are
incomparable with L/U-PTAs, we strictly extend the set of PTAs for which this
problem is decidable. Although we showed that it cannot be decided whether a
PTA is an IP-PTA, we introduced a new syntactic subclass of IP-PTAs, namely
reset-PTAs, for which, when bounded, the EF-emptiness problem is decidable. It
is worth noting that, to the best our knowledge, there is no other non-trivial
set of syntactic restrictions making the reachability emptiness problem
decidable for PTAs (aside from L/U-PTAs, of course).

We also considered several decision problems, and contributed in solving
several open problems for PTAs and subclasses: this was achieved thanks to the
results proved for IP-PTAs, and to (variations of) an original proof for the
undecidability of the EF-emptiness problem for general PTAs with a single
bounded rational-valued parameter and only non-strict constraints.

We also have achieved some decidability for the existential parametric problem
on the EG liveness property. This could be done by imposing original
constraints to the classical subclass of L/U-PTAs, pertaining to the topology
of the domain of the parameter values. This domain should be a closed and
bounded hyperrectangle of the rational space. The subclass together with the
EG property really lies on the boundary of decidability: on the one hand, we
have proved that considering unbounded, or bounded but open domains leads
again to undecidability for EG. On the other hand, if we consider—instead of
the EG property which asks for the existence of a maximal finite or infinite
path staying in some locations—only infinite maximal paths (existence of
discrete cycles), then we have proved that the problem becomes decidable (for
either closed bounded domains, or unbounded domains—the case of open bounded
domains remains open). And finally, if we consider only finite maximal paths
(existence of deadlocks), then we have proved that the problem becomes
consistently undecidable.

### Future works

Future work includes

  1. (1)

studying the decidability of EC-emptiness for open bounded L/U-PTAs (possibly
adapting techniques developed in [San11]),

  2. (2)

extending the EG decidability result to shapes other than hyperrectangles, and

  3. (3)

studying actual synthesis, and implementing efficient algorithms.

In addition, the decidability of problems we proved undecidable for L/U-PTAs
should be studied for two subclasses of L/U-PTAs, where all parameters are
upper bounds (U-PTAs) or all lower bounds (L-PTAs).

## References

  * [ACEF09] Étienne André, Thomas Chatain, Emmanuelle Encrenaz, and Laurent Fribourg.  An inverse method for parametric timed automata.  International Journal of Foundations of Computer Science, 20(5):819–836, 10 2009.
  * [AD94] Rajeev Alur and David L. Dill.  A theory of timed automata.  Theoretical Computer Science, 126(2):183–235, April 1994.
  * [AHV93] Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi.  Parametric real-time reasoning.  In S. Rao Kosaraju, David S. Johnson, and Alok Aggarwal, editors, STOC, pages 592–601, New York, NY, USA, 1993. ACM.
  * [AL17] Étienne André and Didier Lime.  Liveness in L/U-parametric timed automata.  In Alex Legay and Klaus Schneider, editors, ACSD, pages 9–18. IEEE, 2017.
  * [ALM20] Étienne André, Didier Lime, and Nicolas Markey.  Language preservation problems in parametric timed automata.  Logical Methods in Computer Science, 16, 1 2020.
  * [ALR15] Étienne André, Didier Lime, and Olivier H. Roux.  Integer-complete synthesis for bounded parametric timed automata.  In RP, volume 9058 of Lecture Notes in Computer Science. Springer, 2015.
  * [ALR16a] Étienne André, Didier Lime, and Olivier H. Roux.  Decision problems for parametric timed automata.  In Kazuhiro Ogata, Mark Lawford, and Shaoying Liu, editors, ICFEM, volume 10009 of Lecture Notes in Computer Science, pages 400–416. Springer, 2016.
  * [ALR16b] Étienne André, Didier Lime, and Olivier H. Roux.  On the expressiveness of parametric timed automata.  In Martin Fränzle and Nicolas Markey, editors, FORMATS, volume 9984 of Lecture Notes in Computer Science, pages 19–34. Springer, 2016.
  * [ALR18] Étienne André, Didier Lime, and Mathias Ramparison.  TCTL model checking lower/upper-bound parametric timed automata without invariants.  In David N. Jansen and Pavithra Prabhakar, editors, FORMATS, volume 11022 of Lecture Notes in Computer Science, pages 1–17. Springer, 2018.
  * [ALR19] Étienne André, Didier Lime, and Mathias Ramparison.  Parametric updates in parametric timed automata.  In Jorge A. Pérez and Nobuko Yoshida, editors, FORTE, volume 11535 of Lecture Notes in Computer Science, pages 39–56. Springer, 2019.
  * [And19] Étienne André.  What’s decidable about parametric timed automata?  International Journal on Software Tools for Technology Transfer, 21(2):203–219, 4 2019.
  * [BBLS15] Nikola Beneš, Peter Bezděk, Kim Gulstrand Larsen, and Jiří Srba.  Language emptiness of continuous-time parametric timed automata.  In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, ICALP, Part II, volume 9135 of Lecture Notes in Computer Science, pages 69–81. Springer, July 2015.
  * [BLT09] Laura Bozzelli and Salvatore La Torre.  Decision problems for lower/upper bound parametric timed automata.  Formal Methods in System Design, 35(2):121–151, 2009.
  * [BO14] Daniel Bundala and Joël Ouaknine.  Advances in parametric real-time reasoning.  In Erzsébet Csuhaj-Varjú, Martin Dietzfelbinger, and Zoltán Ésik, editors, MFCS, Part I, volume 8634 of Lecture Notes in Computer Science, pages 123–134. Springer, 2014.
  * [BR07] Véronique Bruyère and Jean-François Raskin.  Real-time model-checking: Parameters everywhere.  Logical Methods in Computer Science, 3(1:7), 2007.
  * [BY03] Johan Bengtsson and Wang Yi.  Timed automata: Semantics, algorithms and tools.  In Lectures on Concurrency and Petri Nets, Advances in Petri Nets, volume 3098 of Lecture Notes in Computer Science, pages 87–124. Springer, 2003.
  * [CES86] Edmund M. Clarke, E. Allen Emerson, and A. Prasad Sistla.  Automatic verification of finite-state concurrent systems using temporal logic specifications.  ACM Transactions on Programming Languages and Systems, 8(2):244–263, 1986.
  * [Doy07] Laurent Doyen.  Robust parametric reachability for timed automata.  Information Processing Letters, 102(5):208–213, 2007.
  * [HKPV98] Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya.  What’s decidable about hybrid automata?  Journal of Computer and System Sciences, 57(1):94–124, 1998.
  * [HRSV02] Thomas Hune, Judi Romijn, Mariëlle Stoelinga, and Frits W. Vaandrager.  Linear parametric model checking of timed automata.  Journal of Logic and Algebraic Programming, 52-53:183–220, 2002.
  * [JLR15] Aleksandra Jovanović, Didier Lime, and Olivier H. Roux.  Integer parameter synthesis for real-time systems.  IEEE Transactions on Software Engineering, 41(5):445–461, 2015.
  * [Lam77] Leslie Lamport.  Proving the correctness of multiprocess programs.  IEEE Transactions on Software Engineering, 3(2):125–143, 1977.
  * [Mil00] Joseph S. Miller.  Decidability and complexity results for timed automata and semi-linear hybrid automata.  In Nancy A. Lynch and Bruce H. Krogh, editors, HSCC, volume 1790 of Lecture Notes in Computer Science, pages 296–309. Springer, 2000.
  * [Min67] Marvin L. Minsky.  Computation: finite and infinite machines.  Prentice-Hall, Inc., 1967.
  * [Qua14] Karin Quaas.  MTL-model checking of one-clock parametric timed automata is undecidable.  In Étienne André and Goran Frehse, editors, SynCoP, volume 145 of EPTCS, pages 5–17, 2014.
  * [San11] Ocan Sankur.  Untimed language preservation in timed systems.  In MFCS, volume 6907 of Lecture Notes in Computer Science, pages 556–567. Springer, August 2011.
  * [Sch86] Alexander Schrijver.  Theory of linear and integer programming.  John Wiley & Sons, Inc., New York, NY, USA, 1986.
  * [TY01] Stavros Tripakis and Sergio Yovine.  Analysis of timed systems using time-abstracting bisimulations.  Formal Methods in System Design, 18(1):25–68, 2001.
  * [Wan96] Farn Wang.  Parametric timing analysis for real-time systems.  Information and Computation, 130(2):131–150, 1996.