On the expressive power of invariants in parametric timed automata

TL;DR

This paper introduces a syntactic restriction on parametric timed automata that preserves expressiveness while enabling decidable parameter synthesis, offering a practical trade-off between complexity and expressiveness.

Contribution

It proposes a new subclass of PTAs with only invariants, allowing exact parameter synthesis under certain constraints, balancing expressiveness and decidability.

Findings

Decidability of reachability in the new formalism.

Exact synthesis of parameter valuations for reachability.

Applicability demonstrated through a case study.

Abstract

The verification of systems combining hard timing constraints with concurrency is challenging. This challenge becomes even harder when some timing constants are missing or unknown. Parametric timed formalisms, such as parametric timed automata (PTAs), tackle the synthesis of such timing constants (seen as parameters) for which a property holds. Such formalisms are highly expressive, but also undecidable, and few decidable subclasses were proposed. We propose here a syntactic restriction on PTAs consisting in removing guards (constraints on transitions) to keep only invariants (constraints on locations). While this restriction preserves the expressiveness of PTAs (and therefore their undecidability), an additional restriction on the type of constraints allows to not only prove decidability, but also to perform the exact synthesis of parameter valuations satisfying reachability. This formalism, that seems trivial at first sight as it benefits from the decidability of the reachability problem with a better complexity than Timed Automata (TAs), suffers from the undecidability of the whole TCTL logic that TAs, on the contrary enjoy. We believe our formalism allows for an interesting trade-off between decidability and practical expressiveness and is therefore promising. We show its applicability in a small case study.

Equations

$$\phi ::=\top |\text{ap}|\neg \phi |\phi \wedge \phi |\mathsf{E}\phi {\mathsf{U}}_{\bowtie c}\phi |\mathsf{A}\phi {\mathsf{U}}_{\bowtie c}\phi$$

$${\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{s}}\geq 0\land{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{v}}\geq 0\land{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{send}}>0\land{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{rced}}>0.$$

Full text

linecolor=red,backgroundcolor=red!25,bordercolor=red]Instructions: ICECCS 10 pages double column, including references and appendix

linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: hello linecolor=purple,backgroundcolor=purple!25,bordercolor=purple]DL: hello linecolor=orange,backgroundcolor=orange!25,bordercolor=orange]$\mathbb{MR}$: hello

I Introduction

The verification of systems combining hard timing constraints with concurrency is challenging. This challenge becomes even harder when some timing constants are missing or unknown. Parametric timed formalisms tackle the synthesis of such timing constants (seen as parameters) for which a property holds. A well-known such formalism is parametric timed automata [AHV93], a formalism extending finite-state automata with clocks [AD94], that can be compared to either integer constants or to integer-valued or real-valued parameters along guards (over transitions) or in invariants (in locations). Such formalisms are highly expressive, but also highly undecidable, and only a few decidable subclasses were proposed.

In the PTA literature, the main problem studied is $\mathsf{EF}$-emptiness (“is the set of valuations for which a given location is reachable for at least one run empty?”): it is “robustly” undecidable in the sense that, even when varying the setting, undecidability is preserved. For example, $\mathsf{EF}$-emptiness is undecidable even for a single bounded parameter [Mil00], even for a single rational-valued or integer-valued parameter [Ben+15], even with only one clock compared to parameters [Mil00], or with strict constraints only [Doy07] (see [And19] for a survey). Decidability can be obtained using two main directions.

First, reducing the number of clocks may lead to decidability: for example, decidability is ensured in some restrictive settings such as over discrete time with a single parametric clock (i. e., compared to parameters in at least one guard) [AHV93], or over discrete or dense time with one parametric clock and arbitrarily many non-parametric clocks [BO14, Ben+15], or over discrete time with two parametric clocks and a single parameter [BO14]. But the practical power of these restrictive settings remains unclear.

Second, restricting the syntax may also lead to decidability, notably on two main subclasses: in [Hun+02], L/U-PTAs are proposed as a subclass where parameters are partitioned into upper-bound parameters (only compared to clocks as upper-bounds, i. e., of the form $x>p$ or $x\geq p$, where $x$ is a clock and $p$ a parameterlinecolor=purple,backgroundcolor=purple!25,bordercolor=purple]DL: pas clair: de quel côté on met paramètres et horloges? je mettrais directement “$x<p$ or $x\leq p$ where x is a clock and p a parameter”linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: fixed) and lower-bound parameters. While L/U-PTAs benefit from the decidability of $\mathsf{EF}$-emptiness [JLR15, BL09], $\mathsf{AF}$-emptiness (“is the set of valuations for which a given location is reachable for all runs empty?”) is undecidable [JLR15]; even more annoying, it is impossible to achieve exact synthesis, even for $\mathsf{EF}$: that is, it is not possible in general to compute the set of parameter valuations for which a given location is reachable. A second restriction of the syntax is proposed in [ALR19]: in reset-PTAs, whenever a clock is compared to a parameter, all clocks must be reset (possibly to parameters, which extends the original PTA syntax). While exact synthesis over bounded rational-valued parameters can be achieved for $\mathsf{EF}$, resetting all clocks as soon as one clock is compared to a parameter is a strong practical restriction, and is dedicated to systems that have some cyclic, repetitive behavior.linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: OK? Délicat de critiquer trop frontalement notre précédent papier mais… linecolor=orange,backgroundcolor=orange!25,bordercolor=orange]$\mathbb{MR}$: ça va c’est cool quand meme linecolor=purple,backgroundcolor=purple!25,bordercolor=purple]DL: Nice.

Contribution

In this work, we propose an original subclass of parametric timed automata, with interesting practical results. We restrict the expressive power by disallowing guards in the model, therefore leaving the model with only invariants.

On the one hand, we show that this model of PTAs with only invariants (PTAsI) is at least as expressive as the original PTAs, and therefore inherits its notorious undecidability results.

On the other hand, by restraining the shape of the constraints in these invariants, giving PTAs with only invariants and upper-bound constraints (PTAs${}_{I}^{U}$), we get decidability results independently of the number of clocks or parameters used. In addition, we show that we can synthesize the exact set of parameters for which reachability ($\mathsf{EF}$) properties hold. This result is particularly welcome, as existing classes for which decidability of the emptiness problems hold does usually not guarantee the possibility to perform synthesis: the best-known existing subclass of PTAs, i. e., L/U-PTAs, benefit from decidability results [Hun+02, BL09] but synthesis cannot be achieved, even over integer-valued parameters [JLR15].

Our formalism of PTAs${}_{I}^{U}$ is the first of its kind to allow for exact synthesis over unbounded, rational-valued parameters (in contrast to [Hun+02, BL09, ALR19]) without imposing conditions on the number of clocks or parameters (in contrast to [BO14, Ben+15]), nor imposing frequent resets (in contrast to [ALR19]). This makes this formalism promising, together with a still interesting expressive power. In fact, we show that for more complex properties (e. g., nested TCTL formulas), PTAs${}_{I}^{U}$ become undecidable, which shows that our formalism is far from featuring a trivial expressiveness.linecolor=orange,backgroundcolor=orange!25,bordercolor=orange]$\mathbb{MR}$: super We also exemplify our formalism on a case study, where we model a data streaming protocol using PTAs${}_{I}^{U}$.

Outline

Section II recalls the necessary preliminaries, introduces the class of PTAs without guards (PTAsI) and the problems of interest. Section III proves that reachability is undecidable for PTAI. Section IV introduces an additional restriction (PTAs${}_{I}^{U}$), and proves decidability of the emptiness problems of reachability, together with the possibility to perform synthesis. In contrast, we show that TCTL-emptiness is undecidable for PTAs${}_{I}^{U}$, making it an expressive formalism at the border between decidability and undecidability. Section V exemplifies our formalism on a case study. Section VI concludes the paper and proposes some perspectives.

II Preliminaries

II-A Clocks, parameters and parametric clock constraints

We assume a set $\mathbb{X}=\{x_{1},\dots,x_{H}\}$ of clocks, i. e., real-valued variables that evolve at the same rate. A clock valuation is a functionlinecolor=purple,backgroundcolor=purple!25,bordercolor=purple]DL: ça ne semble pas très bien marcher l’espace initial dans LongVersionlinecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: en fait longeversion + commentaires c’est moche, mais sans les commentaires, tout va bien. Bon, j’ai simplifié puisque de toute façon on ne fait que du long ici $w:\mathbb{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 assigning [math] to all clocks. Given $d\in{\mathbb{R}}_{+}$, $w+d$ denotes the valuation s.t. $(w+d)(x)=w(x)+d$, for all $x\in\mathbb{X}$. Given $R\subseteq\mathbb{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 $\mathbb{P}=\{p_{1},\dots,p_{M}\}$ of parameters, i. e., unknown constants. A parameter valuation $v$ is a function $v:\mathbb{P}\to{\mathbb{Q}}_{+}$.

We assume ${\bowtie}\in\{<,\leq,=,\geq,>\}$ and ${\triangleleft}\in\{<,\leq\}$. A parametric clock constraint $\mathit{pcc}$ is a constraint over $\mathbb{X}\cup\mathbb{P}$ defined by a set of inequalities of the form $x\bowtie\sum_{1\leq i\leq M}\alpha_{i}p_{i}+d$, with $\alpha_{i}\in\{0,1\}$ and $d\in{\mathbb{Z}}$. Given $\mathit{pcc}$, we write $w\models v(\mathit{pcc})$ if the expression obtained by replacing each $x$ with $w(x)$ and each $p$ with $v(p)$ in $\mathit{pcc}$ evaluates to true.

II-B Parametric timed automata

Let $\mathit{AP}$ be a set of atomic propositions. We first recall PTAs [AHV93].

Definition 1**.**

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

• •

$\Sigma$* is a finite set of actions,*

• •

$L$* is a finite set of locations,*

• •

$\mathbf{L}$* is a label function $\mathbf{L}:L\to 2^{\mathit{AP}}$,*

• •

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

• •

$\mathbb{X}$* is a finite set of clocks,*

• •

$\mathbb{P}$* is a finite set of parameters, *

• •

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

• •

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

Given a parameter valuation $v$, we denote by $v(\mathcal{A})$ the non-parametric structure where all occurrences of a parameter $p_{i}$ have been replaced by $v(p_{i})$. We denote as a timed automaton any structure $v(\mathcal{A})$.111Technically and strictly speaking, we should use a rescaling of the constants to avoid comparisons of clocks with rationals: by multiplying all constants in $v(\mathcal{A})$ by the least common multiple of their denominators, we obtain an equivalent (integer-valued) TA, as defined in [AD94]. A bounded PTA is a PTA with a bounded parameter domain that assigns to each parameter a minimum integer bound and a maximum integer bound. That is, each parameter $p_{i}$ ranges in an interval $[a_{i},b_{i}]$, with $a_{i},b_{i}\in{\mathbb{N}}$. Hence, a bounded parameter domain is a hyperrectangle of dimension $M$.

Let us first recall the concrete semantics of TAs.

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

Given a PTA $\mathcal{A}=(\Sigma,L,\mathbf{L},\ell_{0},\mathbb{X},\mathbb{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\models v(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}}{{\mapsto}}(\ell^{\prime},w^{\prime})$, if $(\ell,w),(\ell^{\prime},w^{\prime})\in S$, there exists $e=(\ell,g,a,R,\ell^{\prime})\in E$, $w^{\prime}=[w]_{R}$, and $w\models v(g)$. *

• –

delay transitions: $(\ell,w)\stackrel{{\scriptstyle d}}{{\mapsto}}(\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}}{{\longrightarrow}}(\ell^{\prime},w^{\prime})$ for a combination of a delay and discrete transition where $((\ell,w),e,(\ell^{\prime},w^{\prime}))\in{\rightarrow}$ if $\exists d,w^{\prime\prime}:(\ell,w)\stackrel{{\scriptstyle d}}{{\mapsto}}(\ell,w^{\prime\prime})\stackrel{{\scriptstyle e}}{{\mapsto}}(\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 run of $v(\mathcal{A})$ is a possibly infinite alternating sequence of states of $v(\mathcal{A})$ and edges starting from the initial state $s_{0}$ of the form $s_{0}\stackrel{{\scriptstyle e_{0}}}{{\longrightarrow}}s_{1}\stackrel{{\scriptstyle e_{1}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle e_{m-1}}}{{\longrightarrow}}s_{m}\stackrel{{\scriptstyle e_{m}}}{{\longrightarrow}}\cdots$, such that for all $i=0,1,\dots$, $e_{i}\in E$, and $(s_{i},e_{i},s_{i+1})\in{\rightarrow}$. Given a state $s=(\ell,w)$, we say that $s$ is reachable if $s$ appears in a run of $v(\mathcal{A})$, or simply that $\ell$ is reachable in $v(\mathcal{A})$, if there exists a state $(\ell,w)$ that is reachable. By extension, we say that a label $\mathit{lb}$ is reachable in $v(\mathcal{A})$ if there exists a state $(\ell,w)$ that is reachable such that $\mathit{lb}\in\mathbf{L}(\ell)$.

Given a parameter valuation $v$ and a run of $v(\mathcal{A})$ $\rho=(\ell_{0},w_{0})\stackrel{{\scriptstyle e_{0}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle e_{i-1}}}{{\longrightarrow}}(\ell_{i},w_{i})\stackrel{{\scriptstyle e_{i}}}{{\longrightarrow}}(\ell,w)$ we define the length of a run as the number of edges in $\rho$.linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: j’ai viré la notation $|\rho|$, non utilisée

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. Given a run $\rho$ of $v(\mathcal{A})$, $\mathsf{time}(\rho)$ gives the total sum of the delays $d$ along $\rho$.

II-C A new syntactic restriction

We now introduce the first main restriction of our formalism, that consists in removing guards from PTAs.

Definition 3**.**

A PTA with only invariants (PTAI)* is a PTA where, in each transition, $g$ is always true, i. e., is an empty set of inequalities.*

II-D Timed CTL

TCTL [ACD93] is the quantitative extension of CTL where temporal modalities are augmented with constraints on duration. Formulae are interpreted over TTS.

Given $\textit{ap}\in\mathit{AP}$ and $c\in{\mathbb{N}}$, a TCTL formula is given by the following grammar:

[TABLE]

$\mathsf{A}$ reads “always”, $\mathsf{E}$ reads “exists”, and $\mathsf{U}$ reads “until”.

Standard abbreviations include Boolean operators as well as $\mathsf{EF}_{\bowtie c}\varphi$ for $\mathsf{E}\top\mathsf{U}_{\bowtie c}\varphi$, $\mathsf{AF}_{\bowtie c}\varphi$ for $\mathsf{A}\top\mathsf{U}_{\bowtie c}\varphi$ and $\mathsf{EG}_{\bowtie c}\varphi$ for $\neg\mathsf{AF}_{\bowtie c}\neg\varphi$. ($\mathsf{F}$ reads “eventually” while $\mathsf{G}$ reads “globally”.)

Definition 4** (Semantics of TCTL).**

Given a TA $v(\mathcal{A})$, the following clauses define when a state $s_{i}$ of its TTS $(S,s_{0},{\rightarrow})$ satisfies a TCTL formula $\varphi$, denoted by $s_{i}\models\varphi$, by induction over the structure of $\varphi$ (semantics of Boolean operators is omitted):

$s_{i}\models\mathsf{E}\varphi\mathsf{U}_{\bowtie c}\Psi$* if there is a maximal run $\rho$ in $v(\mathcal{A})$ with $\sigma=s_{i}\stackrel{{\scriptstyle e_{i}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle e_{j-1}}}{{\longrightarrow}}s_{j}$ ($i<j$) a prefix of $\rho$ *s.t. $s_{j}\models\Psi$, $\mathsf{time}(\sigma)\bowtie c$, and if $\forall k$ s.t. $i\leq k<j$, $s_{k}\models\varphi$, and 2. 2.

$s_{i}\models\mathsf{A}\varphi\mathsf{U}_{\bowtie c}\Psi$* if for each maximal run $\rho$ in $v(\mathcal{A})$ there exists $\sigma=s_{i}\stackrel{{\scriptstyle e_{i}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle e_{j-1}}}{{\longrightarrow}}s_{j}$ ($i<j$) a prefix of $\rho$ *s.t. $s_{j}\models\Psi$, $\mathsf{time}(\sigma)\bowtie c$, and if $\forall k$ s.t. $i\leq k<j$, $s_{k}\models\varphi$.

In $\mathsf{E}\varphi\mathsf{U}_{\bowtie c}\Psi$ the classical until is extended by requiring that $\varphi$ be satisfied within a duration (from the current state) verifying the constraint “$\bowtie c$”. Given $v$, a PTA${}_{I}^{U}$ $\mathcal{A}$ and a TCTL formula $\varphi$, we write $v(\mathcal{A})\models\varphi$ when $s_{0}\models\varphi$.

We define flat TCTL as the subset of TCTL where, in $\mathsf{E}\varphi\mathsf{U}_{\bowtie c}\varphi$ and $\mathsf{A}\varphi\mathsf{U}_{\bowtie c}\varphi$, $\varphi$ must be a formula of propositional logic (a Boolean combination of atomic propositions).

II-E Problems

In this paper, we address the following problems:

**TCTL-emptiness problem:

**Input: a PTAI $\mathcal{A}$ and a TCTL formula $\varphi$

Problem: is the set of valuations $v$ such that $v(\mathcal{A})\models\varphi$ empty?

**TCTL-synthesis problem:

**Input: a PTAI $\mathcal{A}$ and a TCTL formula $\varphi$

Problem: synthesize the set of valuations $v$ such that $v(\mathcal{A})\models\varphi$.

We will focus notably on the TCTL formula “$\mathsf{EF}$” expressing reachability [AD94]. That is, $\mathsf{EF}$-emptiness asks whether the set of parameter locations for which a given location is reachable for at least one run is empty or not. Similarly, $\mathsf{EF}$-synthesis asks to synthesize these valuations.

III The power of invariants in PTAs

In this section, we show that the expressive power of invariants in PTAs is surprisingly high: in fact, we show that a PTA with guards but without invariants can be transformed to an equivalent PTAI. As most undecidability results for PTAs hold even without invariants, our transformation shows that PTAI are (at least) as expressive as PTAs—and therefore as undecidable too. Notably, the simplest problem for PTAs ($\mathsf{EF}$-emptiness) is undecidable for PTAsI.

III-A Transforming guards into invariants

Let us describe our transformation from a PTA $\mathcal{A}$ without invariants to a PTAI $T(\mathcal{A})$. For each edge $e=(\ell_{1},g,a,R,\ell_{2})$ of $\mathcal{A}$, we add in $T(\mathcal{A})$ a new location $\ell_{1}^{\prime}$ with invariant $I(\ell_{1}^{\prime})=g$ and replace $e$ with a transition that is always true from $\ell_{1}$ to $\ell_{1}^{\prime}$ with action $a$ and no reset: $e^{\prime}=(\ell_{1},\text{true},a,\emptyset,\ell_{1}^{\prime})$. Then we add a unique transition from $\ell_{1}^{\prime}$ to $\ell_{2}$ that is always true, without action and with the original resets $R$ of $e$: $e^{\prime\prime}=(\ell_{1}^{\prime},\text{true},\epsilon,R,\ell_{2})$ ($\epsilon$ denotes the silent action; note that actions do not matter much in our setting anyway as we are concerned with reachability properties).

Example 1**.**

*An example of this transformation is given in Fig. 1. The transition (say $e$) from $\ell_{1}$ to $\ell_{2}$ in Fig. 1(a) is translated into

1. a new transition from $\ell_{1}$ to a new location $\ell_{1}^{\prime}$ with as invariant the guard of the original transition $e$, i. e., $x\leq p$, and

2. a new transition from $\ell_{1}^{\prime}$ to $\ell_{2}$ with the same reset as the one of the original transition $e$, i. e., $x:=0$.

This translation is exemplified in Fig. 1(b).*

The guard on the transition from $\ell_{2}$ to $\ell_{3}$ is translated similarly.

III-B Characterization of the transformation

We show that, for any run of $v(\mathcal{A})$, there exists in $v(T(\mathcal{A}))$ a run twice as long, whose states of index $2\times i$ are identical to states of index $i$ of the original run, for each $i$ between 0 and the length of the run minus 1.

Lemma 1**.**

Let $\mathcal{A}$ be a PTA without invariant, and $v$ a parameter valuation. There is a run $\rho=(\ell_{0},w_{0})\stackrel{{\scriptstyle e_{0}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle e_{i-1}}}{{\longrightarrow}}(\ell_{i},w_{i})\stackrel{{\scriptstyle e_{i}}}{{\longrightarrow}}(\ell,w)\cdots$ in $v(\mathcal{A})$ iff there is a run $\rho^{\prime}=(\ell_{0},w_{0})\stackrel{{\scriptstyle e_{0}^{\prime}}}{{\longrightarrow}}(\ell_{0}^{\prime},w_{0}^{\prime})\stackrel{{\scriptstyle e_{0}^{\prime\prime}}}{{\longrightarrow}}\cdots\stackrel{{\scriptstyle e_{i-1}^{\prime\prime}}}{{\longrightarrow}}(\ell_{i},w_{i})\stackrel{{\scriptstyle e_{i}^{\prime}}}{{\longrightarrow}}(\ell_{i}^{\prime},w_{i}^{\prime})\stackrel{{\scriptstyle e_{i}^{\prime\prime}}}{{\longrightarrow}}(\ell,w)\cdots$ in $v(T(\mathcal{A}))$.

Proof.

Let $\rho$ be a run of $v(\mathcal{A})$ ending in a concrete state $(\ell,w)$. We build by induction on $n$, a run $\rho^{\prime}$ in $v(T(\mathcal{A}))$ of length $2n$ taking the same sequence of edges as $\rho$ w.r.t. our transformation and ending in the same concrete state222Note that the fact that the length is even is a consequence of the construction: with two edges, first from $\ell$ to $\ell^{\prime\prime}$ and the second from $\ell^{\prime\prime}$ to $\ell^{\prime}$, if the former can be taken then $I(\ell^{\prime\prime})$ is satisfied, and the run cannot stay forever in $\ell^{\prime\prime}$ because of $I(\ell^{\prime\prime})$ and is forced to take the latter to $\ell^{\prime}$..

If $n=0$, then $\rho^{\prime}$ consists only of the initial location of $T(\mathcal{A})$ which has no invariant, so we can stay there forever as in the initial location of $\mathcal{A}$. So any run of length 0 of $v(T(\mathcal{A}))$ is a run of $v(\mathcal{A})$ and conversely.

Suppose now that we have built $\rho^{\prime}$ for size $n$ and consider a run $\rho$ with $n+1$ edges. Then $\rho$ consists of a run $\rho_{1}$, ending in $(\ell_{1},w_{1})$ with $n$ edges followed by a delay $d$ and finally a discrete transition along the edge $e$ to the concrete state $(\ell_{2},w_{2})$. From the induction hypothesis, we can build an equivalent run $\rho^{\prime}_{1}$ in $T(\mathcal{A})$ of length $2n$ ending in $(\ell_{1},w_{1})$, Let $w^{\prime}_{1}$ be the clock valuation obtained from $w_{1}$ after the delay $d$. By construction, if constraints defined by the guard of $e$ are satisfied by $w^{\prime}_{1}$ then in $\rho^{\prime}_{1}$, we can take the transition $e^{\prime}$ without guards from $\ell_{1}$ to $\ell_{1}^{\prime}$ as $w^{\prime}_{1}\models v(I(\ell_{1}^{\prime}))$. Once in $\ell_{1}^{\prime}$, we cannot stay forever because of $I(\ell_{1}^{\prime})$. We can also immediately in a [math]-delay take the transition $e^{\prime\prime}$ from $\ell_{1}^{\prime}$ to $\ell_{2}$ and clocks in $\mathbb{X}$ are reset so $w_{2}=[w^{\prime}_{1}]_{R}$, and we obtain a run of length $2(n+1)$ in $v(T(\mathcal{A}))$ ending in $(\ell_{2},w_{2})$.

For the other direction, starting from a run in $T(\mathcal{A})$, the initial step of the induction is similar. Let $\rho^{\prime}$ be a run of $v(T(\mathcal{A}))$ of length $2(n+1)$ ending in a concrete state $(\ell_{2},w_{2})$. Then $\rho^{\prime}$ consists of a run $\rho^{\prime}_{1}$, ending in $(\ell_{1},w_{1})$ with $2n$ edges followed by a first delay $d_{1}$, then a discrete transition $e^{\prime}$ to $\ell_{1}^{\prime}$, and a possible delay $d_{2}$ and finally a discrete transition $e^{\prime\prime}$ to $\ell_{2}$. Let $e$ be the edge in $\mathcal{A}$ corresponding to $e^{\prime},e^{\prime\prime}$ w.r.t. our construction of $T(\mathcal{A})$, with guard $g=I(\ell_{1}^{\prime})$ and the same resets as in $e^{\prime\prime}$. Suppose now that we have built by induction hypothesis $\rho$ in $v(\mathcal{A})$ for size $n$ equivalent to a run $\rho^{\prime}_{1}$ in $v(T(\mathcal{A}))$ ending in $(\ell_{1},w_{1})$, Let $w^{\prime}_{1}$ be the clock valuation obtained after the delay $d_{1}$ from $w_{1}$ and $w^{\prime\prime}_{1}$ after the delay $d_{2}$ from $w^{\prime}_{1}$. By construction, if constraints defined by $I(\ell_{1}^{\prime})$ are satisfied by $w^{\prime}_{1}$ then $w^{\prime}_{1}\models v(g)$. The first transition $e^{\prime}$ in $v(T(\mathcal{A}))$ to $\ell_{1}^{\prime}$ can be taken, similarly $e$ can already be taken in $v(\mathcal{A})$. After the delay $d_{2}$, we still have $w^{\prime\prime}_{1}\models I(\ell_{1}^{\prime})$ therefore we still have $w^{\prime\prime}_{1}\models v(g)$. The second transition $e^{\prime\prime}$ in $v(T(\mathcal{A}))$ to $\ell_{2}$ can be taken, similarly $e$ can still be taken in $v(\mathcal{A})$. Clocks are reset along $e$ so $w_{2}=[w^{\prime\prime}_{1}]_{R}$ and we obtain a run of length $n$ in $v(\mathcal{A})$ ending in $(\ell_{2},w_{2})$. ∎

III-C Undecidability for PTAsI

Theorem 1**.**

$\mathsf{EF}$-emptiness is undecidable for PTAsI.

Proof.

From Lemma 1, for any valuation $v$, reachability of a location in $v(\mathcal{A})$ and $v(T(\mathcal{A}))$ is equivalent. Therefore, $\mathsf{EF}$-emptiness holds for $\mathcal{A}$ iff $\mathsf{EF}$-emptiness holds for $T(\mathcal{A})$. As $\mathsf{EF}$-emptiness is undecidable for PTAs without invariant [AHV93], $\mathsf{EF}$-emptiness is undecidable for PTAsI. ∎

IV A new decidable subclass

We now consider PTAsI with only upper-bound invariants.

Definition 5**.**

A PTA with only upper-bound invariants (PTA${}_{I}^{U}$) is a PTAI where each inequality in an invariant is of the form $x\triangleleft\sum_{1\leq i\leq M}\alpha_{i}p_{i}+d$.

An example of PTA${}_{I}^{U}$ is given in Fig. 6.

PTAs${}_{I}^{U}$ can be seen as a subclass of L/U-PTAs, a formalism for which $\mathsf{EF}$-emptiness is decidable [Hun+02, BL09] while $\mathsf{AF}$-emptiness is undecidable [JLR15]. In addition, the synthesis of (even integer-valued) parameters for which $\mathsf{EF}$ holds in L/U-PTAs cannot be done [JLR15]. PTAs${}_{I}^{U}$ can also be seen as a subclass of U-PTAs [BL09], i. e., L/U-PTAs with only upper-bound parameters, a formalism for which $\mathsf{EF}$-emptiness is decidable [Hun+02, BL09] while $\mathsf{AF}$-emptiness is open, and full TCTL-emptiness is undecidable [ALR18]; in addition, $\mathsf{EF}$-synthesis of integer-valued parameter can be achieved [BL09], but the possibility to perform or not the exact synthesis of rational-valued parameters for $\mathsf{EF}$ remains open.

The main differences between PTAs${}_{I}^{U}$ and U-PTAs are

the absence of guards in PTAs${}_{I}^{U}$, and 2. 2.

the possibility only for U-PTAs to involve constraints of the form $x>c$ or $x\geq c$ in clock constraints, provided $c$ is a constant (no parameter can be used as a lower-bound constraint).

In this section, we will see that these differences will allow not only for positive decidability results but will also make exact synthesis possible.

IV-A Reachability ($\mathsf{EF}$)

IV-A1 $\mathsf{EF}$-emptiness

We first show that, while matching the decidability of L/U-PTAs (and U-PTAs) for $\mathsf{EF}$-emptiness, the complexity of $\mathsf{EF}$-emptiness for PTA${}_{I}^{U}$ is not the same as for U-PTAs, which is PSPACE-complete for integer parameter valuations [BL09]; in our case, given a PTA${}_{I}^{U}$ $\mathcal{A}$ and a special parameter valuation $v_{1}$ that sets all parameters to $1$, it is sufficient to test in $v_{1}(\mathcal{A})$ the reachability of a given location in a [math]-delay (a run of duration 0), which is linear in the number of locations of $\mathcal{A}$.linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: plutôt que…? That is, we do not perform a symbolic analysis (using the region graph [AD94] or the zone graph [BY03]) of some TA, but we directly syntactically analyze our PTA${}_{I}^{U}$.

Formally, let $v_{1}$ be the parameter valuation such that $\forall 1\leq i\leq M:v_{1}(p_{i})=1$. In the following lemma, we will show that there exists a valuation $v$ such that there exists a run in $v(\mathcal{A})$ reaching a given location $\ell_{f}$ iff there exists a 0-delay run in $v_{1}(\mathcal{A})$ reaching $\ell_{f}$. By 0-delay run, we mean for which the sum of the delays along the edges is 0. This will allow us to only test 0-delay runs in $v_{1}(\mathcal{A})$ to decide $\mathsf{EF}$-emptiness.

Lemma 2**.**

Let $\mathcal{A}$ be a PTA${}_{I}^{U}$ and $\ell_{f}$ a goal location. There exists a parameter valuation $v$ and a run in $v(\mathcal{A})$ reaching $\ell_{f}$ iff there exists a 0-delay run in $v_{1}(\mathcal{A})$ reaching $\ell_{f}$.

Proof.

• $\Longrightarrow$

Assume there exists a parameter valuation $v$ and a run $\rho$ in $v(\mathcal{A})$ reaching $\ell_{f}$. We first show that there exists a 0-delay run $\rho_{0}$ in $v(\mathcal{A})$ reaching $\ell_{f}$ (and, in fact, going through the same locations and edges as $\rho$, with only the delay being replaced with 0). This is immediate from the syntax of PTAs${}_{I}^{U}$: since we only allow invariants of the form $x\triangleleft\sum_{1\leq i\leq M}\alpha_{i}p_{i}+d$, then nothing can constrain a run to spend a certain amount of time in a location. Therefore, $\rho_{0}$ can follow the same locations and edges as in $\rho$ without letting any time elapse. This gives that there exists a 0-delay run $\rho_{0}$ in $v(\mathcal{A})$ reaching $\ell_{f}$.

We will now show that this run $\rho_{0}$ is also a run of $v_{1}(\mathcal{A})$. This is not entirely immediate, as $v_{1}(\mathcal{A})$ and $v(\mathcal{A})$ have different invariants, coming from different parameter valuations. Indeed, in case of invariants of the form $x<p$, a 0-delay run is blocked in this location whenever $p=0$ (as the constraint $x<0$ is never satisfiable due to the non-negative nature of clocks). However, by definition, $\rho_{0}$ does not pass through any location with an invariant of the form $x<p$, with $v(p)=0$, since this is a valid run of $v(\mathcal{A})$. That is, for any location $\ell$ along $\rho_{0}$ with an invariant containing an inequality of the form $x<p$, $v(p)>0$. We can finally conclude by observing that, in $v_{1}(\mathcal{A})$, no such invariant blocking a 0-delay run exists since, by definition of $v_{1}(\mathcal{A})$, all parameters evaluate to 1. Therefore $\rho_{0}$ is also a run reaching $\ell_{f}$ in $v_{1}(\mathcal{A})$.

• $\Longleftarrow$

The opposite direction is trivial. It suffices to pick $v=v_{1}$ and, since there exists a 0-delay run in $v_{1}(\mathcal{A})$ reaching $\ell_{f}$, then there exists a run (in 0-delay) in $v(\mathcal{A})$ reaching $\ell_{f}$.

∎

From Lemma 2, we state the following theorem.

Theorem 2**.**

$\mathsf{EF}$-emptiness is decidable in NLOGSPACE for PTA${}_{I}^{U}$.

Proof.

Let $\mathcal{A}$ be a PTA and $\ell_{f}$ be a target location. From Lemma 2, there exists a parameter valuation $v$ and a run in $v(\mathcal{A})$ reaching $\ell_{f}$ iff there exists a 0-delay run in $v_{1}(\mathcal{A})$ reaching $\ell_{f}$. That is, it suffices to test only the existence of at least one 0-delay run in $v_{1}(\mathcal{A})$ to decide $\mathsf{EF}$-emptiness in $\mathcal{A}$.

From the nature of PTAs${}_{I}^{U}$, there exists a 0-delay run in $v_{1}(\mathcal{A})$ iff there exists in the automaton $v_{1}(\mathcal{A})$ seen as a graph a syntactic path from $\ell_{0}$ to $\ell_{f}$ that features no state with an invariant involving a comparison of the form $x<0$, for some $x$. We can therefore consider $v_{1}(\mathcal{A})$ as a directed graph, in which we remove all the edges to locations where there is an invariant containing a comparison of the form $x<0$ for some $x$. In this obtained oriented graph, we perform the reachability of $\ell_{f}$ from $\ell_{0}$ which is NLOGSPACE [Pap94], so is $\mathsf{EF}$-emptiness for PTA${}_{I}^{U}$. ∎

IV-A2 $\mathsf{EF}$-synthesis

We will show that, in order to compute $\mathsf{EF}$-synthesis, it suffices to test (syntactically, without semantic analysis) each automaton obtained by replacing each parameter valuation with either 0 or 1. This is a strong result, as $\mathsf{EF}$-synthesis cannot be performed for L/U-PTAs with either integer or rational valued parameters [JLR15], and can only be performed for U-PTAs over integer-valued parameters [BL09]. linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: ben si, non ? linecolor=orange,backgroundcolor=orange!25,bordercolor=orange]$\mathbb{MR}$: non EXPTIME pour la synthèse We first define an equivalence relation for parameter valuations.

Definition 6**.**

Let $v,v^{\prime}$ be two parameter valuations. We say that $v\sim v^{\prime}$ if, for each parameter $p$, $v(p)=0$ iff $v^{\prime}(p)=0$ (i. e., $v(p)>0$ iff $v^{\prime}(p)>0$).

Lemma 3**.**

Let $\mathcal{A}$ be a PTA${}_{I}^{U}$ and $\ell_{f}$ a goal location. Let $v,v^{\prime}$ be two parameter valuations such that $v\sim v^{\prime}$.

There exists a run in $v(\mathcal{A})$ reaching $\ell_{f}$ iff there exists a 0-delay run in $v^{\prime}(\mathcal{A})$ reaching $\ell_{f}$.

Proof.

The proof reuses the same technique as in Lemma 2.

• $\Longrightarrow$

Assume there exists a parameter valuation $v$ and a run $\rho$ in $v(\mathcal{A})$ reaching $\ell_{f}$. From the reasoning used in the proof of Lemma 2, there exists a 0-delay run $\rho_{0}$ in $v(\mathcal{A})$ reaching $\ell_{f}$ (and, in fact, going through the same locations and edges as $\rho$, with only the delay being replaced with 0).

We will now show that this run $\rho_{0}$ is also a run of $v^{\prime}(\mathcal{A})$. Following again the reasoning used in the proof of Lemma 2, by definition, $\rho_{0}$ does not pass through any location with an invariant of the form $x<p$, with $v(p)=0$, since this is a valid run of $v(\mathcal{A})$. That is, for any location $\ell$ along $\rho_{0}$ with an invariant containing an inequality of the form $x<p$, $v(p)>0$. We can finally conclude by observing that, in $v^{\prime}(\mathcal{A})$, no such invariant blocking a 0-delay run exists since, from the fact that $v\sim v^{\prime}$, $v(p)>0$ iff $v^{\prime}(p)>0$ for all $p$. Therefore $\rho_{0}$ is also a run reaching $\ell_{f}$ in $v^{\prime}(\mathcal{A})$.

• $\Longleftarrow$

The opposite direction is similar. Since there exists a 0-delay run in $v^{\prime}(\mathcal{A})$, then following the same reasoning as above and since $v\sim v^{\prime}$, then this same 0-delay run is also a run of $v(\mathcal{A})$.

∎

From Lemma 3, it suffices to test one valuation in each of the regions defined by Definition 6. Each region being defined by $v(p)=0$ or $v(p)>0$, for each parameter $p$, it suffices to test both 0 and a non-zero value, e. g., 1. We end up with a set $V$ of $2^{|\mathbb{P}|}$ parameter valuations. This gives the following theorem.

Theorem 3**.**

We can compute the set $\mathsf{EF}$-synthesis of parameter valuations for PTA${}_{I}^{U}$ within exponential time w.r.t. the size of the input.

Proof.

From Lemma 3, given a PTA${}_{I}^{U}$ $\mathcal{A}$ it suffices to test the existence of at least one 0-delay run for one parameter valuation $v$ in each of the regions defined by Definition 6, i. e., from the set $V$. From the proof of Theorem 2, this can be achieved syntactically by solving a reachability problem in the graph of $v(\mathcal{A})$. If the answer to the reachability problem is positive for this parameter valuation, the whole region is added to the result. That is, considering two parameters $p_{1}$ and $p_{2}$, and the valuation such that $v(p_{1})=0$ and $v(p_{2})=1$, the added region is $p_{1}=0\land p_{2}>0$. However, iterate similarly for all valuations in $V$ gives $2^{|\mathbb{P}|}$ different valuated automata and we have to test the reachability for each of them. Therefore, to compute $\mathsf{EF}$-synthesis, we obtain a complexity exponential in time. ∎

This result makes the subclass of PTA${}_{I}^{U}$ very interesting, as a subclass of PTAs where $\mathsf{EF}$-synthesis can be performed. Rare subclasses such as reset-update-to-parameter PTAs [ALR19] enjoy this possibility (and only on bounded parameters), while well-known L/U-PTAs enjoy the only decidability of $\mathsf{EF}$-emptiness while $\mathsf{EF}$-synthesis has been proven intractable [JLR15].

IV-B Undecidability of TCTL-emptiness

While $\mathsf{EF}$-emptiness is decidable for PTA${}_{I}^{U}$, one can wonder whether this extends to the whole TCTL-emptiness problem. We exhibit in this section a nested TCTL formula (by opposition to flat TCTL formula, e. g., $\mathsf{EF}$ or $\mathsf{AF}$), namely $\mathsf{EG}\mathsf{AF}_{=0}$ ap for some atomic property ap and prove that $\mathsf{EG}\mathsf{AF}_{=0}$-emptiness is undecidable for (possibly bounded) PTA${}_{I}^{U}$. The formula $\mathsf{EG}\mathsf{AF}_{=0}$ was already used to prove the TCTL-emptiness of U-PTAs in [ALR18]. This implies the undecidability of the whole TCTL-emptiness problem for (possibly bounded) PTA${}_{I}^{U}$.

Theorem 4**.**

The $\mathsf{EGAF}_{=0}$-emptiness problem is undecidable for bounded PTA${}_{I}^{U}$.

Proof.

We reduce from the boundedness problem for two-counter machines (i. e., whether the value of the counters remains bounded along the execution), which is undecidable [KC10]. Recall that a two-counter machine is a finite state machine with two integer-valued counters $\mathtt{c}_{1},\mathtt{c}_{2}$. Two different instructions are considered, we present those for $\mathtt{c}_{1}$, those for $\mathtt{c}_{2}$ are similar:

when in state $\mathtt{q}_{i}$, increment $\mathtt{c}_{1}$ and go to $\mathtt{q}_{j}$; 2. 2.

when in state $\mathtt{q}_{i}$, if $\mathtt{c}_{1}=0$ go to $\mathtt{q}_{k}$, otherwise decrement $\mathtt{c}_{1}$ and go to $\mathtt{q}_{j}$.

We assume w.l.o.g. that the machine halts iff it reaches a special state $\mathtt{q}_{\textrm{halt}}$.

General explanation of the encoding

Let $\circ$ and $\circ$ be two labels. We define a PTA${}_{I}^{U}$ that, under some conditions, will encode the machine, and for which \mathsf{EGAF}_{=0}{\hbox{\pagecolor{yellow}\circ}}-emptiness holds iff the counters in the machine remain bounded. We will reuse an encoding originally from [ALR16, proof of theorem 1], and apply a few modifications. In fact, recall that PTA${}_{I}^{U}$ disallow the use of comparisons of the form $x=p$, or $x=c$ with $c$ a constant.

We label our transitions with: $\circ$ for the locations already present in [ALR16] (depicted in yellow in our figures), and $\circ$ for the newly introduced locations (depicted in white in our figures). In [ALR16], the gadgets use edges of the form of Fig. 2(a) to encode the two-counter machine instructions. To define a PTA${}_{I}^{U}$, we replace each of these edges by a special construction given in Fig. 2(b) using only inequalities of the form $x\leq k$ and $x<k$ with $k$ either a constant or a parameter. Non guarded transitions are depicted as dotted edges. We will show that a run will exactly encode the two-counter machine if all transitions $x\leq a+1$ (resp. $x\leq 1$) to a location labeled with $\circ$ are in fact taken when the clock valuation is exactly equal to $a+1$ (resp. $1$). Those runs are further denoted by \rho_{\hbox{\pagecolor{yellow}\circ}}. In the transformed version given in Fig. 2(b), due to the $\leq$ invariant runs exist that take the guard “too early” (i. e., before $x_{1}=a+1$). Those are denoted by $\rho_{\circ}$. But, in that case, observe that in $\ell_{1}^{\prime}$, one can either take the transition to $\ell^{\prime\prime}$ or to $\ell_{2}^{\prime}$ (as the invariant to satisfy is $x_{1}<a+1$) and then, go to $\ell_{\mathtt{error}}$. Therefore on this gadget, \mathsf{EG}\mathsf{AF}_{=0}$$\circ is true at $\ell^{\prime}$ iff the guard $x_{1}\leq a+1$ from $\ell$ to $\ell^{\prime}$ is taken at the very last moment. In our gadgets encoding the counters, there will be for each location with invariant $x\leq k$ an associated location with invariant $x<k$, with only a transition to $\ell_{\mathtt{error}}$. Note that \mathsf{AF_{=0}}{\hbox{\pagecolor{yellow}\circ}}{} is trivially truelinecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: en fait seulement AF=0 in $\ell$ and $\ell^{\prime\prime}$ as both locations are labeled with $\circ$ (many runs also exist from $\ell$ to $\ell_{\mathtt{error}}$ and do not encode properly the machine; they will be discarded in our reasoning later).

Our PTA${}_{I}^{U}$ $\mathcal{A}$ uses one parameter $a$ and three parametric clocks  $x_{1},x_{2},z$. Each state $\mathtt{q}_{i}$ of the two-counter machine is encoded by a location $\ell^{i}$ of $\mathcal{A}$. Each increment instruction of the two-counter machine is encoded into a PTA${}_{I}^{U}$ fragment. The decrement instruction is a modification of the one in [ALR16] using the same modifications as the increment gadget.

Given $v$, our encoding is such that when in $\ell^{i}$ with $w(z)=0$ then $w(x_{1})$ (resp. $w(x_{2})$) represents the value of the counter $\mathtt{c}_{1}$ (resp. $\mathtt{c}_{2}$) encoded by $1-v(a)\mathtt{c}_{1}$ (resp. $1-v(a)\mathtt{c}_{2}$) with $v(a)$ small enough so $v(a)\mathtt{c}_{1}<1$ (resp. $v(a)\mathtt{c}_{2}<1$). The two branches in the gadgets handle both cases $w(x_{1})>w(x_{2})$ and $w(x_{1})\leq w(x_{2})$.

Increment gadget

Depicted in Fig. 3. We assume $a\in[0,1]$, in which case our PTA${}_{I}^{U}$ is bounded (if $a$ is unbounded, then our construction proves the unbounded case). In the following, we write $w$ as the tuple $(w(x_{1}),w(x_{2}),w(z))$. The initial encoding when $w(z)=0$ is $w(x_{1})=1-v(a)\mathtt{c}_{1},w(x_{2})=1-v(a)\mathtt{c}_{2},w(z)=0$. From $\ell^{i}$, we prove that there is a unique run, going through the upper branch of the gadget, that reaches $\ell^{j}$ without violating our property. It is the one that takes each transition to a location with an invariant $z\leq 0$ at the exact moment $w(z)=0$, the transition to a location with an invariant $x_{2}\leq 1$ at the exact moment $w(x_{2})=1$ and transition to a location with an invariant $x_{1}\leq a+1$ at the exact moment $w(x_{1})=v(a)+1$. The other runs, that take the transitions “too early” are removed as they violate the property; indeed, if a run takes a transition before the “last moment” allowed by the invariant (e. g., $x\leq 1$), then it can possibly take the successor state with invariant ($x<1$) and go to $\ell_{\mathtt{error}}$. That is, $\mathsf{EG}\mathsf{AF}_{=0}$ does not hold, because not all runs go in 0-time to a $\circ$ location.

So, for each transition, many runs can take it, but we only consider from now on the only one that takes the transition at the last moment, i. e., when the clock is exactly equal to the parameter/constant it is compared to. The same applies at each transition. This gives the following run for the increment gadget:

(\hbox{\pagecolor{yellow}\ell^{i}},w)\stackrel{{\scriptstyle 0}}{{\longrightarrow}}(\ell_{0}^{i},(1-v(a)\mathtt{c}_{1},1-v(a)\mathtt{c}_{2},0))\stackrel{{\scriptstyle 0}}{{\longrightarrow}}(\hbox{\pagecolor{yellow}\ell_{1}^{i}},(1-v(a)\mathtt{c}_{1},1-v(a)\mathtt{c}_{2},0))\stackrel{{\scriptstyle v(a)\mathtt{c}_{2}}}{{\longrightarrow}}(\ell_{2}^{i},(1-v(a)\mathtt{c}_{1}+v(a)\mathtt{c}_{2},1,v(a)\mathtt{c}_{2}))\stackrel{{\scriptstyle 0}}{{\longrightarrow}}(\hbox{\pagecolor{yellow}\ell_{3}^{i}},(1-v(a)\mathtt{c}_{1}+v(a)\mathtt{c}_{2},0,v(a)\mathtt{c}_{2}))\stackrel{{\scriptstyle v(a)-v(a)\mathtt{c}_{2}+v(a)\mathtt{c}_{1}}}{{\longrightarrow}}(\ell_{4}^{i},(1+v(a),v(a)-v(a)\mathtt{c}_{2}+v(a)\mathtt{c}_{1},v(a)+v(a)\mathtt{c}_{1}))\stackrel{{\scriptstyle 0}}{{\longrightarrow}}(\hbox{\pagecolor{yellow}\ell_{5}^{i}},(0,v(a)-v(a)\mathtt{c}_{2}+v(a)\mathtt{c}_{1},v(a)+v(a)\mathtt{c}_{1}))\stackrel{{\scriptstyle 1-v(a)-v(a)\mathtt{c}_{1}}}{{\longrightarrow}}(\ell_{6}^{i},(1-v(a)-v(a)\mathtt{c}_{1},1-v(a)\mathtt{c}_{2},1))\stackrel{{\scriptstyle 0}}{{\longrightarrow}}(\hbox{\pagecolor{yellow}\ell^{j}},(1-v(a)(\mathtt{c}_{1}+1),1-v(a)\mathtt{c}_{2},0)).

We apply the same reasoning on the lower branch of Fig. 3.

Decrement and 0-test gadget

The decrement and 0-test gadget, depicted in Fig. 4, is similar to the one of [ALR16] and undergoes the same modifications as in Fig. 3, the increment gadget. Assume the same requirements as for the increment gadget. From $\ell^{i}$, following the same reasoning as for the increment gadget we prove that there is a unique run, going through the upper branch of the decrement gadget, that reaches $\ell^{j}$ without violating our property.

Assume we are in a configuration $(\ell^{i},w)$ where $w(z)=0$ and suppose $w(x_{1})<1$. We can enter the configuration $(\ell_{i}^{1},(w(x_{1}),w(x_{2}),0))$ as the invariant $z=0$ ensures no time has elapsed; in its short form, the run that reaches $\ell_{j}$ correctly, i. e., satisfying our property $\mathsf{EG}\mathsf{AF}_{=0}$ is:

(\hbox{\pagecolor{yellow}\ell^{i}},w)\stackrel{{\scriptstyle 0}}{{\longrightarrow}}(\ell_{1}^{i},(1-v(a)\mathtt{c}_{1},1-v(a)\mathtt{c}_{2},0))\stackrel{{\scriptstyle 0}}{{\longrightarrow}}(\hbox{\pagecolor{yellow}\ell_{2}^{i}},(1-v(a)\mathtt{c}_{1},1-v(a)\mathtt{c}_{2},0))\stackrel{{\scriptstyle v(a)\mathtt{c}_{1}}}{{\longrightarrow}}(\ell_{3}^{i},(1,1-v(a)\mathtt{c}_{2}+v(a)\mathtt{c}_{1},v(a)\mathtt{c}_{1}))\stackrel{{\scriptstyle 0}}{{\longrightarrow}}(\hbox{\pagecolor{yellow}\ell_{4}^{i}},(0,1-v(a)\mathtt{c}_{2}+v(a)\mathtt{c}_{1},v(a)\mathtt{c}_{1}))\stackrel{{\scriptstyle v(a)-v(a)\mathtt{c}_{1}+v(a)\mathtt{c}_{2}}}{{\longrightarrow}}(\ell_{5}^{i},(v(a)-v(a)\mathtt{c}_{1}+v(a)\mathtt{c}_{2},v(a)+1,v(a)+v(a)\mathtt{c}_{2}))\stackrel{{\scriptstyle 0}}{{\longrightarrow}}(\hbox{\pagecolor{yellow}\ell_{6}^{i}},(v(a)-v(a)\mathtt{c}_{1}+v(a)\mathtt{c}_{2},0,v(a)+v(a)\mathtt{c}_{2}))\stackrel{{\scriptstyle 1-v(a)\mathtt{c}_{2}}}{{\longrightarrow}}(\ell_{7}^{i},(1-v(a)\mathtt{c}_{1}+v(a),1-v(a)\mathtt{c}_{2},v(a)+1))\stackrel{{\scriptstyle 0}}{{\longrightarrow}}(\hbox{\pagecolor{yellow}\ell^{j}},(1-v(a)(\mathtt{c}_{1}-1),1-v(a)\mathtt{c}_{2},0)).

We apply the same reasoning on the lower branch of Fig. 4.

Initial gadget

In Fig. 5, the initial gadget ensures the same way as presented before that the counters are both initialized to 0. Recall that $w(x_{1})=1-v(a)\mathtt{c}_{1}$, and $w(x_{2})=1-v(a)\mathtt{c}_{2}$. The unique run that does not violate $\mathsf{EG}\mathsf{AF}_{=0}$ reaches $\ell_{1}$ exactly when $w(x_{1})=w(x_{2})=1$, ensuring $\mathtt{c}_{1}=\mathtt{c}_{2}=0$.

Simulating the 2-counter machine

Now, let us consider the runs \rho_{\hbox{\pagecolor{yellow}\circ}} that take each transition to a location where there is an invariant at the very last moment; note that other runs violate the property anyway.

• •

If the counters of the two-counter machine remain bounded then,

• –

either the two-counter machine halts by reaching $\mathtt{q}_{\textrm{halt}}$ and there exist parameter valuations $v$ (typically a sufficiently small value for $v(a)$ to encode the value of the counters during the computation). In the constructed PTA${}_{I}^{U}$, once valuated with $v$ there is a (unique)linecolor=orange,backgroundcolor=orange!25,bordercolor=orange]$\mathbb{MR}$: oui? linecolor=orange,backgroundcolor=orange!25,bordercolor=orange]$\mathbb{MR}$: ok run simulating correctly the machine, reaching $\ell_{\mathtt{halt}}$ and staying there forever.

In this first case, \mathsf{EGAF}_{=0}{\hbox{\pagecolor{yellow}\circ}} holds for these valuations: hence \mathsf{EGAF}_{=0}{\hbox{\pagecolor{yellow}\circ}}-emptiness is false;

• –

or the two-counter machine loops forever, never reaches $\mathtt{q}_{\textrm{halt}}$, with values of the counters remaining bounded. There exist small parameter valuations $v$ that encode the maximal value of the counters. In the constructed PTA${}_{I}^{U}$, once valuated with $v$ there is an infinite (unique)linecolor=orange,backgroundcolor=orange!25,bordercolor=orange]$\mathbb{MR}$: ? linecolor=orange,backgroundcolor=orange!25,bordercolor=orange]$\mathbb{MR}$: ok run in the PTA${}_{I}^{U}$ simulating correctly the machine. As this run is infinite, we infinitely often visit the decrement and/or the increment gadget(s).

In this second case, \mathsf{EGAF}_{=0}{\hbox{\pagecolor{yellow}\circ}} also holds for these valuations: hence \mathsf{EGAF}_{=0}{\hbox{\pagecolor{yellow}\circ}}-emptiness is again false.

• •

Conversely, if the counters of the two-counter machine are unbounded, then for any valuation, all runs end in $\ell_{\mathtt{error}}$. This happens either because all the runs took on purpose an unguarded transition to $\ell_{\mathtt{error}}$ or because they blocked due to the fact that counters are unbounded, and therefore, for any arbitrarily small valuation, one of the guards will eventually block the run and send it to $\ell_{\mathtt{error}}$ thanks to the unguarded transitions. That is, it is possible, e. g., in $\ell_{5}^{i}$ of Fig. 3, when the value of $w(z)=v(a)(\mathtt{c}_{1}+1)$ becomes strictly greater than $1$ after a sufficient number of steps. It is no longer possible to take the transition to $\ell_{6}^{i}$ because of the invariant $z\leq 1$ and there is no choice other than reach $\ell_{\mathtt{error}}$ again. Hence there is no parameter valuation for which \mathsf{EGAF}_{=0}{\hbox{\pagecolor{yellow}\circ}} holds, so \mathsf{EGAF}_{=0}{\hbox{\pagecolor{yellow}\circ}}-emptiness is true.

We conclude that \mathsf{EGAF}_{=0}{\hbox{\pagecolor{yellow}\circ}}-emptiness is true iff the values of the counters of the two-counter machine are unbounded. ∎

In this section, we have proved the following properties about PTA${}_{I}^{U}$. Our first result here is that the $\mathsf{EF}$-emptiness for PTA${}_{I}^{U}$ is less than the same reachability problem in classical TAs without parameters.

Paradoxically, this simpler complexity for one TCTL decision problem ($\mathsf{EF}$) does not make PTA${}_{I}^{U}$ a trivial subclass of (P)TAs at all. On the contrary, we proved that the decidability of $\mathsf{EF}$-emptiness does not extend to the whole TCTL logic by exhibiting a TCTL formula for which deciding the emptiness of parameter valuations satisfying it is undecidable, while model-checking TCTL logic is decidable in TAs [ACD93].

V Proof of concept: Case study

To illustrate the usability of PTAs${}_{I}^{U}$, we describe in this section a case study modeled and verified using PTAs${}_{I}^{U}$.

Software support

PTAs${}_{I}^{U}$ are natively supported by IMITATOR [And+12], which is a parametric model checker performing parameter synthesis for parametric timed automata, extended with some useful features such as synchronization, global variables, etc.

Description

The idea here is to model a Real-time Transport Protocol (RTP) using PTAs${}_{I}^{U}$. RTP is a network protocol usually used to deliver video, audio over a network. RTP is mainly used in Voice over IP, teleconference and since the last few years in systems that involve media streaming.

RTP is typically running over User Datagram Protocol (UDP), which can broadcast data to several clients, and is faster as TCP (Transmission Control Protocol) as it does not provide guarantees for message delivery.

Fig. 6 represents a simplified version of an RTP protocol combined with a Real-Time Control Protocol (RTCP). A server sends audio and video data to a client, and the client has the possibility to pause the data stream or ask for more data when its buffer is empty. We use two clocks to model the protocol. {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x} represents the server, while {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}y} represents the client. In each location, the first word represents the state of the client, while the second represents the state of the server. The automaton starts in location {\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathrm{\ell_{1}}} as the client is waiting for its data stream. On the {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{begin}} action, the server first opens the channel for the video within {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{v}} units of time, and the channel for the audio within {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{s}}-{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{v}} units of time, assuming otherwise audio and video would not be synchronized at reception by the client. Then data is streamed for at most {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{send}} units of time to prevent overflowing the bandwidth, in location $\mathrm{idle,sending}$. At this moment, the server stops sending for an undetermined amount of time. In the meantime, the client’s buffer is being emptied. When running {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{outOfData}}, the client switches to location $\mathrm{askMore,sending}$ as the server is still sending data. {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}y} is reset and the system has the possibility to switch to location $\mathrm{idle,sending}$ again if the server is still streaming data, i. e., the constraint {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x}<{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{send}} is still satisfied. While in $\mathrm{idle,sending}$, the client can choose to {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{interrupt}} the data stream. When in location $\mathrm{idle,notSending}$, the client still uses the data of the buffer, but has to request more data at some point, i. e., while {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}y}<{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{rced}} is satisfied. The procedure from {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{start}} is similar to the previously described one.

From locations $\mathrm{askMore,sending}$ and $\mathrm{idle,notSending}$ the location $\mathrm{askMore,notSending}$ is reachable, when the server is not streaming and the client’s buffer is empty. This is the bug state of the system. We are interested in computing the concrete parameter valuations of {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{send}},{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{rced}},{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{s}},{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{v}} s.t. the system can reach the “bad” state $\mathrm{askMore,notSending}$—that is, we aim at performing $\mathsf{EF}$($\mathrm{askMore,notSending)}$-synthesis.

Experiments

We modeled the case study in Fig. 6 in the input language of IMITATOR. Experiments were conducted with IMITATOR 2.11 “Butter Kouign-amann”, on a 2.4 GHz Intel Core i5 processor with 2 GiB of RAM in a VirtualBox environment running Ubuntu.linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: running which os? 333Models and results are available at https://www.imitator.fr/static/ICECCS19/

The synthesis time is less than 1 second with four parameters.

Applying IMITATOR to Fig. 6, we obtain the following result for $\mathsf{EF}$($\mathrm{askMore,notSending)}$-synthesis:

[TABLE]

That is, for almost all parameter valuations, there exists an execution of the system such that it reaches the bad location $\mathrm{askMore,notSending}$. This is not surprising, as it depends on the rate of data exchanged and of the connection quality to the network.linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: ça te va ? je suis pas trop sûr… linecolor=orange,backgroundcolor=orange!25,bordercolor=orange]$\mathbb{MR}$: oui In other words, this bug state can be reached in any case as the data stream can be blocked at any time, i. e., the client may have to wait for the video to load.

A more interesting question is to study whether all runs of some valuations may eventually reach the bug location. This would be worrying, as it would denote that the protocol has no chances of success for these valuations. Therefore, we focus on $\mathsf{EF}$($\mathrm{askMore,notSending}$)-synthesis. This time, we obtain that the set of valuations for which all runs eventually reach $\mathrm{askMore,notSending}$ is empty, and therefore no valuation makes the protocol entirely unsuccessful.

linecolor=blue,backgroundcolor=blue!25,bordercolor=blue]ÉA: dommage que la synthèse ne montre pas d’accumulation de contraintes (du genre $p>p^{\prime}$, car ça aurait pu arriver, en tout cas pour $\mathsf{AF}$

VI Conclusion

We proposed a new parametric timed formalism to reason about timed systems with some uncertain or unknown timing constants, with two interesting positive results. First, the emptiness of the valuation set for which at least one run reaches a location i. e., $\mathsf{EF}$-emptiness, is decidable in linear time which is better than solving the reachability problem for TAs, as it is PSPACE-complete. Second, we showed that exact synthesis can be achieved in exponential time.

In contrast, we showed that (nested) TCTL-emptiness is undecidable, making PTAs${}_{I}^{U}$, as model-checking TCTL is decidable for TAs, a formalism at the border between decidability and undecidability.

Our formalism seems to allow for promising practical applications as shown by Section V, where we successfully modeled a simple data streaming protocol.

Future work

On the theoretical side, the emptiness of some flat TCTL formulas remains open for PTAs${}_{I}^{U}$, notably $\mathsf{AF}$, $\mathsf{EG}$ and $\mathsf{AG}$-emptiness. Improving the complexity of $\mathsf{EF}$-synthesis is also an interesting direction.

More practically, we are interested in proposing dedicated efficient synthesis algorithms for PTAs${}_{I}^{U}$ (independently of the underlying decidability).