# Liveness in L/U-Parametric Timed Automata

Étienne André, Didier Lime

► To cite this version:

Étienne André, Didier Lime. Liveness in L/U-Parametric Timed Automata. 2016. hal-01304232

HAL Id: hal-01304232

https://hal.science/hal-01304232

Preprint submitted on 19 Apr 2016

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Liveness in L/U-Parametric Timed Automata*

Étienne André and Didier Lime

École Centrale de Nantes, IRCCyN, CNRS, UMR 6597, France

## Abstract

We study timed systems in which some timing features are unknown parameters. Parametric timed automata are a classical formalism for such systems but for which most interesting problems are 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 a lower bounds.

We further study L/U-PTAs by considering liveness related problems. We prove that: (1) the existence of at least one parameter valuation for which there exists an infinite run in the automaton is PSPACE-complete; (2) the existence of a parameter valuation such that the system has a deadlock is however undecidable; (3) 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.

**1998 ACM Subject Classification** D.2.4 Software/Program Verification: Formal methods

**Keywords and phrases** L/U-PTA, EG-emptiness, deadlock-freeness, infinite run

**Digital Object Identifier** 10.4230/LIPIcs.CVIT.1942.23

## 1 Introduction

Following Lamport, properties of systems are often characterized as safety properties ("something bad will never happen") and liveness properties ("something good will eventually happen") [11]. Safety generally reduces to reachability, while liveness is more complex. The "good" behavior may not be reached 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 [7].

We study here those 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) [2] have been introduced to deal with such parametric timed systems. They consist in finite automata equipped with real-valued clocks that can be compared with constants or parameters in constraints restricting if and when the edges can be taken.

The simple problem of whether there exists a valuation for each parameter such that some control location is reachable in the timed automaton obtained by replacing the parameters with those valuations (also called EF-emptiness) is undecidable for PTAs for both integer- and rational-valued parameters. Several alternative proofs refine this result in terms of the number of parameters, number of clocks compared to parameters, types of constraints, etc. (see, *e. g.*, [12, 8, 5, 3]).

<figure><img src="image_2.png" /></figure>

<footnote>* This work is partially supported by the ANR national research program "PACS" (ANR-14-CE28-0002).</footnote>
## 23:2 Liveness in L/U-Parametric Timed Automata

In order to overcome these disappointing results, lower-bound/upper-bound parametric timed automata (L/U-PTAs) are introduced as a subclass of PTAs where each parameter either always appears as an upper bound when compared to a clock, or always as a lower bound [9]. The EF-emptiness problem, and also the EF-universality problem ("Can we reach a given location, regardless of what valuations we give to the parameters?") are decidable for L/U-PTAs.

In [6], infinite acceptance properties are considered: the emptiness and the universality of the valuation set for which a given location is infinitely often traversed are decidable for integer-valued parameters. In [10], it is shown that the AF-emptiness problem ("Does there exist a valuation of the parameters, such that the system reaches a given location for all runs?") is undecidable for L/U-PTAs with integer- and rational-valued parameters.

## Contribution

With the notable exception of [10], and to some extent of [6] 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 [10] 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. deciding the existence of at least one parameter valuation for which there exists an infinite run in the automaton is PSPACE-complete;

2. deciding 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: 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.

## Outline

We recall the necessary preliminaries in Section 2. We then consider the problem of the existence of at least one parameter valuation for which there exists an infinite run (Section 3), for which there exists a deadlock (Section 4), and for which a run remains in a given set of locations (Section 5). We conclude and discuss perspectives in Section 6.

# 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., of the form $[a, b]$, $(a, b]$, $[a, b)$ or $(a, b)$ where $a, b \in \mathbb{N}$ and $a \le 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 \to \mathbb{R}_+$. We
## 2.2 Parametric Timed Automata

<footnote>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.</footnote>

<footnote>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 \to \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 such that $\forall p \in P, v(p) \in \mathbb{N}$.</footnote>

<footnote>In the following, we assume $\sim \in \{<, \le, \ge, >\}$. Throughout this paper, $lt$ denotes a linear term over $X \cup P$ of the form $\sum_{1 \le i \le H} \alpha_i x_i + \sum_{1 \le j \le 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$ (i. e., a convex polyhedron) over $X \cup P$ is a conjunction of inequalities of the form $lt \sim 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$ s.t. $w|v \models C$.</footnote>

<footnote>A guard $g$ is a constraint over $X \cup P$ defined by inequalities of the form $x \sim \sum_{1 \le j \le M} \beta_j p_j + d$, with $\beta_j \in \{0, 1\}$ and $d \in \mathbb{Z}$.</footnote>

<footnote>**► Definition 1.** A PTA $\mathcal{A}$ is a tuple $\mathcal{A} = (\Sigma, L, l_0, X, P, I, E)$, where: i) $\Sigma$ is a finite set of actions, ii) $L$ is a finite set of locations, iii) $l_0 \in L$ is the initial location, iv) $X$ is a finite set of clocks, v) $P$ is a finite set of parameters, vi) $I$ is the invariant, assigning to every $l \in L$ a guard $I(l)$, vii) $E$ is a finite set of edges $e = (l, g, \sigma, R, l')$ where $l, l' \in L$ are the source and target locations, $\sigma \in \Sigma$, $R \subseteq X$ is a set of clocks to be reset, and $g$ is a guard.</footnote>

<footnote>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)$.</footnote>

<footnote>**► Definition 2 (Concrete semantics of a TA).** Given a PTA $\mathcal{A} = (\Sigma, L, l_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</footnote>

<footnote>$S = \{(l, w) \in L \times \mathbb{R}_+^H \mid w|v \models I(l)\}, s_0 = (l_0, \vec{0})$</footnote>

<footnote>$\rightarrow$ consists of the discrete and (continuous) delay transition relations:</footnote>

<footnote>discrete transitions: $(l, w) \stackrel{e}{\rightarrow} (l', w')$, if $(l, w), (l', w') \in S$, there exists $e = (l, g, \sigma, R, l') \in E$, $w' = [w]_R$, and $w|v \models g$.</footnote>

<footnote>delay transitions: $(l, w) \stackrel{d}{\rightarrow} (l, w+d)$, with $d \in \mathbb{R}_+$, if $\forall d' \in [0, d], (l, w+d') \in S$.</footnote>

<footnote>Moreover we write $(l, w) \stackrel{e}{\mapsto} (l', w')$ for a sequence of delay and discrete transitions where $((l, w), e, (l', w')) \in \mapsto$ if $\exists d, w'' : (l, w) \stackrel{d}{\rightarrow} (l, w'') \stackrel{e}{\rightarrow} (l', w')$.</footnote>

<footnote>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 (or simply a run) of $v(\mathcal{A})$ is an 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{e_0}{\rightarrow} s_1 \stackrel{e_1}{\rightarrow} \dots \stackrel{e_{m-1}}{\rightarrow} s_m$, such that for all $i = 0, \dots, m-1$, $e_i \in E$, and $(s_i, e_i, s_{i+1}) \in \mapsto$. Given a state $s = (l, 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 $l$ is reachable in $v(\mathcal{A})$, if there exists a state</footnote>
1

2

3

4

5

6

(l, w) that is reachable. Given a set of locations $G \subseteq L$, we say that a run stays in G if all of its states (l, w) are such that $l \in G$. 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.3 Subclasses of PTAs

7

8

9

10

11

**► 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, whenever it appears in a guard or an invariant $x \sim \sum_{1 \le j \le M} \beta_j p_j + d$ (where $\beta_i = 1$) then necessarily $\sim \in \{\le, <\}$ (resp. $\sim \in \{\ge, >\}$).

12

13

14

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

15

16

17

**► Lemma 4.** Let $\mathcal{A}$ be an L/U-PTA and $v$ be a parameter valuation. Let $v'$ be a valuation such that for each upper-bound parameter $p^+$, $v'(p^+) \ge v(p^+)$ and for each lower-bound parameter $p^-$, $v'(p^-) \le v(p^-)$. Then any run of $v(\mathcal{A})$ is a run of $v'(\mathcal{A})$.

18

19

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

20

21

22

23

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

24

25

We say that a bounded PTA is a *closed bounded PTA* if, for each parameter *p*, its ranging interval *bounds*(*p*) is of the form $[\inf, \sup]$; otherwise it is an *open bounded PTA*.

26

We define similarly bounded L/U-PTAs.

## 2.4 Decision Problems

27

28

Let $\mathcal{P}$ be a given a class of decision problems.

**P-emptiness problem:**

29

**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?

30

In this paper, we mainly focus on the following three decision problems:

<figure><img src="image_3.png" /></figure>

* deadlock-existence: given a TA $v(\mathcal{A})$, is there at least one run of $v(\mathcal{A})$ that is deadlocked, i. e., has no discrete successor (possibly after some delay)?

31

32

<figure><img src="image_4.png" /></figure>

* cycle-existence: given a TA $v(\mathcal{A})$, is there at least one run of $v(\mathcal{A})$ with an infinite number of discrete transitions?

33

34

<figure><img src="image_5.png" /></figure>

* EG: given a TA $v(\mathcal{A})$ and a subset $G$ of its locations, is there at least one maximal run of $v(\mathcal{A})$ along which the location always remain in $G$?

35

36

For example, given a PTA $\mathcal{A}$, deadlock-existence-emptiness asks: “does there exist a valuation $v$ of the parameters such that at least one run of $v(\mathcal{A})$ is deadlocked, i. e., has no discrete successor”. In the following, we often abbreviate deadlock-existence-emptiness and cycle-existence-emptiness as ED-emptiness and EC-emptiness, respectively.

37

38

39

40
<figure><img src="image_6.png" /><figcaption>Figure 1 Examples of L/U-PTAs</figcaption></figure>

Note that ED-emptiness is equivalent to AC-universality, where AC-universality asks whether all parameter valuations are such that all runs contain an infinite number of discrete transitions. Conversely, EC-emptiness is equivalent to AD-universality (for all valuations, all runs are deadlocked). In addition, EG-emptiness is also close to both former problems: EG is true if there exists either a finite run with a deadlock staying in $G$, or an infinite run staying in $G$.

### 3 Cycle-Existence-Emptiness

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

**Proof (sketch).** From Lemma 4, this problem is equivalent to testing the TA obtained by valuating upper-bound (resp. lower-bound) parameters with their maximal (resp. minimum) value in *bounds*. See Appendix A for a detailed proof. ◀

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 Figure 1a. 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 $l_0$ is bounded by $p$, and hence finite. However, extending to rational-valued parameters a result from [6], we can still prove decidability.

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

**Proof (sketch).** We show that there exists a rational-valued valuation yielding such an infinite run iff there exists an integer-valued valuation yielding such an infinite run. We can then apply [6, Theorem 8], that proves that the existence of such a valuation is PSPACE-complete. See Appendix B for a detailed proof. ◀

**► Theorem 8.** *The cycle-existence-emptiness problem is 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 7 to conclude that this problem is decidable and PSPACE-complete. ◀

Without surprise, this problem becomes undecidable for general PTAs, even when bounded.

**► Theorem 9.** *The cycle-existence-emptiness problem is undecidable for (bounded) PTAs with 3 clocks and 1 parameter.*
<figure><img src="image_7.png" /><figcaption>(a) Initial gadget</figcaption></figure>

<figure><img src="image_8.png" /><figcaption>(b) Increment gadget</figcaption></figure>

Figure 2 EC-emptiness: gadgets

**Proof.** We reduce from the boundedness problem of a 2-counter machine, which is undecid-
able [13]. 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 $q_i$, increment $C_k$ and go to $q_j$;

- when in state $q_i$, decrement $C_k$ and go to $q_j$;

- when in state $q_i$, if $C_k = 0$ then go to $q_j$, otherwise block.

The machine starts in state $q_0$; by definition, it halts when it reaches a specific state called $q_{halt}$. The boundedness problem for 2-counter machines asks whether the value of the counters remains smaller than some bound, and is undecidable [13].

Given such a machine $\mathcal{M}$, we encode it as a PTA $\mathcal{A}(\mathcal{M})$; our encoding is adapted from an existing encoding of a 2-counter machine, used to (re)prove the EF-emptiness problem for bounded PTAs and then further related results, and found in [4]. We describe it in details, as we will modify it in the subsequent proofs.

Each state $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 Figure 2a (that also blocks the case where $a=0$). Clearly, when in $q_0$ with $x=0$, we have $y=z=1$, which indeed corresponds to counter values 0.

We now present the gadget encoding the increment instruction of $C_1$ in Figure 2b. 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 we use only equalities, there are really only two paths that go through the gadget: one going through $l_{i2}$ and one through $l'_{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 \le 1$, i. e., $ac_2 \ge 0$, which implies that $a \ge 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 \le 1+a$, i. e., $a(c_1+1) \ge 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) \le 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'_{i2}$ if $1-ac_1 \le a+1$, i. e., $a(c_1+1) \ge 0$, and when entering $l'_{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) \le 1 + a$, i. e., $a(c_1 + 1) \le 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 \le 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 Figure 2a 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.

From $q_i$, to encode zero-testing $C_1$ and going to $q_j$, we only need to add a transition from $q_i$ to $q_j$ with guard $y = 1 \land x = 0$.

All those gadgets also work for $C_2$ by swapping $y$ and $z$.

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

Finally, we add a self-loop (with no guard) on the location $q_{halt}$, ensuring that whenever $q_{halt}$ is reachable then there exists an infinite run in the PTA.

We now prove that the value of the counters remains bounded iff there exists a parameter valuation $v$ such that $v(\mathcal{A})$ yields an infinite run. First note that if $a = 0$ the initial gadget cannot be passed, and there is no infinite run. Assume $a > 0$. Consider two cases:

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 there exists an infinite run.

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

a. either the machine reaches $q_{halt}$: in that case, if $c = 0$ and $0 < a \le 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_{halt}$. From there, this run is infinite thanks to the self-loop on $q_{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.

b. or the machine does not halt. Then again, for a sufficiently small parameter valuation (i. e., $a < 1$ if $c = 0$ and $a \le \frac{1}{c}$ otherwise), the machine is properly simulated, and since the machine does not halt, then the run simulating the infinite execution is infinite too. For other values of $a$, the machine will block at some point in an incrementer gadget, because $a$ is not small enough and the guard to $q_j$ cannot be satisfied.

In both subcases, there exist parameter valuations for which there exists an infinite run.

Hence the value of the counters remains bounded iff there exists a parameter valuation $v$ such that $v(\mathcal{A})$ contains an infinite run. ◀

► **Remark.** Throughout this paper, we allow guards and invariants of the form $x \sim \sum_{1 \le j \le M} \beta_j p_j + d$, which is more restrictive than [6] (that allows parametric coefficients different from 0 and 1, as well as diagonal constraints), but more permissive than [2], that only allows a syntax $x \sim p$. In fact, most papers in the literature define their own syntax (see [3] for a survey). We can adapt our proof to fit in the most restrictive syntax ($x \sim 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
<figure><img src="image_9.png" /><figcaption>Figure 3 ED-emptiness for bounded L/U-PTAs: increment gadget</figcaption></figure>

<figure><img src="image_10.png" /><figcaption>(a) Initial gadget</figcaption></figure>

<caption>(b) Final gadget</caption>

<caption>Figure 4 ED-emptiness for bounded L/U-PTAs: initial and final gadgets</caption>

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 Deadlock-Existence-Emptiness

► **Theorem 10.** 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 9, that we transform into an L/U-PTA by replacing any comparison of a clock with $a$ (say $x = a$) into $x \le a^+ \land x \ge a^-$, where $a^-$ (resp. $a^+$) is a lower-bound (resp. upper-bound) parameter. We give the modified increment gadget in Figure 3 (other gadgets are modified in a similar fashion).

We replace the initial gadget (Figure 2a) with the new one in Figure 4a. Before initializing the values of the counters, this gadget first ensures that $a^- \le a^+$.

We also add a new location $q'_{halt}$ reachable from $q_{halt}$ as shown in the final gadget in Figure 4b. 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_{halt}$) to location $q'_{halt}$. That is, it is always possible to reach $q'_{halt}$ from any location without condition, except from $q_{halt}$. From that particular location, $q'_{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 [13]. Let us reason by cases on the valuations of $a^-$ and $a^+$.

1. If $a^- > a^+$, the initial gadget cannot be passed, but thanks to the unguarded transitions to $q'_{halt}$, all runs eventually end in $q'_{halt}$, from which the absence of deadlock is guaranteed by the unguarded self-loop.
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_{halt}$ while the machine does not halt. Let us consider a run in the TA obtained with such a parameter valuation.

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.

b. or this run would block in a gadget (were it not for the unguarded transitions to $q'_{halt}$, due to a guard that cannot be satisfied); in that case, thanks to the unguarded transitions to $q'_{halt}$, this run can go to $q'_{halt}$, from which it is deadlock-free.

c. or this run reaches $q_{halt}$; from there, thanks to the upper transition in Figure 4b, it can reach $q'_{halt}$, from which it is again deadlock-free.

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

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

a. Either the machine does not halt:

i. ...and the counters remain bounded: for some parameter valuations small enough to encode the value of the counters (typically $a^{-} = a^{+} \le \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'_{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 \le 1$ and $a^{-}(c_1+1) > 1$. Hence, the run cannot continue in the encoding, but can reach $q'_{halt}$, from where the run is non-blocking.

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'_{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.

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^{+} \le \frac{1}{c}$, then there exists one run that correctly simulates the machine (beside plenty of runs that will go to $q'_{halt}$ due to the unguarded transitions); this run that correctly simulates the machine eventually reaches $q_{halt}$. From $q_{halt}$, for such valuations, the system is deadlocked: indeed, the transitions from $q_{halt}$ to $q'_{halt}$ can only be taken if $a^{-} < a^{+}$ or $a^{-} = 0$. 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 11.** *The deadlock-existence-emptiness problem is undecidable for open bounded L/U-PTAs, L/U-PTAs, bounded PTAs and PTAs, with 3 clocks and 2 parameters.*
23:10 Liveness in L/U-Parametric Timed Automata

1

**Proof.** Let us consider each formalism:

2

**open bounded L/U-PTAs** In the above construction, we can assume, e. g., $a^- \in (0, 1]$, which does not impact the proof.

3

4

**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'_{halt}$, from which the system is deadlock-free, hence without impacting the spirit of the proof.

6

7

8

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

9

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

10

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$. ▼

11

5 EG-Emptiness

12

13

14

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

15

**► Theorem 12.** *The EG-emptiness problem is decidable for closed bounded L/U-PTAs.*

16

**Symbolic Semantics**

17

Let us first recall the symbolic semantics of PTAs (see, e. g., [10]).

18

19

20

21

22

23

24

We define the *time elapsing* of a constraint *C*, denoted by $C^\rightarrow$, as the constraint over *X* and *P* obtained from *C* by delaying all clocks by an arbitrary amount of time. We define the *past* of *C*, denoted by $C^\leftarrow$, as the constraint over *X* and *P* obtained from *C* by letting time pass backward by an arbitrary amount of time (see [10]). 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).

25

26

27

28

A *parametric zone* is a convex polyhedron over $X \cup P$ in which all constraints on variables are of the form $x \sim \text{plt}$, (parametric rectangular constraints) or $x_i - x_j \sim \text{plt}$ (parametric diagonal constraints), where $x_i \in X$, $x_j \in X$ and $\text{plt}$ is a parametric linear term over $P$, i. e., a linear term without clocks ($\alpha_i = 0$ for all $i$).

29

30

A symbolic state is a pair $s = (l, C)$ where $l \in L$ is a location, and $C$ its associated parametric zone. The initial symbolic state of $\mathcal{A}$ is $s_0 = (l_0, (\{\emptyset\} \wedge I(l_0)))^\rightarrow \wedge I(l_0))$.

31

32

33

34

The symbolic semantics relies on the *Succ* operation. Given a symbolic state $s = (l, C)$ and an edge $e = (l, g, \sigma, R, l')$, *Succ(s, e)* = $(l', C')$, with $C' = (([C \wedge g])_R \wedge I(l'))^\rightarrow \wedge I(l')$. The *Succ* operation is effectively computable, using polyhedra operations: note that the successor of a parametric zone *C* is a parametric zone (see e. g., [10]).

35

36

37

38

A symbolic run of a PTA is an alternating sequence of symbolic states and edges starting from the initial symbolic state, of the form $s_0 \stackrel{e_0}{\Rightarrow} s_1 \stackrel{e_1}{\Rightarrow} \dots \stackrel{e_{m-1}}{\Rightarrow} s_m$, such that for all $i = 0, \dots, m-1$, $e_i \in E$, and $s_{i+1}$ belongs to *Succ(s*, *e*)). In the following, we simply refer to symbolic states belonging to a run of $\mathcal{A}$ as symbolic states of $\mathcal{A}$.

39

We can now come back to the proof of Theorem 12.

40

41

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

42

43

Lemma 4 ensures that the TA $v_{\text{inf/sup}}(\mathcal{A})$, where $v_{\text{inf/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. In $v_{\text{inf/sup}}(\mathcal{A})$, it is decidable

44
to find an infinite path staying in G, or conclude that none exist [1]. If we do find such a path, we can terminate by answering yes to the EG-emptiness problem.

If we do not, then, in $v_{inf/sup}(\mathcal{A})$, all paths staying in G are finite. If we keep only discrete actions and locations, which are in finite number, those paths therefore form a finite tree. Let us recall again that, thanks to Lemma 4, all the discrete paths that stay in G 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 above) for all the paths in the finite tree (not only those that are maximal). Recall that each symbolic state $s$ is a pair $(l, C)$, where $l$ 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: *i*) remove all parts that are in the past of the guard of an outgoing transition in $\mathcal{A}$ (using operation $C^\Upsilon$), and that would satisfy the target location invariant; *ii*) test for emptiness. 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 G for any parameter valuation. ◀

Note that this proof fails when the L/U-PTA is not bounded or closed: consider the L/U-PTA in Figure 1b. As $p$ grows, there are more and more discrete behaviors, but there is no cycle for any parameter valuation. In [6], the authors provide a finite upper bound $N_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_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 Figure 1c. 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 [6] 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}_{\text{bounds}}$ with a single open bound in $\text{bounds}$ or an unbounded L/U-PTA, the EG-emptiness problem becomes undecidable.

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

**Proof (sketch).** The proof reduces from the halting problem of a 2-counter machine. We reuse the encoding of Theorem 10, and modify it so that the 2-counter machine executes in a constant 1-time unit duration. This is achieved by replacing any occurrence of “1” in the encoding with a (new) 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^+$ (by modifying a bit the construction for the zero-test). Then, we add a global invariant $w \le 1$ (where $w$ is a new clock) to all locations. Now that the duration of any gadget is at least $b^-$, we therefore have that, for any valuation $b^- > 0$, the number of operations the machine can perform is finite due to the global invariant $w \le 1$. We assume $a^-, a^+, b^+ \in [0, 1]$ and $b^- \in (0, 1]$.
We prove that the 2-counter machine halts iff the set of valuations satisfying EG(L \ {q'_{halt}}) is not empty. We rule out valuations such that a^{-} > a^{+} or b^{-} > b^{+} by sending them directly to q'_{halt}. For valuations a^{-} < a^{+} or b^{-} < b^{+}, the machine may not be correctly simulated: either the encoding loops, and then blocks after some operations (due to the invariant) which leads to q'_{halt}; or it reaches q_{halt}, and goes to q'_{halt} thanks to an appropriate gadget. Finally, valuations a^{-} = a^{+} and b^{-} = b^{+} > 0 may simulate correctly the machine: if these valuations are not small enough, an increment will block, leading to q'_{halt}; otherwise, for some valuations sufficiently small, and only if the machine halts, then q_{halt} is reached, and from there no transition leads to q'_{halt}, ensuring EG(L \ {q'_{halt}}).

See Appendix C for a detailed proof.

► Remark. The above construction works over 1 time unit (an invariant can be added to $q'_{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 usually 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 [\inf, \sup]$ becomes $\inf \le x \le \sup \wedge p = x$). This may not be true for L/U-PTAs, as such a construction requires to compare the clock and the parameter using an equality. In addition, our proof for unbounded L/U-PTAs uses one parameter less than for open bounded L/U-PTAs.

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

**Proof (sketch).** We 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 13; however, we must use a different PTA encoding (the encoding used in the proof of Theorem 13 does not work for unbounded L/U-PTAs, as it strongly relies on the fact that $b^{-}$ be strictly positive). Instead, we propose an encoding inspired by that of a 2-counter machine proposed in [5] to prove the undecidability of the EF-emptiness problem for PTAs with a single integer-valued parameter (that can also be rational-valued). We modify the encoding of [5] to obtain an L/U-PTA, 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 10 and 13). Then, we add a global invariant $w \le b^{+}$ (where $w$ is a fresh clock never reset, and $b^{+}$ a fresh upper-bound parameter), to ensure that, for any valuation of $b^{+} > 0$, the number of operations the machine can perform is finite (which requires some modifications of the gadgets to ensure that they require at least 1 time unit). The proof then follows a reasoning similar to that of Theorem 13.

See Appendix D for a detailed proof.

► Remark. 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).

# 6 Conclusion

Despite the vast number of undecidability results linked to the formalism of parametric timed automata, and to which we also contribute here, we 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 consistently decidable (with bounded domains or not). And finally, if we consider only finite maximal paths (existence of deadlocks), then we have proved that the problem becomes consistently undecidable.

Future work includes extending the EG decidability result to shapes other than hy-
perrectangles and studying actual synthesis. 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).

**Acknowledgements.** The authors thank Olivier H. Roux for fruitful discussions on the topic of parametric timed automata.

References

1 Rajeev Alur and David L. Dill. A theory of timed automata. *Theoretical Computer Science*, 126(2):183-235, 1994.

2 Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi. Parametric real-time reasoning. In *STOC*, pages 592–601. ACM, 1993.

3 Étienne André. What's decidable about parametric timed automata? In *FTSCS*, volume 596 of *Communications in Computer and Information Science*, pages 1–17. Springer, 2015.

4 Étienne André, Didier Lime, and Olivier H. Roux. Decision problems for parametric timed automata. Technical report, 2016. URL: www.lipn13.fr/t/PTAs.pdf.

5 Nikola Beneš, Peter Bezděk, Kim G. Larsen, and Jiří Srba. Language emptiness of continuous-time parametric timed automata. In *ICALP, Part II*, volume 9135 of *LNCS*, pages 69–81. Springer, 2015.

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

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

8 Laurent Doyen. Robust parametric reachability for timed automata. *Information Processing Letters*, 102(5):208–213, 2007.

9 Thomas Hune, Judi Romijn, Mariëlle Stoelinga, and Frits W. Vaandrager. Linear parametric model checking of timed automata. *JLAP*, 52-53:183–220, 2002.

10 Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. Integer parameter synthesis for timed automata. *IEEE TSE*, 41(5):445–461, 2015.

11 Leslie Lamport. Proving the correctness of multiprocess programs. *IEEE TSE*, 3(2):125–143, 1977.

12 Joseph S. Miller. Decidability and complexity results for timed automata and semi-linear hybrid automata. In *HSCC*, volume 1790 of LNCS, pages 296–309. Springer, 2000.

13 Marvin L. Minsky. *Computation: finite and infinite machines*. Prentice-Hall, Inc., 1967.
A Proof of Theorem 6

**Theorem 6 (recalled).** *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 4), 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}_{\text{bounds}}$ be a closed bounded L/U-PTA. Let $v_{\text{inf/sup}}$ be the valuation such that, for each lower-bound parameter $p^-$, $v_{\text{inf/sup}}(p^-) = \text{inf}(p^-, \text{bounds})$ and, for each upper-bound parameter $p^+$, $v_{\text{inf/sup}}(p^+) = \text{sup}(p^+, \text{bounds})$.

1. If $v_{\text{inf/sup}}(\mathcal{A})$ contains an infinite run (which can be checked in PSPACE [1]), then since $\mathcal{A}_{\text{bounds}}$ is closed, $v_{\text{inf/sup}}$ belongs to $\text{bounds}$, and hence the set of parameter valuations that yield an infinite run is not empty.

2. On the contrary, if $v_{\text{inf/sup}}(\mathcal{A})$ contains no infinite run, then from the monotonicity property of L/U-PTAs (Lemma 4), no other valuation in $\text{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.

B Proof of Lemma 7

**Theorem 7 (recalled).** *Given an L/U-PTA $\mathcal{A}$ and a subset of its locations $G$, the problem of the existence of at least one parameter valuation $v$ such that $v(\mathcal{A})$ has a run passing infinitely often through $G$ 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.

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

23. $\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 $G$. Let $v'$ be the integer parameter valuation obtained from $v$ as follows:

$$v'(p) = \begin{cases} v(p) & \text{if } v(p) \in \mathbb{N} \\ [v(p)] & \text{if } p \text{ is an upper-bound parameter} \\ [v(p)] & \text{if } p \text{ is a lower-bound parameter} \end{cases}$$

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

Now, in [6, 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 $G$ is PSPACE-complete. This concludes the proof.
<figure><img src="image_11.png" /><figcaption>Figure 5 EG-emptiness for bounded L/U-PTAs: increment gadget</figcaption></figure>

1

C Proof of Theorem 13

2

Theorem 13 (recalled). *The EG-emptiness problem is undecidable for open bounded L/U-PTAs, with 4 clocks and 4 parameters.*

3

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

4

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

5

6

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

7

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 Figure 5. 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.

9

10

11

12

13

14

15

16

2. We modify the zero-test so that its duration is within $[b^-, b^+]$, as in Figure 6: only the first transition encodes the zero-test, the two other transitions 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_{i1}$ and waiting enough time to take the transition to $l_{i2}$ (i. e., a duration in $ac_2$) we have: $z = b$ and $x = y = ac_2$. After reaching $l_{i2}$ and waiting enough time to take the transition to $q_j$ (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.

18

19

20

21

22

23

24

25

26

27

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

28

29

30

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 \le 1$.

31

32

Then, before starting the 2-counter machine encoding, we add an initial gadget given in Figure 7. This gadget constrains $a^- \le a^+$, $b^- \le b^+$, and is such that when leaving the

33

34
<figure><img src="image_12.png" /><figcaption>Figure 6 EG-emptiness for bounded L/U-PTAs: zero-test gadget</figcaption></figure>

<figure><img src="image_13.png" /><figcaption>Figure 7 EG-emptiness for bounded L/U-PTAs: initial gadget</figcaption></figure>

gadget then $y, z \in [b^{-} \le 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'_{halt}$ location (without any invariant, i. e., not requiring $w \le 1$), with two transitions from $q_{halt}$ as depicted in Figure 8. We then add a transition (with no guard) from any location of the encoding (except $q_{halt}$) to $q'_{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'_{halt}$. (If the value is small enough, the system can either lead to $q'_{halt}$ or continue in the 2-counter machine encoding.) We also add a transition to $q'_{halt}$ (with no guard) from all locations in the initial gadget in Figure 7.

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 EG($L \setminus \{q'_{halt}\}$) is not empty.

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

2. If $a^{-} < a^{+}$ and $b^{-} \le b^{+}$, then the machine may not be correctly simulated: a given run will either reach $q_{halt}$, in which case it will also reach $q'_{halt}$ (as the guard from $q_{halt}$ to $q'_{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 \le 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'_{halt}$, thanks to the unguarded transitions from any location to $q'_{halt}$. Hence if $a^{-} < a^{+}$, EG($L \setminus \{q'_{halt}\}$) does not hold.

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

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

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 \le 1$, and the run will end in $q'_{halt}$. Hence if the 2-counter machine does not halt, EG($L \setminus \{q'_{halt}\}$) does not hold.

<figure><img src="image_14.png" /><figcaption>Figure 8 EG-emptiness for bounded L/U-PTAs: final gadget</figcaption></figure>
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^+ \le \frac{b^-}{c}$ and $b^- = b^+ \le \frac{1}{m}$, then there exists one run that correctly simulates the machine (beside plenty of runs that will go to $q'_{halt}$ due to the unguarded transitions); this run that correctly simulates the machine eventually reaches $q_{halt}$. From $q_{halt}$, for such valuations, the system is deadlocked: indeed, the transitions from $q_{halt}$ to $q'_{halt}$ can only be taken if $a^- < a^+$ or $b^- < b^+$. Hence $\text{EG}(L \setminus \{q'_{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 $\text{EG}(L \setminus \{q'_{halt}\})$ holds.

Hence the 2-counter machine halts iff the set of valuations for which $\text{EG}(L \setminus \{q'_{halt}\})$ holds is not empty. ◀

D Proof of Theorem 14

**Theorem 14 (recalled).** 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 13; however, we must use a different PTA encoding (the encoding used in the proof of Theorem 13 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 [5] 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 [5], the proof also works identically with a rational-valued parameter). The model of the 2-counter machine slightly differs from that considered in the rest of this paper. Two different instructions are considered:

- when in state $q_i$, increment $C_k$ and go to $q_j$;

- when in state $q_i$, if $C_k = 0$ then go to $q_k$, otherwise decrement $C_k$ and go to $q_j$;

Starting from the initial configuration $(q_0, C_1 = 0, C_2 = 0)$ the machine either reaches $q_{halt}$ and halts, or loops forever. Knowing whether the machine halts is undecidable [13].

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 10 and 13).

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 \le 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 Figure 9 (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]$.

The test and decrement gadget is similar, and given in Figure 10. We performed a slight modification to the zero-test of [5], that was executed in 0-time; we require in our
<figure><img src="image_15.png" /><figcaption>Figure 9 EG-emptiness for L/U-PTAs: increment gadget</figcaption></figure>

<figure><img src="image_16.png" /><figcaption>Figure 10 EG-emptiness for L/U-PTAs: test and decrement gadget</figcaption></figure>

construction that each gadget takes at least one time unit. Hence, we rewrote it in Figure 10 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^{-} \le a^{+}$ (in the spirit of the same operation in the proof of Theorem 13): 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''}$, 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''}$, 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 Figure 11, constraining $a^{-} \le a^{+}$ and $b^{+} > 0$, and resetting all clocks.

In addition, just as in Theorem 13, we add unguarded transitions from any location

<figure><img src="image_17.png" /><figcaption>Figure 11 EG-emptiness for L/U-PTAs: initial gadget</figcaption></figure>
<figure><img src="image_18.png" /><figcaption>Figure 12 EG-emptiness for L/U-PTAs: final gadget</figcaption></figure>

(including that of the initial gadget, but excluding $q_{halt}$) to a new location $q'_{halt}$. We also add two transitions from $q_{halt}$ to $q'_{halt}$ given in the final gadget in Figure 12.

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

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

2. If $a^{-} < a^{+}$ and $b^{+} > 0$, then the machine may not be correctly simulated: a given run will either reach $q_{halt}$, in which case it will also reach $q'_{halt}$ (as the guard from $q_{halt}$ to $q'_{halt}$ in Figure 12 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 \le b^{+}$ will eventually block a transition after at most $b^{+}$ steps. When being blocked, a run has no other option than going to $q'_{halt}$, because of the unguarded transitions from any location to $q'_{halt}$. Hence if $a^{-} < a^{+}$ and $b^{+} > 0$, $EG(L \setminus \{q'_{halt}\})$ does not hold.

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

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 \le b^{+}$, and the run will end in $q'_{halt}$ because of the unguarded transitions from any location to $q'_{halt}$. Hence if the 2-counter machine does not halt, $EG(L \setminus \{q'_{halt}\})$ does not hold.

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^{+} \le c$ and sufficiently large valuations of $b^{+}$ (typically $b^{+} \ge 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_{halt}$. From $q_{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'_{halt}$, i. e., for which $EG(L \setminus \{q'_{halt}\})$ holds.

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