# Exemplifying Parametric Timed Specifications over Signals with Bounded Behavior

Étienne André, Masaki Waga, Natuski Urabe, Ichiro Hasuo

► To cite this version:

Étienne André, Masaki Waga, Natuski Urabe, Ichiro Hasuo. Exemplifying Parametric Timed Specifications over Signals with Bounded Behavior. 14th NASA Formal Methods Symposium (NFM 2022), May 2022, Pasadena, United States. pp.470-488, 10.1007/978-3-031-06773-0_25. hal-03690071

HAL Id: hal-03690071

https://hal.science/hal-03690071v1

Submitted on 20 Mar 2025

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
# Exemplifying parametric timed specifications over signals with bounded behavior*

Étienne André¹ ID, Masaki Waga² ID, Natuski Urabe³ ID, and Ichiro Hasuo³,⁴ ID

¹ Université de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France

² Kyoto University, Kyoto, Japan

³ National Institute of Informatics, Tokyo, Japan

⁴ The Graduate University for Advanced Studies, SOKENDAI, Tokyo, Japan

**Abstract.** Specifying properties can be challenging work. In this paper, we propose an automated approach to exemplify properties given in the form of automata extended with timing constraints and timing parameters, and that can also encode constraints over real-valued signals. That is, given such a specification and given an admissible automaton for each signal, we output concrete runs exemplifying real (or impossible) runs for this specification. Specifically, our method takes as input a specification, and a set of admissible behaviors, all given as a subclass of rectangular hybrid automata, namely timed automata extended with arbitrary clock rates, signal constraints, and timing parameters. Our method then generates concrete runs exemplifying the specification.

**Keywords:** specification, timed automata, hybrid automata, signals

## 1 Introduction

Model checking has had a lot of successes in the last decades (see, e. g., [Kur18]). Still, its use in the industry can be seen as slightly disappointing, considering its high advantages in providing system designers with formal guarantees in the correctness of their system. This is especially true for *quantitative model checking*, that considers systems extended with quantities such as probabilities, time, costs... Among the explanations, one reason is the high expertise required by model checking users to master the model, the specification and their semantics. Even domain experts may do manual errors, leading to specifications with a completely different behaviors from the expectations. These issues may then only be solved using a tedious debugging phase.

<footnote>* This is the author (and extended) version of the manuscript of the same name published in the proceedings of the 14th NASA Formal Methods Symposium (NFM 2022). The final authenticated version is available at springer.com. This work is partially supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST and by the ANR-NRF French-Singaporean research program ProMiS (ANR-19-CE25-0015).</footnote>
<figure><img src="image_2.png" /><figcaption>Fig. 1: Examples of PTAS</figcaption></figure>

*Contribution* In this work, we propose an approach to exemplify concrete continuous evolutions of signals over time, according to a specification. We introduce as a specification formalism *parametric timed automata with signals (PTASs)* as an extension of (parametric) timed automata [AD94; AHV93]: our PTASs use the full power of timed automata, with clocks compared to constants, and add the possibility to specify *signal (linear) constraints*, such as "$s_1 \ge 3 \times s_2$". This allows us to easily express specifications of the form “whenever signal $s_1$ is larger than 50, then within at most 15 time units, it holds that $s_1 \ge 3 \times s_2$ and then, within at most 20 more time units, both signals are equal ($s_1 = s_2$)”. Fig. 1a depicts the PTAS encoding this specification (where $c$ is a clock, while $s_1$ and $s_2$ are signals), i. e., $\ell_T$ is reachable whenever the specification is met for some execution.

In addition, we allow for *timing parameters* (unknown constants), thus enabling parametric specifications mixing discrete actions, signal constraints and timing parameters all together, such as “after a first sensing (action *sense*) occurring within $[5, p]$, it holds that $s_1 = s_2$, and after a second sensing occurring within $[5, p]$, it holds that $s_1 < \frac{s_2}{2}$”, where $p$ is a timing parameter. The PTAS encoding this specification is given in Fig. 1b. In this latter case, the exemplification comes in the form of a concrete valuation for *p* and an evolution of the signals satisfying the specification.

In order to bound the possible signal behaviors, we introduce as additional input *signal bounding automata (SBA)*, i. e., automata bounding the admissible behaviors of the signals. These SBAs can be gathered from a (rough) knowledge from the system under consideration; they can also be used to search among the widely variety signals satisfying the specification; for example, we may want to search signals for each scenario, e. g., driving with/without acceleration/deceleration. In addition, thanks to the SBAs, we avoid generating irrelevant signals, e. g., signals with unrealistically large value change even in the negative example generation. Our SBAs assign signals an arbitrary (but piecewise constant) derivative, according to some guards. For example, an SBA could allow a signal $s$ to move from stopped ($\dot{s} = 0$) to slowly growing ($\dot{s} = 1$) and, provided its value is large enough (e. g., $s > 100$), to growing fast ($\dot{s} = 2$). Or another SBA could allow signal $s$ to alternate between slowly ($\dot{s} = 1$) and rapidly ($\dot{s} = 3$) growing—or decreasing; this latter SBA is depicted in Fig. 2.

We generate not only *positive* (“correct”) exemplifications, but also *negative* (“incorrect”, i. e., that do not match the specification). The crux behind this
<figure><img src="image_3.png" /><figcaption>Fig. 2: An example of SBA</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Fig. 3: Concrete runs for Figs. 1a and 2</figcaption></figure>

is that, in order to illustrate a specification, we may need both positive and negative examples that are close to the boundary. See Fig. 4 for an example.

**Example 1.** Let $\mathcal{A}$ be the PTAS in Fig. 1a; let $\mathcal{A}_1$ be the SBA in Fig. 2, and let $\mathcal{A}_2$ be the SBA in Fig. 2 where $s_1$ is replaced with $s_2$. We assume initially $s_1, s_2 \in [0, 10]$. Given the PTAS $\mathcal{A}$ and the 2 SBAs $\mathcal{A}_1$ and $\mathcal{A}_2$ bounding the behavior of $s_1$ and $s_2$, our framework automatically generates several signal evolutions satisfying the specification; we give 3 of them in Fig. 3. Observe that they present 3 very different evolutions of the signals, with different initial valuations, evolution rates, and final valuations.

Our approach is summarized in Fig. 6. More specifically, our contributions are as follows:

1. We introduce three formalisms, all being subclasses of rectangular hybrid automata [Hen96], namely *parametric timed automata with signals* (PTASs) to express specifications, *signal bounding automata* (SBAs) to bound the behavior of each signal, and *parametric linear multi-rate automata* (PLMAs) that will be used for the parallel composition of the aforementioned formalisms; the relationship between these classes is given in Fig. 5;

2. We equip PLMAs with both a concrete and a symbolic semantics;

3. We propose an exemplification algorithm for PLMAs, yielding concrete parameter valuations together with positive and negative runs;

4. We implement our framework into the *IMITATOR* model checker [And21];

5. We show the applicability of our approach on a set of specifications.

*Outline Section 2* reviews related works. *Section 3* recalls the necessary preliminaries. Then, *Section 4* introduces the general class of parametric linear multirate automata (PLMAs), as well as two subclasses used in the subsequent approach. *Section 5* formally defines our specification exemplification problem. *Section 6*
<figure><img src="image_5.png" /><figcaption>Fig. 4: Positive and negative runs for Fig. 1b</figcaption></figure>

<figure><img src="image_6.png" /><figcaption>Fig. 5: Formalisms manipulated in our approach</figcaption></figure>

<figure><img src="image_7.png" /><figcaption>Fig. 6: Our general approach</figcaption></figure>

is the core of our contribution, proposing to exemplify specifications using tech-
niques to exhibit parameter valuations and concrete runs for reachability prop-
erties in PLMAs. Section 7 exemplifies our approach on a set of specifications.
Section 8 concludes and proposes possible future works.

## 2 Related works

There are several works [HMF15; RHM17; PLK18; Bas+21] to visualize counterexamples of a formal specification. One of the closest works to ours is STLInpector [RHM17]. Given a signal temporal logic (STL) [MN04] formula $\varphi$, STLInpector generates a signal $s$ differentiating $\varphi$ and a mutated formula $\varphi'$. Similarly, in [PLK18], concrete traces are automatically generated, that satisfy or violate an STL formula. Such signals are generated by SMT. A difference between [PLK18] and [RHM17] is that [PLK18] considers linear (as opposed to rectangular) predicates. Another related work is ShapEx [Bas+21]. Given a shape expression [Nic+19] $\varphi$, ShapEx generates signals represented by $\varphi$ based on a sampling-based algorithm. Compared with most of these related works, the main difference with our approach is the use of *signal bounding automata*: since most of the existing techniques generate a signal without bounding the admissible
behaviors, an unrealistic signal may be generated. Another difference, especially from SMT-based approaches, is that it is easy for our automata-based approach to generate various signals by covering various paths of the automaton. In contrast, for example, [PLK18] requires an additional constraint, called a *blocking constraint*, to generate various signals. Nevertheless, the use of SMT in the analysis of an automaton (much like nuXmv [Cim+19]) is future work. In addition, most of these works utilize MITL [MNP06], STL [MN04], or an extension of regular expressions. Our approach takes as input a more general, automata-based formalism (using notably timing parameters and multi-rate variables), not restricted to a given logic. We note that one can translate a formula in most of these logics to a timed automaton, which our formalism captures. See e. g., [Bri+17; ACM02] for translation of such logical expressions to timed automata.

In [PBV18], a method is proposed for *visualizing* counterexamples for function block diagrams, of properties expressed in LTL. Both the model and the property can be animated. In [DR19], the focus is *explaining* the violation of a property against a concrete run. The property is given in the low-level “control flow temporal logic” (CFTL). An originality is the notion of *severity*, explaining by how much a timing constraint is violated (which shares similarities with *robustness* [DM10]). The approach is implemented into VYPR2 [Daw+19]. A main difference with our approach is that [DR19] targets the explanation of *one* particular run violation, whereas we seek arbitrary exemplifications of a property (both positive and negative), independently of a run. Visualization of specifications was also considered, e. g., for Z specification [KC99] and for a DSL based on Event-B [TMB16].

Another direction to tackle the difficulty of specification writing is translation of a natural language description to a temporal logic formula, e. g., [He+21].

Finally, our new notion of *signal bounding automaton*, used to bound the possible behavior of the signals, can be reminiscent of the recent model-bounded monitoring framework, which we introduced in [WAH21]. In that paper, we used a rough over-approximation to bound the possible behaviors while performing monitoring of a black-box system. Similar idea is also used in [Bar+20] to bound the signal space in the falsification problem by a timed automaton [AD94].

The main originality of our work is

1. the use of quantitative specifications (involving notably continuous time, timing parameters and signals), and

2. the use of signal bounding automata to bound the admissible behaviors.

# 3 Preliminaries: Constraints and Rectangular Hybrid Automata

## 3.1 Clocks, parameters and guards

We assume a set $V = \{v_1, \dots, v_H\}$ of real-valued continuous variables. Different from timed automata “clocks” [AD94], our variables (closer to hybrid systems’ “continuous variables”) can have different rates, and turn negative. A variable
valuation is a function $\mu : \mathbb{V} \to \mathbb{R}$. We write $\vec{0}$ for the variable valuation assigning
0 to all variables. Given $d \in \mathbb{R}$, and a flow (or rate) function $f : \mathbb{V} \to \mathbb{Q}$
assigning each variable with a flow (i. e., the value of its derivative), we define
the time elapsing function $te$ as follows: $te(\mu, f, d)$ is the valuation such that
$\forall v \in \mathbb{V} : te(\mu, f, d)(v) = \mu(v) + f(v) \times d$. Given $R \subseteq \mathbb{V}$, we define the *reset* of a
valuation $\mu$, denoted by $[\mu]_R$, as follows: $[\mu]_R(v) = 0$ if $v \in R$, and $[\mu]_R(v) = \mu(v)$
otherwise.

We assume a set $\mathbb{P} = \{p_1, \dots, p_M\}$ of (timing) parameters, i. e., unknown constants. A parameter valuation $\lambda$ is a function $\lambda : \mathbb{P} \to \mathbb{Q}_+$. We assume $\bowtie \in \{\langle-, \leq, =, \geq, \rangle\}$. A parametric linear term over $\mathbb{V} \cup \mathbb{P}$ is of the form $\sum_{1 \leq i \leq H} \alpha_i v_i + \sum_{1 \leq j \leq M} \beta_j p_j + d$, with $v_i \in \mathbb{V}$, $p_j \in \mathbb{P}$, and $\alpha_i, \beta_j, d \in \mathbb{Q}$. A parametric linear inequality is $\text{plt} \bowtie 0$, where $\text{plt}$ is a parametric linear term. A parametric linear constraint $\mathbf{C}$ (i. e., a convex polyhedron) over $\mathbb{V} \cup \mathbb{P}$ is a conjunction of parametric linear inequalities. Given $\mathbf{C}$, we write $\mu \models \lambda(\mathbf{C})$ if the expression obtained by replacing each $v$ with $\mu(v)$ and each $p$ with $\lambda(p)$ in $\mathbf{C}$ evaluates to true.

## 3.2 Rectangular hybrid automata

Let $\mathcal{I}(\mathbb{R})$ denote the set of all intervals over $\mathbb{R}$. We first recall rectangular hybrid automata (RHAs)$^5$, a subclass of hybrid automata. Our definition involves (timing) parameters; parameters could be seen as syntactic sugar for a subset of variables (i. e., variables of arbitrary initial value and of zero rate throughout the automaton), but we still add them explicitly as they will explicitly appear in subsequent subclasses of RHAs.

**Definition 1 (RHA).** A rectangular hybrid automaton (RHA) $\mathcal{A}$ is a tuple
$\mathcal{A} = (\Sigma, L, \ell_0, F, \mathbb{V}, V_0, \mathbb{P}, I, f, E)$, where:

1. $\Sigma$ is a finite set of actions,

2. $L$ is a finite set of locations,

3. $\ell_0 \in L$ is the initial location,

4. $F \subseteq L$ is the set of accepting locations,

5. $\mathbb{V}$ is a finite set of variables,

6. $V_0 : \mathbb{V} \to \mathcal{I}(\mathbb{R})$ is the initial set of variable valuations,

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

8. $I$ is the invariant, assigning to every $\ell \in L$ a parametric linear constraint
$I(\ell)$ over $\mathbb{V} \cup \mathbb{P}$,

9. $f$ is the flow (or rate), assigning to every $\ell \in L$ and $v \in \mathbb{V}$ a flow $f(\ell, v) \in \mathcal{I}(\mathbb{R})$,

10. $E$ is a finite set of edges $e = (\ell, g, a, R, \ell')$ where $\ell, \ell' \in L$ are the source and target locations, $a \in \Sigma$, $R \subseteq \mathbb{V}$ is a set of variables to be reset, and $g$ is a parametric linear constraint over $\mathbb{V} \cup \mathbb{P}$.

<footnote n="5">⁵ We use a slightly different definition of RHAs when compared to, e. g., [Hen96]: in that latter work, RHAs use *bounded* rectangular regions for invariants and flows. In addition, the definition of the variable reset is also different in [Hen96] (they use a *rectangular update*). These definitions have no impact on the correctness nor applicability of our approach.</footnote>
*Parallel composition* RHAs can be composed using synchronized product (see e. g., [Ras05, Definition 4]) in a way similar to finite-state automata. The synchronized product of *n* RHAs $\mathcal{A}_i, i \in \{1, ..., n\}$, denoted by $\mathcal{A}_1 \parallel \mathcal{A}_2 \parallel \dots \parallel \mathcal{A}_n$, is known to be an RHA [HPR94]. Of importance is that, in a composed location, the global flow constraint is the intersection of the local component flow constraints.

*Concrete semantics* We do not give the concrete semantics of this formalism, as we will manipulate a subclass called parametric linear multi-rate automaton (PLMA).

# 4 Parametric linear multi-rate automata

Timed automata extend finite-state automata with clocks (i. e., real-valued variables evolving at the same constant rate 1), that can be compared with integer constants along transitions (“guards”) or within locations (“invariants”). Parametric timed automata (PTAs) extend TAs with parameters within guards and invariants in place of integer constants [AHV93], i. e., allowing inequalities of the form $v \succcurlyeq p$ (simple guards) or sometimes $v - v' \succcurlyeq p$ (diagonal constraints), where $v, v' \in \mathbb{V}$ and $p \in \mathbb{P}$. Here, we extend PTAs notably with:

1. multi-rate clocks (called *variables*), i. e., each clock can have an arbitrary (but constant) rational rate in each location; and

2. linear constraints over variables and parameters, instead of the usual definition $v \succcurlyeq p$.

We first define parametric linear multi-rate automata (PLMA) with their syntax (Section 4.1) and semantics (Section 4.2); we then propose two other subformalisms of RHAs (Section 4.3) used subsequently in this paper.

## 4.1 Syntax

We extend (P)TAs with (constant) *flows*; in the absence of timing parameters, this formalism is usually called *multi-rate timed automata* [Alu+95; DY95]. Also note that, different from TA clocks, our variables can possibly turn *negative*. In addition, we extend the usual syntax of clock guards to our aforementioned definition of *parametric linear constraints*.

**Definition 2 (PLMA).** An RHA $\mathcal{A} = (\Sigma, L, \ell_0, F, \mathbb{V}, V_0, \mathbb{P}, I, f, E)$ is a parametric linear multi-rate automaton (PLMA) if: $\forall \ell \in L, \forall v \in \mathbb{V}: f(\ell, v) \in \mathbb{Q}$.

That is, a PLMA is an RHA where all flows are constant. Observe that the flow is taken in $\mathbb{Q}$, which includes negative rates and zero-rates (also called *stopwatches* [CL00]).

A PLMA is *strongly deterministic* if $\forall \ell \in L, \forall a \in \Sigma, |\{(\ell'_1, g', a', R', \ell'_2) \in E | \ell'_1 = \ell \land a' = a\}| \le 1$.
<figure><img src="image_8.png" /><figcaption>Fig. 7: A PLMA example</figcaption></figure>

*Example 2.* Consider the PLMA in Fig. 7. In the PLMA figures, we use notation $\dot{v}_i = d$ in location $\ell_j$ to denote $f(\ell_j, s_i) = d$. This PLMA contains two variables $v_1$ and $v_2$, and one parameter $p$. $\ell_1$ is the initial location, while $\ell_3$ is the (only) accepting location. We have $V_0(v_1) = [0, 0]$ and $V_0(v_2) = [-2, 2]$.

Given a parameter valuation $\lambda$, we denote by $\lambda(\mathcal{A})$ the non-parametric structure where all occurrences of a parameter $p_i$ have been replaced by $\lambda(p_i)$. We call such a structure a *linear multi-rate automaton* (LMA). Note that, whenever all rates are 1 ($\forall \ell \in L, \forall v \in V, f(\ell, v) = 1$), all guards and invariants are of the form $v \bowtie d, d \in \mathbb{Q}_+$, and all variables are initially 0 (i. e., $\forall v \in V: V_0(v) = \{0\}$), then the resulting structure is a *timed automaton* [AD94].<fnref n="6" />

## 4.2 Semantics

**Concrete semantics of LMAs** The semantics of LMAs is close to that of multi-rate automata, extended with linear constraints over variables.

**Definition 3 (Semantics of an LMA).** Given a PLMA $\mathcal{A} = (\Sigma, L, \ell_0, F, \mathbb{V}, V_0, \mathbb{P}, I, f, E)$, and a parameter valuation $\lambda$, the semantics of $\lambda(\mathcal{A})$ is given by the timed transition system (TTS) $(S, S_0, \rightarrow)$, with

$$ - S = \{(\ell, \mu) \in L \times \mathbb{R}^H \mid \mu \models \lambda(I(\ell))\}, $$

$$ - S_0 = \{(\ell_0, \mu) \mid \mu \models \lambda(I(\ell_0)) \wedge \forall v : \mu(v) \in V_0(v)\}, $$

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

1. discrete transitions: $(\ell, \mu) \stackrel{e}{\mapsto} (\ell', \mu')$, if $(\ell, \mu), (\ell', \mu') \in S$, and there exists $e = (\ell, g, a, R, \ell') \in E$, such that $\mu' = [\mu]_R$, and $\mu \models \lambda(g)$.

2. delay transitions: $(\ell, \mu) \stackrel{d}{\mapsto} (\ell, \text{te}(\mu, f(\ell), d))$, with $d \in \mathbb{R}_+$, if $\forall d' \in [0, d], (\ell, \text{te}(\mu, f(\ell), d')) \in S$.

Moreover we write $(\ell, \mu) \stackrel{(d,e)}{\mapsto} (\ell', \mu')$ for a delay transition followed by a discrete transition if $\exists \mu'' : (\ell, \mu) \stackrel{d}{\mapsto} (\ell', \mu'') \stackrel{e}{\mapsto} (\ell', \mu')$.

Given an LMA $\lambda(\mathcal{A})$ with concrete semantics $(S, S_0, \rightarrow)$, we refer to the states of $S$ as the *concrete states* of $\lambda(\mathcal{A})$. A *concrete run* of $\lambda(\mathcal{A})$ is an alternating sequence of concrete states of $\lambda(\mathcal{A})$ and pairs of edges and delays starting from an initial state $s_0 \in S_0$ of the form $s_0, (d_0, e_0), s_1, \dots$ with $i = 0, 1, \dots, e_i \in E$, $d_i \in \mathbb{R}_+$ and $s_i \stackrel{(d_i, e_i)}{\longrightarrow} s_{i+1}$. Given a state $s = (\ell, \mu)$, we say that $s$ is reachable

<footnote n="6">⁶ Strictly speaking, a TA requires $d \in \mathbb{N}$; however, using an appropriate rescaling of the constants (by multiplying all constants in $\lambda(\mathcal{A})$ by the least common multiple of their denominators), we obtain an equivalent (integer-valued) TA.</footnote>
in $\lambda(\mathcal{A})$ if $s$ appears in a run of $\lambda(\mathcal{A})$. By extension, we say that $\ell$ is reachable. A run $\rho$ is said to be *accepting* if there exists $\ell \in F$ such that $\ell$ is reachable along $\rho$.

A negative run of $\lambda(\mathcal{A})$ is an alternating sequence of states $(\ell_i, \mu_i)$ and pairs of edges and delays of the form $(\ell_0, \mu_0), (d_0, e_0), (\ell_1, \mu_1), \dots$ with $i = 0, 1, \dots, e_i \in E$ and $d_i \in \mathbb{R}_+$, which is not a concrete run of $\lambda(\mathcal{A})$. That is, there exists some $i$ such that $(\ell_i, \mu_i)$ is not a concrete state of $\lambda(\mathcal{A})$, or $(\ell_i, \mu_i) \xrightarrow{(d_i, e_i)} (\ell_{i+1}, \mu_{i+1})$ does not belong to the semantics of $\lambda(\mathcal{A})$. To distinguish from negative runs, we will sometimes refer to concrete runs as *positive* runs.

**Example 3.** Consider again the PLMA $\mathcal{A}$ in Fig. 7, and let $\lambda$ be such that $\lambda(p) = 12$. Consider the following run $\rho$ of $\lambda(\mathcal{A})$: $(\ell_1, (0, -2)), (e_1, 3.8), (\ell_2, (0, 9.4)), (e_2, 3), (\ell_3, (3, 9.4)), \text{ where } e_1 \text{ is the edge from } \ell_1 \text{ to } \ell_2 \text{ in Fig. 7, and } e_2 \text{ is the edge from } \ell_2 \text{ to } \ell_3. \text{ (As an abuse of notation, we write } (\ell_0, (0, -2)) \text{ for } (\ell_0, \mu_0) \text{ where } \mu_0(v_1) = 0 \text{ and } \mu_0(v_2) = -2.)$ Observe that, after 3.8 time units in $\ell_1$, we have $v_1 = 2 \times 3.8 = 7.6$ (which satisfies invariant $v_1 \le 10$) while $v_2 = 9.4$; therefore, guard $2 \times v_1 > v_2 + 2$ evaluates to $15.2 > 11.4$, and therefore the transition to $\ell_2$ can be taken. After 3 time units in $\ell_2$, not modifying the value of $v_2$ as $f(\ell_2, v_2) = 0$, the guard to $\ell_3$ is satisfied as $9.4 \in [9, 13]$ (recall that $\lambda(p) = 12$).

$\rho$ is accepting as it ends in the accepting location $\ell_3$.

Now consider the following alternative sequence $\rho'$: $(\ell_1, (0, 0)), (e_1, 5), (\ell_2, (0, 15)), (e_2, 3), (\ell_3, (3, 15)).$ This sequence is a *negative* run of $\lambda(\mathcal{A})$, as the transition via $e_2$ cannot be taken for this valuation $(15 \notin [9, 13])$. However, $\rho'$ is a positive run of $\lambda'(\mathcal{A})$, where $\lambda'(p) = 14.5$.

A graphical representation of (positive and negative) runs focusing on the *evolution of the variables over time* can be obtained directly from the runs. This graphical representation is made of $H$ lines (where $H$ denotes the variables cardinality) obtained as follows: given a (positive or negative) run $(\ell_0, \mu_0), (d_0, e_0), (\ell_1, \mu_1), \dots$, given a variable $v$, the initial point is $(0, \mu_0(v))$. Then, for each $i \ge 0$, we add a point $(\tau_i + d_i, \mu_i(v) + d_i \times f(\ell_i)(v))$ and a point $(\tau_{i+1}, \mu_{i+1}(v))$, where $\tau_i$ is the absolute date at which $\ell_i$ is entered, i. e., $\tau_i = \sum_{j=0}^{j<i} d_j$. That is, each variable $v$ defines graphically a non-necessarily differentiable piecewise linear function.

**Example 4.** Consider the first run $\rho$ from Example 3. Its associated graphical representation is given in Fig. 8.

**Symbolic semantics** Let us now define the symbolic semantics of PLMAs, as an extension of the semantics of PTAs (see e. g., [Hun+02; And+09; JLR15]) to multi-rates and linear constraints.
<figure><img src="image_9.png" /><figcaption>Fig. 8: Graphical run</figcaption></figure>

<figure><img src="image_10.png" /><figcaption>Fig. 9: A parametric zone graph</figcaption></figure>

**Constraints** We first need to define operations on constraints. Given a parameter valuation $\lambda$ and a variable valuation $\mu$, we denote by $\mu|\lambda$ the valuation over $\mathbb{V} \cup \mathbb{P}$ such that for all variables $v$, $\mu|\lambda(v) = \mu(v)$ and for all parameters $p$, $\mu|\lambda(p) = \lambda(p)$. Given a parametric linear constraint $C$, we use the notation $\mu|\lambda \models C$ to indicate that $\mu \models \lambda(C)$. We say that $C$ is satisfiable if $\exists\mu, \lambda$ s.t. $\mu|\lambda \models C$. We will often use geometrical concepts for constraints; in particular, whenever $\mu|\lambda \models C$, then the valuation $\mu|\lambda$ can be seen as a point belonging to the polyhedron $C$.

We define the time elapsing of $C$ w.r.t. flow $f: \mathbb{V} \to \mathbb{Q}$, denoted by $te(C, f)$, as the constraint over $\mathbb{V}$ and $\mathbb{P}$ obtained from $C$ by delaying all variables by an arbitrary amount of time according to $f$. That is, $\mu'|\lambda \models te(C, f)$ iff $\exists\mu: \mathbb{V} \to \mathbb{R}, \exists d \in \mathbb{R} \text{ s.t. } \mu|\lambda \models C \wedge \mu' = te(\mu, f, d)$.

Given $R \subseteq \mathbb{V}$, we define the *reset* of $C$, denoted by $[C]_R$, as the constraint obtained from $C$ by resetting to 0 the variables in $R$, and keeping the other variables unchanged. We denote by $C \downarrow_P$ the projection of $C$ onto $\mathbb{P}$, i. e., obtained by eliminating the variables not in $\mathbb{P}$ (e. g., using Fourier-Motzkin [Sch86]). The application of these operation to a linear constraint yields a linear constraint; this can be computed efficiently using operations on polyhedra [BMZ08].

**Definition 4 (Symbolic state).** A symbolic state is a pair $(\ell, C)$ where $\ell \in L$ is a location, and $C$ is a linear constraint called a parametric zone.

**Definition 5 (Symbolic semantics).** Given a PLMA $\mathcal{A} =$ ($\Sigma, L, \ell_0, F, \mathbb{V}, V_0, \mathbb{P}, I, f, E$), the symbolic semantics of $\mathcal{A}$ is the labeled transition system called parametric zone graph $\mathcal{PZG}(\mathcal{A}) = (E, \mathbf{S}, \mathbf{s}_0, \Rightarrow)$, with

$$ - \mathbf{S} = \{(\ell, \mathbf{C}) \mid \mathbf{C} \subseteq I(\ell)\}, $$

$$ - \mathbf{s}_0 = (\ell_0, te(\bigwedge_{1 \le i \le H} v_i \in V_0(v_i)), f(\ell_0) \wedge I(\ell_0)), \text{ and} $$

$$ - ((\ell, \mathbf{C}), e, (\ell', \mathbf{C}')) \in \Rightarrow \text{ if } e = (\ell, g, a, R, \ell') \in E \text{ and } \mathbf{C}' = te(((\mathbf{C} \wedge g)]_R \wedge I(\ell')), f(\ell')) \wedge I(\ell') \text{ with } \mathbf{C}' \text{ satisfiable.} $$

That is, in the parametric zone graph, nodes are symbolic states, and arcs are labeled by edges of the original PLMA. Observe that, as in PTAs, a symbolic state contains all the valuations after time elapsing (instead of just the valuations after a discrete transition).

If $((\ell, \mathbf{C}), e, (\ell', \mathbf{C}')) \in \Rightarrow$, we write $\text{Succ}(\mathbf{s}, e) = (\ell', \mathbf{C}')$, where $\mathbf{s} = (\ell, \mathbf{C})$. By extension, we write $\text{Succ}(\mathbf{s})$ for $\cup_{e \in E} \text{Succ}(\mathbf{s}, e)$.

A symbolic run $\mathbf{r}$ of $\mathcal{A}$ is an alternating sequence of symbolic states of $\mathcal{A}$ and edges starting from the initial state $\mathbf{s}_0$ of the form $\mathbf{s}_0, e_0, \mathbf{s}_1, \dots$ with $i = 0, 1, \dots, e_i \in E$, and $\text{Succ}(\mathbf{s}_i, e_i) = \mathbf{s}_{i+1}$. (The symbolic runs of $\mathcal{A}$ are the runs of $\mathcal{PZG}(\mathcal{A})$.) $\text{edgeAt}(\mathbf{r}, k)$ denotes $e_k$, and $\text{stateAt}(\mathbf{r}, k)$ denotes $\mathbf{s}_k$. When $\mathbf{r}$ is
finite, $|\mathbf{r}|$ denotes its length, i. e., its number of edges (therefore, a finite symbolic
run contains $|\mathbf{r} + 1|$ symbolic states).

*Example 5.* Consider again the PLMA $\mathcal{A}$ in Fig. 7. Then, $\mathcal{PZG}(\mathcal{A})$ (limited to its reachable states) is given in Fig. 9. The constraints in each location give both the admissible valuations for $p$ for which this location is reachable, and a condition over the continuous variables $v_1$ and $v_2$ to remain in this location. Note that (the reachable part of) this PZG is finite, which is not necessarily the case in general.

## 4.3 Two other subclasses of RHAs: PTASs and SBAs

### Parametric timed automata with signals

**Definition 6.** An RHA $\mathcal{A} = (\Sigma, L, \ell_0, F, \mathbb{V}, V_0, \mathbb{P}, I, f, E)$ is a parametric timed automaton with signals (PTAS) if:

1. the set of variables is partitioned into $\mathbb{V} = \mathbb{C} \cup \mathbb{S}$, where $\mathbb{C}$ is a set of standard TA clocks (i. e., variables with rates 1), and $\mathbb{S}$ is a set of signals;

2. all clock rates are 1, i. e., $\forall \ell \in L, \forall c \in \mathbb{C}, f(\ell, c) = 1$;

3. signals satisfy the following constraints:

(a) all signal rates are unconstrained, i. e., $\forall \ell \in L, \forall s \in \mathbb{S}, f(\ell, s) = \mathbb{R}$;

(b) a signal cannot be reset, i. e., $\forall (\ell, g, a, R, \ell') \in E, \forall v \in R : v \notin \mathbb{S}$; and

(c) each parametric linear inequality in guards and invariants cannot involve both a standard clock from $\mathbb{C}$ and a signal from $\mathbb{S}$ (i. e., comparisons of the form $c \succcurlyeq s$, with $c \in \mathbb{C}$ and $s \in \mathbb{S}$, are not allowed).

Observe that, since the signal rates are $= \mathbb{R}$, the formalism of PTAS is not a subclass of PLMAs (see Fig. 5), as this latter formalism imposes $f(\ell, s) = d$ for some $d \in \mathbb{Q}$. However, in practice, a PTAS will always be composed (using synchronized product) with a set of PLMAs (actually SBAs, see below) constraining the rate of signals (see Lemma 1 below).

*Example 6.* Consider the PTAS in Fig. 1b. Its clock set is $\mathbb{C} = \{c\}$ while its signal set is $\mathbb{S} = \{s_1, s_2\}$. The set of parameters is $\mathbb{P} = \{p\}$. We have $f(\ell_1, c) = f(\ell_2, c) = f(\ell_T, c) = 1$ (not explicitly depicted in Fig. 1b).

**Signal bounding automata** Second, we define a signal bounding automaton as a special LMA used to constrain the admissible behaviors of a signal. Therefore, it contains a single variable (actually a signal), no parameter, and no reset.

**Definition 7.** A PLMA $\mathcal{A} = (\Sigma, L, \ell_0, F, \mathbb{S}, \mathbb{P}, I, f, E)$ is a signal bounding automaton (SBA) if:

1. $\mathbb{P} = \emptyset$;

2. $|\mathbb{S}| = 1$; and

3. no resets are allowed, i. e., $\forall (\ell, g, a, R, \ell') \in E, R = \emptyset$.
*Example 7.* An example of SBA is given in Fig. 2, where $\mathcal{S} = \{s_1\}$. In the SBA figures, we use notation $s_1 = d$ in location $\ell$ to denote $f(\ell, s_1) = d$.

**Lemma 1.** Let $\mathcal{A}$ be a PTAS with $n$ signals. Let $A_i, i \in \{1, \dots, n\}$ be $n$ SBAs such that $A_i$ contains a signal variable $s_i$. Then $\mathcal{A} \parallel A_1 \parallel \dots \parallel A_n$ is a PLMA.

*Proof.* Let $\mathcal{A}$ be a PTAS with $n$ signals. Let $A_i, i \in \{1, \dots, n\}$ be $n$ SBAs such that $A_i$ contains a signal variable $s_i$. Then $\mathcal{A} \parallel A_1 \parallel \dots \parallel A_n$ is a PLMA.

In practice, SBAs can also involve one or more clocks, e. g., to measure time between signal changes. This is both harmless in theory, and allowed by our implementation.

# 5 Problem

## 5.1 Framework

**Expressing specifications over signals** In our work, we consider as first input a PTAS featuring a set of $n$ signals, and acting as a *specification automaton*. Given a parameter valuation $\lambda$ and a specification expressed as a PTAS $\mathcal{A}$ with accepting locations $F$, the specification is satisfied iff $F$ is reachable in $\lambda(\mathcal{A})$.

*Example 8.* Consider again the PTAS in Fig. 1a, featuring one clock $c$ and two signals $s_1$ and $s_2$. Location $\ell_T$ is reachable whenever the following property is satisfied: “whenever signal $s_1$ is larger than 50, then within at most 15 time units, it holds that $s_1 \ge 3 \times s_2$ and then, within at most 20 more time units, both signals are equal”.

**Bounding signal behaviors** In order to define the admissible behaviors of the signals, we also consider an SBA for each of the signals used in the PTAS.

*Example 9.* Consider again the SBA in Fig. 2. This SBA constrains the behavior of signal $s_1$: this signal can either increase (with flow 1 or flow 3), or decrease (flow -1 or -3). This automaton also constrains $s_1$ to remain non-negative.

## 5.2 Formal problem

Since the specification (given by a PTAS) is parametric, we first aim at deriving concrete parameter valuations for which the specification is valid, i. e., for which one accepting state is reachable. Second, for a given concrete valuation, we aim at deriving a set of concrete accepting positive runs, as well as negative runs.

**Specification exemplification problem:**

INPUT: A PTAS $\mathcal{A}$ featuring $n$ signals, and $n$ SBAs $A_i, i \in \{1, \dots, n\}$

PROBLEM: Exhibit a set of parameter valuations $\lambda$ and a set of concrete accepting positive runs and negative runs of $\lambda((\mathcal{A} \parallel A_1 \parallel \dots \parallel A_n))$
<table>
  <thead>
    <tr>
      <th colspan="2">Algorithm 1: Main algorithm exemplify(A)</th>
    </tr>
  </thead>
  <tbody>
    <tr>
      <td>input</td>
      <td>: A PLMA with symbolic initial state s<sub>0</sub> and accepting locations F</td>
    </tr>
    <tr>
      <td>output</td>
      <td>: A set of negative runs and positive runs</td>
    </tr>
    <tr>
      <td>1</td>
      <td>Explore PZG(A) until a state (l<sub>T</sub>, C) is found, for some l<sub>T</sub> &isin; F and some C</td>
    </tr>
    <tr>
      <td>/*</td>
      <td>Pick a run r from s<sub>0</sub> to (l<sub>T</sub>, C)</td>
    </tr>
    <tr>
      <td>2</td>
      <td>r &larr; PickSymbRun(PZG, s<sub>0</sub>, (l<sub>T</sub>, C))</td>
    </tr>
    <tr>
      <td>3</td>
      <td>return exemplify3(A, r)</td>
    </tr>
  </tbody>
</table>

**Assumptions** Recall that our general approach is given in Fig. 6. In Section 6, we come to our main approach for exemplifying specifications over signals with a bounded behavior; to this end, we propose a method to derive concrete parameter valuations and concrete runs for a PLMA.

In our approach, we make the following assumption (only required when computing *negative* runs):

**Assumption 1** *The PTAS and SBAs must be strongly deterministic, and feature no silent transition.*

(Silent actions, also called ε-transitions, are unobservable actions—not defined in Definition 1 anyway.)

# 6 Exemplifying bounded signal specifications

We propose in this section a heuristics-based method to exemplify runs for an arbitrary PLMA.

The entry point is exemplify in Algorithm 1. We first explore the PZG until a target state is found (line 1). Then, we exhibit a symbolic run from the initial state $s_0$ to the target state (line 2). Finally, Algorithm 1 calls exemplify3, given in Algorithm 2, that returns (up to) 3 concrete runs: one positive run together with a concrete parameter valuation, one negative run for a different parameter valuation, and one negative run for the same parameter valuation.

Let us explain these steps in more details in the following.

## 6.1 Exploration and symbolic run exhibition

The construction of the PZG is made on-the-fly, using Definition 5. In our implementation, this is done using a breadth-first search (BFS) manner, but any other exploration order can be used.

Then, the function *PickSymbRun* takes as argument the PZG *PZG*, the initial state $s_0$, and the target state (here $(\ell_T, C)$), and returns a symbolic run from $s_0$ to $(\ell_T, C)$ in *PZG*. The actual function (not given in this paper) is implemented in a straightforward manner in our toolkit using a backward analysis in *PZG* from $(\ell_T, C)$ to $s_0$. The exhibited symbolic run is not necessarily unique and, as heuristics, we use a shortest run (again, not necessarily unique),
<caption>**Algorithm 2: exemplify3(A, r): Exemplifying 3 concrete runs**</caption>

input : A PLMA $\mathcal{A}$, a symbolic run $\mathbf{r}$ from $s_0$ to $(\ell_T, \mathbf{C})$
output : A set $\mathcal{R}$ of concrete negative runs and positive runs
1 & R \leftarrow \emptyset
   /* Part 1: positive run */
2 & $\mu|\lambda \leftarrow exhibitPoint(\mathbf{C})$
3 & $\rho \leftarrow reconstructPos(\mathcal{A}, \mathbf{r}, |\mathbf{r}|, (\ell_T, \mu|\lambda))$
4 & $\mathcal{R} \leftarrow \mathcal{R} \cup \{\rho\}$
   /* Part 2a: negative run (different parameter valuation) */
5 & if hasPdeadlock($\mathbf{r}$) then
   6 & & ($\lambda_i, (\ell_i, \mathbf{C}_i)$) \leftarrow findPdeadlock($\mathbf{r}$)
   7 & & $\mu_i \leftarrow exhibitPoint(\lambda_i(\mathbf{C}_i))$
   8 & & $\rho_{pref} \leftarrow reconstructPos(\mathcal{A}, \mathbf{r}, i, (\ell_i, \mu_i|\lambda_i))$
   9 & & $\rho_{suf} \leftarrow constructNeg(\mathcal{A}, \mathbf{r}, i, |\mathbf{r}|, \mu_i|\lambda_i)$
  10 & & $\rho \leftarrow \rho_{pref} + \rho_{suf}$
  11 & & $\mathcal{R} \leftarrow \mathcal{R} \cup \{\rho\}$
   /* Part 2b: negative run (same parameter valuation) */
  12 & if hasVdeadlock($\mathbf{r}$) then
  13 & & ($\mu_i, (\ell_i, \mathbf{C}_i)$) \leftarrow findVdeadlock($\mathbf{r}, \lambda$)
  14 & & $\rho_{pref} \leftarrow reconstructPos(\mathcal{A}, \mathbf{r}, i, (\ell_i, \mu_i|\lambda))$
  15 & & $\rho_{suf} \leftarrow constructNeg(\mathcal{A}, \mathbf{r}, i, |\mathbf{r}|, \mu_i|\lambda)$
  16 & & $\rho \leftarrow \rho_{pref} + \rho_{suf}$
  17 & & $\mathcal{R} \leftarrow \mathcal{R} \cup \{\rho\}$
  18 & return $\mathcal{R}$

with “shortest” to be understood as the number of discrete steps. Alternative
definitions could be used (e. g., minimal-time run [And+19])—but are not im-
plemented in our toolkit.

6.2 Deriving a final concrete valuation

After exhibiting a symbolic run, our next step is to derive concrete runs from
that symbolic run. This is the purpose of exemplify3($\mathcal{A}, \mathbf{r}$), given in Algorithm 2.

We first explain Algorithm 2 as a whole, and then proceed to subfunctions
in the following. The first step in exemplify3 is to exhibit a “point”, i. e., a con-
crete variable and parameter valuation in the target state constraint C (line 2).
Since C is a polyhedron, we use a dedicated function exhibitPoint(C). There is
no theoretical difficulty in exhibiting a concrete point in a polyhedron; however,
our dedicated function must both be efficient and yield a valuation which is as
“human-friendly” as possible, i. e., avoiding random rational numbers and avoid-
ing as much as possible to select “0” if another suitable valuation exists. The
body of our function exhibitPoint is given in Appendix B.
## 6.3 Exhibiting concrete example runs

We then reconstruct a concrete positive run (line 3 in Algorithm 2) from the point $\mu|\lambda$ that was just exhibited in the final constraint. This function reconstructPos poses no specific theoretical difficulty, but yields some practical subtleties, discussed in Appendix C.1. Note that it is always possible to reconstruct a concrete run from a symbolic run.

The second part of Algorithm 2 (line 5–line 11) consists in exhibiting a negative run (based on $\mathbf{r}$) for a different parameter valuation than the one ($\lambda$) exhibited in the first part of the algorithm. The heuristics we use is to (try to) exhibit a parameter valuation that *cannot* take one of the transitions of the symbolic run $\mathbf{r}$: this is a *parametric deadlock*. If such a valuation exists, then the projection onto the parameters of some constraints along the run $\mathbf{r}$ is *shrinked*, i. e., this run is possible for some parameter valuations up to some state, and then possible for less parameter valuations.

**Parametric deadlocks** Parametric deadlock checking was studied in, e. g., [And16; AL17], and *findPdeadlock* is basically based on these former works, except that we used the symbolic semantics of PLMAs instead of PTAs. *findPdeadlock* attempts at exhibiting a parameter valuation that cannot pass one of the edges of a symbolic run $\mathbf{r}$. In other words, it tries to exhibit a parameter valuation that is a member of a polyhedron at state $i$, but not anymore at $i+1$; therefore, there exists a concrete run in $\lambda(A)$ equivalent to $\mathbf{r}$ up to position $i$, but this does not hold for $i+1$. *findPdeadlock* is given in Appendix D.1.

The third part of Algorithm 2 (line 12–line 17) consists in exhibiting a negative run for the same parameter valuation as the one ($\lambda$) exhibited in the first part of the algorithm. Our heuristics is as follows: we try to find a transition within $\mathbf{r}$ for which some variable valuation (for the parameter valuation $\lambda$) cannot take this transition. This can come from an unsatisfied guard or invariant: this is a *non-parametric deadlock*.

In the following, we explain the subfunctions used in the above description of Algorithm 2.

**Non-parametric deadlocks** *findVdeadlock* attempts to exhibit a variable valuation $\mu$ and a symbolic state $\mathbf{s}$ of a symbolic run $\mathbf{r}$ such that there exists a deadlock after $\mathbf{s}$ for $\mu$, i. e., $\mu$ cannot take the edge following $\mathbf{s}$ along $\mathbf{r}$, even after elapsing some time. This is typically the case of the following situations:

1. A valuation “missing” the guard: e. g., a symbolic state over $v$ (with $f(v) = 1$) constraining $v \ge 0$, with an outgoing guard $v = 2$; any value $v > 2$ is deadlocked, as there is no way to take the guard;

2. A guard restraining the relationship between variables: e. g., a symbolic state over $v_1$ and $v_2$ (with $f(v_1) = 1$ and $f(v_2) = 2$) constraining $v_1 \in [0, 2] \land v_2 \in [0, 2]$ with an outgoing guard $v_1 = v_2 = 2$: for example $v_1 = v_2 = 0$ cannot pass this guard, even after elapsing some time, due to the flow differences of $v_1$ and $v_2$.
**Algorithm 3: constructNeg(A, r, i, j, μᵢ|λᵢ):** Reconstruct a negative run from a symbolic run fragment

**input** : A PLMA *A*; A symbolic run *r* from *s*₀ to (*ℓ*<sub>*T*</sub>, *C*); Start position *i* and end position *j*; Starting valuation *μ*ᵢ|*λ*ᵢ

**output**: A concrete negative run fragment

1 $\rho \leftarrow \mu_i|\lambda_i$

2 **for** $k = i$ **to** $j$ **do** $\rho \leftarrow \rho$, $(\text{edgeAt}(\mathbf{r}, k), 1), (\mu_i|\lambda_i + (k - i))$;

3 **return** $\rho$

findVdeadlock is given in Appendix D.2.

## 6.4 Exhibiting negative concrete example runs

The reconstruction of a negative run fragment is given in Algorithm 3. It takes as arguments the start (i) and end (j) positions of the symbolic run r, as well as the concrete valuation μᵢ|λᵢ to start from at position i. Algorithm 3 simply starts from the valuation μᵢ|λᵢ, and takes the same discrete actions as in the symbolic run, but with an (arbitrary) duration 1: that is, for each k from i to j, we add a transition (edgeAt(r, k), 1) (where 1 denotes the duration), and we add the updated valuation (μᵢ|λᵢ + (k - i)), which is equal to (μᵢ|λᵢ incremented by the number of transitions computed so far (k - i)). Note that it would be possible to take any other duration than 1, and apply the resets as in the symbolic run. The fact that this concrete run is an invalid run comes from the fact that the valuation μᵢ|λᵢ is known to be unable to take the immediately following transition, as it is called at lines 9 and 15 of Algorithm 2 where a parametric (resp. non-parametric) deadlock was exhibited.

## 6.5 Formal result

Exemplifying runs for parametric timed formalisms is a very hard problem, as the mere existence of a parameter valuation for which a location is reachable in a PTA is undecidable [AHV93]. While our method is mostly heuristics-based, we prove that, provided at least one parameter valuation allows to reach an accepting location $ℓ_T \in F$, then our method is able to infer at least one (positive) concrete run.

**Proposition 1.** Let *A* be a PLMA with accepting locations *F*. Assume $∃λ: λ(A)$ reaches some $ℓ_T \in F$. Then, assuming a BFS computation of $\mathcal{P}\mathcal{Z}G(A)$, exemplify(*A*) terminates, and outputs at least one positive run.

Our algorithm has no guarantee to exhibit negative runs for several reasons: notably, we use only heuristics, here based on deadlocks: there could be other negative runs than those exhibited based on a (parametric or non-parametric) deadlocks. Still, one can guarantee the following:
**Proposition 2.** Let $\mathcal{A}$ be a PLMA and $\mathbf{r}$ be a symbolic run of $\lambda(\mathcal{A})$ with a parameter valuation $\lambda$. Assume there is a concrete negative run due to parametric (resp. non-parametric) deadlock with the same discrete actions as $\mathbf{r}$. Then, assuming a BFS computation of $\mathcal{PZG}(\mathcal{A})$, exemplify $\mathbf{3}(\mathcal{A}, \mathbf{r})$ outputs a concrete negative run due to parametric (resp. non-parametric) deadlock.

# 7 Proof of concept

We implemented our exemplification algorithm in IMITATOR [And21] (v.3.3-alpha “Cheese Caramel au beurre salé”).<fnref n="7" />

All polyhedral operations are implemented using PPL [BMZ08]. The approach takes as input a network of PLMAs, and attempts to output a set of runs and parameter valuations. As a heuristics, we try to call up to 6 times Algorithm 1, i. e., we try to exhibit up to 6 symbolic runs, and then for each of them, following Algorithm 2, we derive one parameter valuation and a concrete run, followed by a negative run for a different parameter valuation (if any) and a negative run for the same parameter valuation (if any). All analyses terminate within a few seconds, including graphics generation.

All outputs are textual (in a JSON-like format); however, IMITATOR also automatically outputs basic graphics. While graphics such as in Fig. 3 were (manually) redrawn using LATEX, those in Fig. 13 (Appendix G.2) are the exact output by IMITATOR.

**Extensions** Thanks to the expressive power of IMITATOR, we can go beyond the formalism presented here. Notably, arbitrary updates (not necessarily to 0, but to parameters, or other variables) are allowed; also, Boolean variables can encode predicates, which can be seen as a simpler setting than signals (see below).

*A non-parametric specification over Booleans* Assume the following specification: “whenever action $a_1$ occurs, then following a non-0 time, predicate $P_1$ must hold; then, strictly less than 3 time units later, $a_2$ occurs and predicate $P_2$ must not hold”. The PTAS encoding this specification is given in Fig. 10a; the SBA in Fig. 10b simply allows both predicates to switch anytime between true and false.

We give two positive runs in Figs. 11a and 11b and one negative run in Fig. 11c. Observe that the run in Fig. 11c violates the specification because action $a_2$ occurs exactly in 3 time units (instead of < 3 time units) after *check*.

The full set of runs output by our toolkit is given in Appendix G.1.

*A non-parametric specification over signals* Recall the motivating specification from Example 1 with the PTAS from Fig. 1a and the SBA in Fig. 2. We assume that initially $s_1, s_2 \in [0, 10]$ (such non-deterministic assignment is allowed by our framework, from $V_0$ in Definition 2). Three concrete runs are given in Fig. 3, while all six outputs by IMITATOR are given in Fig. 13 (Appendix G.2).

<footnote n="7">⁷ Source code, models and results are available at 10.5281/zenodo.6382893.</footnote>
<figure><img src="image_11.png" /><figcaption>Fig. 10: A non-parametric specification over Boolean predicates</figcaption></figure>

<figure><img src="image_12.png" /><figcaption>Fig. 11: Positive and negative runs for Fig. 10</figcaption></figure>

A parametric specification over signals Now recall the parametric specification from Fig. 1b. Our approach derives a parameter valuation *p* = 10, for which this specification can be satisfied, as well as the concrete run in Fig. 4a. Then, our approach derives a parameter valuation *p* = 5 for which the specification may be violated, with a negative run in Fig. 4b: this run is not valid because the two *sense* actions are separated by < 5 time units. Finally, our approach derives a second negative run, this time for *p* = 10, given in Fig. 4c: again, this run is not valid because two *sense* actions occur in a time 10/3 < 5. The whole set of positive runs is given in Fig. 14, with the two aforementioned negative runs in Fig. 15 (Appendix G.3).

8 Conclusion

We presented a first approach to exemplify specifications over signals (as real-
valued continuous variables with a piecewise-constant rate), also using regular
TA clocks and timing parameters. Our approach's originality is twofold: expres-
sive quantitative specifications (involving notably continuous time, timing pa-
rameters and signals), and the use of newly introduced *signal bounding automata*
to limit the admissible continuous behavior. Our implementation in *IMITATOR*
makes the process fully automated.

While we do not expect our exemplifying approach to allow for users com-
pletely unfamiliar with model checking and timed formalisms to suddenly be-
come experts in these methods, we believe our approach is a first step towards
helping users with a low expertise to increase the confidence they have in their
specifications.
*Future work* A first future work is to study the theoretical background of our specification formalism, and notably its expressiveness. Also, we so far considered only reachability properties, and our framework shall be extended to liveness/fairness, e. g., using the recent liveness synthesis algorithms for PTAs [NPP18; And+21]. The strong determinism assumption (Assumption 1) is required by our algorithms, but shall eventually be lifted.

Another direction is to allow more flexible formalisms (e. g., rectangular hybrid automata) to bound the signals.

One of the future directions is to extend our framework to exemplify a more widely used formalism, e. g., LTL, MITL [MNP06], or STL [MN04]. At least theoretically, this would be straightforward thanks to the high expressiveness of PTASs. In this latter case, we can also benefit from the *positive run exemplification* to exhibit *negative runs*, by taking as input the PTAS corresponding to the *negation* of the original formula.

Further, providing some “coverage” guarantees, with a sufficient number of positive and negative runs, is on our agenda.

One longer-term future work is to use and evaluate our framework to teach students or engineers who are not familiar with formal specifications.

## References

[ACM02] Eugene Asarin, Paul Caspi, and Oded Maler. "Timed regular expressions". In: *Journal of the ACM* 49.2 (2002), pp. 172–206. DOI: 10.1145/506147.506151 (cit. on p. 5).

[AD94] Rajeev Alur and David L. Dill. "A theory of timed automata". In: *Theoretical Computer Science* 126.2 (Apr. 1994), pp. 183–235. ISSN: 0304-3975. DOI: 10.1016/0304-3975(94)90010-8 (cit. on pp. 2, 5, 8).

[AHV93] Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi. "Parametric real-time reasoning". In: *STOC* (May 16–18, 1993). Ed. by S. Rao Kosaraju, David S. Johnson, and Alok Aggarwal. San Diego, California, United States: ACM, 1993, pp. 592–601. ISBN: 0-89791-591-7. DOI: 10.1145/167088.167242 (cit. on pp. 2, 7, 16).

[AL17] Étienne André and Didier Lime. "Liveness in L/U-Parametric Timed Automata". In: *ACSD* (June 25–30, 2017). Ed. by Alex Legay and Klaus Schneider. Zaragoza, Spain: IEEE, 2017, pp. 9–18. DOI: 10.1109/ACSD.2017.19 (cit. on p. 15).

[Alu+95] Rajeev Alur, Costas Courcoubetis, Nicolas Halbwachs, Thomas A. Henzinger, Pei-Hsin Ho, Xavier Nicollin, Alfredo Olivero, Joseph Sifakis, and Sergio Yovine. "The Algorithmic Analysis of Hybrid Systems". In: *Theoretical Computer Science* 138.1 (1995), pp. 3–34. DOI: 10.1016/0304-3975(94)00202-T (cit. on p. 7).

[And+09] Étienne André, Thomas Chatain, Emmanuelle Encrenaz, and Laurent Fribourg. "An Inverse Method for Parametric Timed Automata". In: *International Journal of Foundations of Computer Science* 20.5 (Oct. 2009), pp. 819–836. DOI: 10.1142/S0129054109006905 (cit. on p. 9).
[And+19] Étienne André, Vincent Bloemen, Laure Petrucci, and Jaco van de Pol. "Minimal-Time Synthesis for Parametric Timed Automata". In: *TACAS, Part II* (Apr. 8–11, 2019). Ed. by Tomáš Vojnar and Lijun Zhang. Vol. 11428. Lecture Notes in Computer Science. Prague, Czech Republic: Springer, 2019, pp. 211–228. DOI: 10.1007/978-3-030-17465-1_12 (cit. on p. 14).

[And+21] Étienne André, Jaime Arias, Laure Petrucci, and Jaco van de Pol. "Iterative Bounded Synthesis for Efficient Cycle Detection in Parametric Timed Automata". In: *TACAS* (Mar. 27–Apr. 1, 2021). Ed. by Jan Friso Groote and Kim G. Larsen. Vol. 12651. Lecture Notes in Computer Science. Virtual: Springer, 2021, pp. 311–329. DOI: 10.1007/978-3-030-72016-2_17 (cit. on p. 19).

[And16] Étienne André. "Parametric Deadlock-Freeness Checking Timed Automata". In: *ICTAC* (Oct. 24–28, 2016). Ed. by Augusto Cesar Alves Sampaio and Farn Wang. Vol. 9965. Lecture Notes in Computer Science. Taipei, Taiwan: Springer, 2016, pp. 469–478. DOI: 10.1007/978-3-319-46750-4_27 (cit. on p. 15).

[And21] Étienne André. "IMITATOR 3: Synthesis of timing parameters beyond decidability". In: *CAV* (July 18–23, 2021). Ed. by Rustan Leino and Alexandra Silva. Vol. 12759. Lecture Notes in Computer Science. virtual: Springer, 2021, pp. 1–14. DOI: 10.1007/978-3-030-81685-8_26 (cit. on pp. 3, 17).

[Bar+20] Benoît Barbot, Nicolas Basset, Thao Dang, Alexandre Donzé, James Kapinski, and Tomoya Yamaguchi. "Falsification of Cyber-Physical Systems with Constrained Signal Spaces". In: *NFM* (May 11–15, 2020). Ed. by Ritchie Lee, Susmit Jha, and Anastasia Mavridou. Vol. 12229. Lecture Notes in Computer Science. Moffett Field, CA, USA: Springer, 2020, pp. 420–439. DOI: 10.1007/978-3-030-55754-6_25 (cit. on p. 5).

[Bas+21] Nicolas Basset, Thao Dang, Felix Gigler, Cristinel Mateis, and Dejan Ničković. "Sampling of shape expressions with ShapEx". In: *MEMOCODE* (Nov. 20–22, 2021). Ed. by S. Arun-Kumar, Dominique Méry, Indranil Saha, and Lijun Zhang. Virtual Event: ACM, 2021, pp. 118–125. DOI: 10.1145/3487212.3487350 (cit. on p. 4).

[BMZ08] Roberto Bagnara, Hill Patricia M., and Enea Zaffanella. "The Parma Polyhedra Library: Toward a Complete Set of Numerical Abstractions for the Analysis and Verification of Hardware and Software Systems". In: *Science of Computer Programming* 72.1–2 (2008), pp. 3–21. DOI: 10.1016/j.scico.2007.08.001 (cit. on pp. 10, 17).

[Bri+17] Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, and Benjamin Monmege. "MightyL: A Compositional Translation from MITL to Timed Automata". In: *CAV, Part I* (July 24–28, 2017). Ed. by Rupak Majumdar and Viktor Kuncak. Vol. 10426. Lecture Notes in Computer Science. Heidelberg, Germany: Springer, 2017, pp. 421–440. DOI: 10.1007/978-3-319-63387-9_21 (cit. on p. 5).

[Cim+19] Alessandro Cimatti, Alberto Griggio, Enrico Magnago, Marco Roveri, and Stefano Tonetta. "Extending nuXmv with Timed Transition Systems and Timed Temporal Properties". In: *CAV, Part I* (July 15–18, 2019). Ed. by Işil Dillig and Serdar Tasiran. Vol. 11561. Lecture Notes in Computer Science. New York City, USA: Springer, 2019, pp. 376–386. DOI: 10.1007/978-3-030-25540-4_21 (cit. on p. 5).
[CL00] Franck Cassez and Kim Guldstrand Larsen. "The Impressive Power of Stopwatches". In: CONCUR (Aug. 22-25, 2000). Ed. by Catuscia Palamidessi. Vol. 1877. Lecture Notes in Computer Science. University Park, PA, USA: Springer, 2000, pp. 138-152. DOI: 10.1007/3-540-44618-4_12 (cit. on p. 7).

[Daw+19] Joshua Heneage Dawes, Giles Reger, Giovanni Franzoni, Andreas Pfeiffer, and Giacomo Govi. "VyPR2: A Framework for Runtime Verification of Python Web Services". In: TACAS, Part II (Apr. 6-11, 2019). Ed. by Tomás Vojnar and Lijun Zhang. Vol. 11428. Lecture Notes in Computer Science. Prague, Czech Republic: Springer, 2019, pp. 98-114. DOI: 10.1007/978-3-030-17465-1_6 (cit. on p. 5).

[DM10] Alexandre Donzé and Oded Maler. "Robust Satisfaction of Temporal Logic over Real-Valued Signals". In: FORMATS (Sept. 8-10, 2010). Ed. by Krishnendu Chatterjee and Thomas A. Henzinger. Vol. 6246. Lecture Notes in Computer Science. Klosterneuburg, Austria: Springer, 2010, pp. 92-106. DOI: 10.1007/978-3-642-15297-9_9 (cit. on p. 5).

[DR19] Joshua Heneage Dawes and Giles Reger. "Explaining Violations of Properties in Control-Flow Temporal Logic". In: RV (Oct. 8-11, 2019). Ed. by Bernd Finkbeiner and Leonardo Mariani. Vol. 11757. Lecture Notes in Computer Science. Porto, Portugal: Springer, 2019, pp. 202-220. DOI: 10.1007/978-3-030-32079-9_12 (cit. on p. 5).

[DY95] Conrado Daws and Sergio Yovine. "Two Examples of Verification of Multirate Timed Automata with Kronos". In: RTSS (Dec. 4-7, 1995). Pisa, Italy: IEEE Computer Society, 1995, pp. 66-75. DOI: 10.1109/REAL.1995.495197 (cit. on p. 7).

[He+21] Jie He, Ezio Bartocci, Dejan Ničković, Haris Isakovic, and Radu Grosu. *From English to Signal Temporal Logic*. Tech. rep. abs/2109.10294. arXiv, 2021 (cit. on p. 5).

[Hen96] Thomas A. Henzinger. "The Theory of Hybrid Automata". In: LICS (July 27-30, 1996). New Brunswick, New Jersey, USA: IEEE Computer Society, 1996, pp. 278-292. DOI: 10.1109/LICS.1996.561342 (cit. on pp. 3.6).

[HMF15] Bardh Hoxha, Nikolaos Mavridis, and Georgios Fainekos. "VISPEC: A graphical tool for elicitation of MTL requirements". In: IROS (Sept. 28-Oct. 2, 2015). Hamburg, Germany: IEEE, 2015, pp. 3486-3492. DOI: 10.1109/IROS.2015.7353863 (cit. on p. 4).

[HPR94] Nicolas Halbwachs, Yann-Éric Proy, and Pascal Raymond. "Verification of Linear Hybrid Systems by Means of Convex Approximations". In: SAS (Sept. 28-30, 1994). Ed. by Baudouin Le Charlier. Vol. 864. Lecture Notes in Computer Science. Namur, Belgium: Springer, 1994, pp. 223-237. DOI: 10.1007/3-540-58485-4_43 (cit. on p. 7).

[Hun+02] Thomas Hune, Judi Romijn, Mariëlle Stoelinga, and Frits W. Vaandrager. "Linear parametric model checking of timed automata". In: *Journal of Logic and Algebraic Programming* 52-53 (2002), pp. 183-220. DOI: 10.1016/S1567-8326(02)00037-1 (cit. on p. 9).

[JLR15] Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. "Integer Parameter Synthesis for Real-Time Systems". In: *IEEE Transactions on Software Engineering* 41.5 (2015), pp. 445-461. DOI: 10.1109/TSE.2014.2357445 (cit. on p. 9).
[KC99] Soon-Kyeong Kim and David A. Carrington. "Visualization of Formal Specifications". In: *APSEC* (Dec. 7-10, 1999). Takamatsu, Japan: IEEE Computer Society, 1999, pp. 102-109. DOI: 10.1109/APSEC.1999.809590 (cit. on p. 5).

[Kur18] Robert P. Kurshan. "Transfer of Model Checking to Industrial Practice". In: *Handbook of Model Checking*. Ed. by Edmund M. Clarke, Thomas A. Henzinger, Helmut Veith, and Roderick Bloem. Springer, 2018, pp. 763-793. DOI: 10.1007/978-3-319-10575-8_23 (cit. on p. 1).

[MN04] Oded Maler and Dejan Ničković. "Monitoring Temporal Properties of Continuous Signals". In: *FORMATS and FTRTFT* (Sept. 22-24, 2004). Ed. by Yassine Lakhnech and Sergio Yovine. Vol. 3253. Lecture Notes in Computer Science. Grenoble, France: Springer, 2004, pp. 152-166. DOI: 10.1007/978-3-540-30206-3_12 (cit. on pp. 4, 5, 19).

[MNP06] Oded Maler, Dejan Ničković, and Amir Pnueli. "From MITL to Timed Automata". In: *FORMATS* (Sept. 25-27, 2006). Ed. by Eugene Asarin and Patricia Bouyer. Vol. 4202. Lecture Notes in Computer Science. Paris, France: Springer, 2006, pp. 274-289. DOI: 10.1007/11867340_20 (cit. on pp. 5, 19).

[Nic+19] Dejan Nickovic, Xin Qin, Thomas Ferrère, Cristinel Mateis, and Jyotir-moy V. Deshmukh. "Shape Expressions for Specifying and Extracting Signal Features". In: *RV* (Oct. 8-11, 2019). Ed. by Bernd Finkbeiner and Leonardo Mariani. Vol. 11757. Lecture Notes in Computer Science. Porto, Portugal: Springer, 2019, pp. 292-309. DOI: 10.1007/978-3-030-32079-9_17 (cit. on p. 4).

[NPP18] Hoang Gia Nguyen, Laure Petrucci, and Jaco van de Pol. "Layered and Collecting NDFS with Subsumption for Parametric Timed Automata". In: *ICECCS* (Dec. 12-14, 2018). Ed. by Anthony Widjaja Lin and Jun Sun. Melbourne, Australia: IEEE Computer Society, Dec. 2018, pp. 1-9. DOI: 10.1109/ICECCS2018.2018.00009 (cit. on p. 19).

[PBV18] Antti Pakonen, Igor Buzhinsky, and Valeriy Vyatkin. "Counterexample visualization and explanation for function block diagrams". In: *INDIN* (July 18-20, 2018). Porto, Portugal: IEEE, 2018, pp. 747-753. DOI: 10.1109/INDIN.2018.8472025 (cit. on p. 5).

[PLK18] Pavithra Prabhakar, Ratan Lal, and James Kapinski. "Automatic Trace Generation for Signal Temporal Logic". In: *RTSS* (Dec. 11-Nov. 14, 2018). Nashville, TN, USA: IEEE Computer Society, 2018, pp. 208-217. DOI: 10.1109/RTSS.2018.00038 (cit. on pp. 4, 5).

[Ras05] Jean-François Raskin. "An Introduction to Hybrid Automata". In: *Handbook of Networked and Embedded Control Systems*. Ed. by Dimitrios Hristu-Varsakelis and William S. Levine. Birkhäuser, 2005, pp. 491-518 (cit. on p. 7).

[RHM17] Hendrik Roehm, Thomas Heinz, and Eva Charlotte Mayer. "STLInspector: STL Validation with Guarantees". In: *CAV, Part I* (July 24-28, 2017). Ed. by Rupak Majumdar and Viktor Kuncak. Vol. 10426. Lecture Notes in Computer Science. Heidelberg, Germany: Springer, 2017, pp. 225-232. DOI: 10.1007/978-3-319-63387-9_11 (cit. on p. 4).

[Sch86] Alexander Schrijver. *Theory of linear and integer programming*. New York, NY, USA: John Wiley & Sons, Inc., 1986 (cit. on p. 10).

[TMB16] Ulyana Tikhonova, Maarten Manders, and Rimco Boudewijns. "Visualization of Formal Specifications for Understanding and Debugging an In-
dustrial DSL". In: *HOFM* (July 4–8, 2016). Ed. by Maria Spichkova and Heinz Schmidt. Vol. 9946. Lecture Notes in Computer Science. Vienna, Austria: Springer, 2016, pp. 179–195. DOI: 10.1007/978-3-319-50230-4_13 (cit. on p. 5).

[WAH21] Masaki Waga, Étienne André, and Ichiro Hasuo. "Model-bounded monitoring of hybrid systems". In: *ICCPS* (May 19–21, 2021). Ed. by Martina Maggio, James Weimer, Mohammad Al Farque, and Meeko Oishi. Nashville, TN, USA: ACM, 2021, pp. 21–32. DOI: 10.1145/3450267.3450531 (cit. on p. 5).
# Appendix

## A Proof of Lemma 1

**Lemma 1 (recalled).** Let $\mathcal{A}$ be a PTAS with $n$ signals. Let $A_i, i \in \{1, \dots, n\}$ be $n$ SBAs such that $A_i$ contains a signal variable $s_i$. Then $\mathcal{A} \parallel \mathcal{A}_1 \parallel \dots \parallel \mathcal{A}_n$ is a PLMA.

First note that the only reason why a PTAS is not a PLMA is because the flow of signal variables are unconstrained ($\forall \ell \in L, \forall s \in S, f(\ell, s) = \mathbb{R}$), while the definition of PLMAs (Definition 2) requires all flows to be (arbitrary) constants. Let $(\ell, \ell_1, \dots, \ell_n)$ be a location of $\mathcal{A} \parallel \mathcal{A}_1 \parallel \dots \parallel \mathcal{A}_n$. From the parallel composition of RHAs, the flow of this composed location is the intersection of the flows of each of the locations $\ell, \ell_1, \dots, \ell_n$. Given a signal $s_i$, the flow of $s_i$ is unconstrained in $\mathcal{A}$ (i.e., $f(\ell, s) = \mathbb{R}$ by Definition 6), and is unconstrained in all SBAs—except in $A_i$ where it is a constant, since Definition 7 defines SBAs as a subclass of PLMAs. Therefore, the intersection of all flows for $s_i$ is equal to this constant. And therefore, $\mathcal{A} \parallel \mathcal{A}_1 \parallel \dots \parallel \mathcal{A}_n$ is a PLMA.

## B Exhibiting a concrete valuation in a polyhedron

We give our algorithm exhibitPoint($\mathbf{C}$) in Algorithm 4.

Since a polyhedron is represented by a constraint (set of linear inequalities), as an abuse of notations, we use both constraint-based notations, and polyhedra-based notations.

Let $\text{Dim}(\mathbf{C})$ denote the set of dimensions (i.e., of variables) of a polyhedron $\mathbf{C}$.

We use the following notations:

- $\text{hasMinimum}(\mathbf{C}, dim)$ is a predicate checking whether variable of dimension $dim$ has a concrete minimum valuation in the polyhedron $\mathbf{C}$. That is, $\mathbf{C} \downarrow_{\{v_{dim}\}}$ (where $v_{dim}$ denotes the variable of dimension $dim$) yields an interval $[a, b]$ or $[a, b)$. In this case, $a$ is the minimum for dimension $dim$, denoted by $\text{minimum}(\mathbf{C}, dim) = a$.

- As a slight abuse of notation, we denote by $\text{infimum}(\mathbf{C}, dim)$ the minimum or infimum value for dimension $dim$, i. e., considering $\mathbf{C} \downarrow_{\{v_{dim}\}}$ yields an interval $(a, b]$ or $(a, b)$ or $[a, b]$ or $[a, b)$, then we define $\text{infimum}(\mathbf{C}, dim) = a$. Dually, we denote by $\text{infimum}(\mathbf{C}, dim) = b$ the maximum or supremum value for dimension $dim$.

We say that a dimension $dim$ is constrained in a polyhedron $\mathbf{C}$ if $dim$ appears in an inequality in the underlying constraint. That is, $dim$ is constrained if $\mathbf{C} \downarrow_{\{v_{dim}\}} \neq (-\infty, \infty)$.

We use $\text{infimum}$ (resp. supremum) to denote the greatest (resp. smallest) possible value which is less (resp. greater) than or equal to all valuations for
<table>
  <caption>Algorithm 4: exhibitPoint(C): exhibiting a point in a polyhedron</caption>
  <thead>
    <tr>
      <th>input</th>
      <td>A polyhedron C</td>
    </tr>
    <tr>
      <th>output</th>
      <td>A point λ ∈ C</td>
    </tr>
  </thead>
  <tbody>
    <tr>
      <td>1</td>
      <td>Let λ</td>
    </tr>
    <tr>
      <td>2</td>
      <td>foreach dim ∈ Dim(C) do</td>
    </tr>
    <tr>
      <td>3</td>
      <td style="padding-left: 2em;">if dim is not constrained in C then</td>
    </tr>
    <tr>
      <td>4</td>
      <td style="padding-left: 4em;">λ(dim) ← 1 /* arbitrary */</td>
    </tr>
    <tr>
      <td>5</td>
      <td style="padding-left: 2em;">else</td>
    </tr>
    <tr>
      <td>6</td>
      <td style="padding-left: 4em;">if hasMinimum(C, dim) then</td>
    </tr>
    <tr>
      <td>7</td>
      <td style="padding-left: 6em;">/* Case 1: constant minimum */</td>
    </tr>
    <tr>
      <td>8</td>
      <td style="padding-left: 6em;">if minimum(C, dim) = 0 ∧ supremum(C, dim) &gt; 0 then</td>
    </tr>
    <tr>
      <td>9</td>
      <td style="padding-left: 8em;">/* Case 1a: supremum &gt; 1: return 1 to avoid 0 */</td>
    </tr>
    <tr>
      <td>10</td>
      <td style="padding-left: 8em;">if supremum(C, dim) &gt; 1 then</td>
    </tr>
    <tr>
      <td>11</td>
      <td style="padding-left: 10em;">λ(dim) ← 1 /* arbitrary to avoid 0 */</td>
    </tr>
    <tr>
      <td>12</td>
      <td style="padding-left: 10em;">else</td>
    </tr>
    <tr>
      <td>13</td>
      <td style="padding-left: 12em;">/* Case 1b: supremum in (0, 1]: return half of it */</td>
    </tr>
    <tr>
      <td>14</td>
      <td style="padding-left: 12em;">λ(dim) ← supremum(C, dim) / 2</td>
    </tr>
    <tr>
      <td>15</td>
      <td style="padding-left: 10em;">else</td>
    </tr>
    <tr>
      <td>16</td>
      <td style="padding-left: 12em;">/* Case 1c: return the minimum */</td>
    </tr>
    <tr>
      <td>17</td>
      <td style="padding-left: 12em;">λ(dim) ← minimum(C, dim)</td>
    </tr>
    <tr>
      <td>18</td>
      <td style="padding-left: 10em;">else if infimum(C, dim) &gt; -∞ ∧ supremum(C, dim) = ∞ then</td>
    </tr>
    <tr>
      <td>19</td>
      <td style="padding-left: 12em;">/* Case 2: some finite infimum, but infinite supremum: return infimum + 1 */</td>
    </tr>
    <tr>
      <td>20</td>
      <td style="padding-left: 12em;">λ(dim) ← infimum(C, dim) + 1</td>
    </tr>
    <tr>
      <td>21</td>
      <td style="padding-left: 10em;">else if infimum(C, dim) = -∞ ∧ supremum(C, dim) &lt; ∞ then</td>
    </tr>
    <tr>
      <td>22</td>
      <td style="padding-left: 12em;">/* Case 3: no finite infimum but some supremum: return 1 if possible, otherwise supremum - 1 */</td>
    </tr>
    <tr>
      <td>23</td>
      <td style="padding-left: 12em;">λ(dim) ← min(1, supremum(C, dim) - 1)</td>
    </tr>
    <tr>
      <td>24</td>
      <td style="padding-left: 10em;">else</td>
    </tr>
    <tr>
      <td>25</td>
      <td style="padding-left: 12em;">/* Case 4: finite infimum and supremum: return middle */</td>
    </tr>
    <tr>
      <td>26</td>
      <td style="padding-left: 12em;">λ(dim) ← infimum(C, dim), supremum(C, dim) / 2</td>
    </tr>
    <tr>
      <td>27</td>
      <td style="padding-left: 10em;">/* Valuate C with the new valuation for dim */</td>
    </tr>
    <tr>
      <td>28</td>
      <td style="padding-left: 10em;">C ← C ∧ dim = λ(dim)</td>
    </tr>
  </tbody>
</table>

a dimension in a constraint. For example, given *dim* ∈ (-2,3] then -2 is an infimum but not a minimum (there is no minimum in this constraint), while 3 is here the supremum and the maximum. We assume the supremum can be ∞ and the infimum can be -∞.

C Computing a concrete (positive) run

C.1 Positive run reconstruction

The reconstruction of a run (fragment) from a symbolic run is given in Algorithm 5. The reconstruction is performed backwards. First, we cancel time elaps-
ing (line 2), i. e., we compute a final valuation from which we can fire (backwards)
the last transition. We then initialize the run to be built from its last (concrete)
state (line 3).

Given $e = (\ell, g, a, R, \ell')$, we write $e.g$ and $e.R$ to denote $g$ and $R$ respectively.

<table><caption>**Algorithm 5: reconstructPos($\mathcal{A}$, $\mathbf{r}$, $i$, $(\ell_i, \mu_i|\lambda)$):** Reconstruct a positive run from a symbolic run</caption><thead><tr><th></th><th></th><th></th></tr></thead><tbody><tr><td>1</td><td>(<i>l</i><sub>i-1</sub>, <b>C</b><sub>i-1</sub>) ← stateAt(<b>r</b>, <i>i</i> - 1)</td><td></td></tr><tr><td></td><td>/* Cancel time elapsing of the last valuation */</td><td></td></tr><tr><td>2</td><td><i>μ</i>'<sub>i</sub> ← exhibitPredCont(<b>C</b><sub>i-1</sub>, <i>e</i><sub>i-1</sub>, <i>l</i><sub>i</sub>, <i>f</i>, <i>I</i>, <i>μ</i><sub>i</sub>)</td><td></td></tr><tr><td>3</td><td><i>ρ</i> ← (<i>l</i><sub>i</sub>, <i>μ</i>'<sub>i</sub>) /* initialization */</td><td></td></tr><tr><td>4</td><td><i>μ</i><sub>k+1</sub> ← <i>μ</i>'<sub>i</sub></td><td></td></tr><tr><td>5</td><td>for <i>k</i> = <i>i</i> - 1 down to 0 do</td><td></td></tr><tr><td>6</td><td>(<i>l</i><sub>k</sub>, <b>C</b><sub>k</sub>) ← stateAt(<b>r</b>, <i>k</i>)</td><td></td></tr><tr><td>7</td><td><i>e</i><sub>k</sub> ← edgeAt(<b>r</b>, <i>k</i>)</td><td></td></tr><tr><td>8</td><td>(<i>l</i><sub>k+1</sub>, <b>C</b><sub>k+1</sub>) ← stateAt(<b>r</b>, <i>k</i> + 1)</td><td></td></tr><tr><td></td><td>/* Exhibit a discrete predecessor valuation */</td><td></td></tr><tr><td>9</td><td><i>μ</i><sub>k</sub> ← exhibitPred(<b>C</b><sub>k</sub>, <i>f</i>(<i>l</i><sub>k</sub>), <i>e</i><sub>k</sub>.g, <i>e</i><sub>k</sub>.R, <i>I</i>(<i>l</i><sub>k+1</sub>), <i>f</i>(<i>l</i><sub>k+1</sub>), <b>C</b><sub>k+1</sub>, <i>μ</i><sub>k+1</sub>, <i>λ</i>)</td><td></td></tr><tr><td></td><td>/* Compute duration between <i>μ</i><sub>k</sub> and its successor */</td><td></td></tr><tr><td>10</td><td><i>d</i> ← computeDur(<i>μ</i><sub>k</sub>, <i>μ</i><sub>k+1</sub>)</td><td></td></tr><tr><td></td><td>/* Update the concrete run */</td><td></td></tr><tr><td>11</td><td><i>ρ</i> ← (<i>l</i><sub>k</sub>, <i>μ</i><sub>k</sub>), (<i>edgeAt</i>(<b>r</b>, <i>k</i>), <i>d</i>), <i>ρ</i></td><td></td></tr><tr><td></td><td>/* Backup for next iteration */</td><td></td></tr><tr><td>12</td><td><i>μ</i><sub>k+1</sub> ← <i>μ</i><sub>k</sub></td><td></td></tr><tr><td>13</td><td>return <i>ρ</i></td><td></td></tr></tbody></table>

The main loop (line 5–line 12) computes the run backwards: first, we exhibit a discrete predecessor valuation (line 9); this is achieved thanks to the dedicated function *exhibitPred*—described in the subsequent Algorithm 6. Then, the duration between the two concrete points is computed (line 10)—this function (not given) is discussed below. Finally, the concrete run is updated (line 11). Here, consistently with our definition in Section 4.2, we use “,” for concatenating states or transitions to a run; that is ($\ell_k, \mu_k$), ($\text{edgeAt}(\mathbf{r}, k)$, $d$), $\rho$ (line 11) denotes the addition of state ($\ell_k, \mu_k$) followed by discrete transition ($\text{edgeAt}(\mathbf{r}, k)$, $d$) in front of $\rho$.

*Computing durations between points* We assume that function `computeDur`($\mu_k$, $\mu_{k+1}$) computes the duration between two consecutive variable valuations. Due to resets (and possible stopwatches), the only way
to achieve this computation is to track a global time clock, i. e., a variable
initially 0, of rate 1 and never reset. In our implementation, we directly add
such a clock from the beginning of the analysis (construction of the parametric
zone graph); however, it is inefficient because

1. it adds one more variables everywhere (hence one more dimensions in all polyhedra), and

2. it may diverge, i. e., its value will never be reset and therefore matches a previously met valuation.

Still, to avoid the second drawback, when testing polyhedra for equality (or inclusion), we first remove (by variable elimination through existential quantification) the global time clock in both polyhedra we test. This comes at an additional cost, as this elimination is usually not a cheap operation. A more efficient way of handling these issues could be to only add the clock when reconstructing the symbolic run. This is future work.

## C.2 Reconstructing predecessors

**Algorithm 6** computes a predecessor, and simply computes a discrete predecessor: by first firing backwards the transition (line 1) using the dedicated function *exhibitPredDisc*, and second by canceling time elapsing, i. e., computing a valuation from which another transition can be fired backwards (line 2) using the dedicated function *exhibitPredCont*. Both functions are described in the following. Note that the correctness of this procedure comes from the fact that the variable valuation passed as an argument is (iteratively) always a valuation from which a discrete predecessor can be computed, without canceling time elapsing (because this was iteratively performed at the previous call).

**Continuous predecessor** The function *exhibitPredCont* canceling time elapsing is given in Algorithm 7. We give an algorithm almost at the implementation level (our implementation is extremely close to this algorithm).

Dually to the time elapsing, we define the *time past* of $\mathbf{C}$ w.r.t. flow $f: \mathcal{V} \to \mathcal{Q}$, denoted by $\mathbf{tp}(\mathbf{C}, f)$, as the constraint over $\mathcal{V}$ and $\mathcal{P}$ obtained from $\mathbf{C}$ by “delaying backwards” all variables by an arbitrary amount of time according to $f$. That is, $\mu|\lambda \models \mathbf{tp}(\mathbf{C}, f)$ iff $\exists \mu: \mathcal{V} \to \mathbb{R}, \exists d \in \mathbb{R} \text{ s.t. } \mu|\lambda \models \mathbf{C} \wedge \mu' = \text{te}(\mu, f, -d)$.

**Discrete predecessor** The function *exhibitPredDisc* canceling time elapsing is given in Algorithm 8. Again, we give an algorithm almost at the implementation level.

Algorithm 8 takes as inputs

1. an edge $e_n$ between some $\ell_n$ and some $\ell_{n+1}$,

2. a symbolic constraint $C_n$,

3. a point $\mu_{n+1}$ of some $C_{n+1}$ “before time elapsing”, i. e., from which one can take in 0-time the transition $e_n$ backwards to $(\ell_n, C_n)$ (this condition is ensured inductively),
<caption>**Algorithm 6:** exhibitPred($\mathbf{C}_{n-1}, e_{n-1}, \ell_n, \mathbf{C}_n, e_n, f, I, \mu_{n+1}$): Exhibit a predecessor</caption>

input : Constraint $\mathbf{C}_{n-1}$
input : Edge $e_{n-1}$
input : Location $\ell_n$
input : Constraint $\mathbf{C}_n$
input : Edge $e_n$
input : Flow function $f$
input : Invariant function $I$
input : Valuation $\mu_{n+1}$
output : A point $\mu_n$ before time elapsing

/* Compute a discrete predecessor, i.e., fire backwards the
transition $n+1$ to $n$ */

1 $\mu'_n \leftarrow exhibitPredDisc(\mathbf{C}_n, e_n, \mu_{n+1})$
/* Cancel time elapsing in state $n$ */

2 $\mu_n \leftarrow exhibitPredCont(\mathbf{C}_{n-1}, e_{n-1}, \ell_n, f, I, \mu'_n)$

3 return $\mu_n$

<caption>**Algorithm 7:** exhibitPredCont($\mathbf{C}_{n-1}, e_{n-1}, \ell_n, f, I, \mu'_n$): Exhibiting a point before time elapsing in a parametric zone</caption>

input : Constraint $\mathbf{C}_{n-1}$ from the state preceding the current one $\mathbf{C}_n$
input : $e_{n-1}$ incoming edge (between $\mathbf{C}_{n-1}$ and $\mathbf{C}_n$)
input : Current location $\ell_n$
input : Flow function $f$
input : Invariant function $I$
input : A point $\mu'_n$ of some $\mathbf{C}_n$ after time elapsing
output : A point $\mu_n$ before time elapsing

/* apply time past */

1 $\mathbf{C}'_n \leftarrow \mathbf{tp}(\mu'_n, (f(\ell_n)))$
/* intersect with current invariant */

2 $\mathbf{C}'_n \leftarrow \mathbf{C}'_n \wedge I(\ell_n)$
/* find the "initial" valuations (symbolic set) */

3 if $(\ell_n, \mu'_n)$ is the initial state then

4 $\mathbf{initvals} \leftarrow \mathbf{C}'_n \wedge \text{initial valuations of clocks and signals}$

5 else
6
/* intersect with incoming state (incl. guard and invariant), to
which updates were applied */

6 $\mathbf{initvals} \leftarrow \mathbf{C}'_n \cap ([(\mathbf{C}_{n-1} \cap e_{n-1} \cdot g)]_{e_{n-1} \cdot R});$
/* Pick a point $\mu_n$ in $\mathbf{initvals}$ */

7 $\mu_n \leftarrow exhibitPoint(\mathbf{initvals})$

8 return $\mu_n$

and returns a point $\mu_n$ of $(\ell_n, \mathbf{C}_n)$ that can reach $\mu_{n+1}$ in 0-time via $e_n$. At line 1 in Algorithm 8, “$\{\mu_{n+1}\}$” denotes the constraint made of the single valuation $\mu_{n+1}$.
<caption>**Algorithm 8: exhibitPredDisc(C<sub>n</sub>, e<sub>n</sub>, μ<sub>n+1</sub>):** Exhibiting a discrete predecessor</caption>

**input** : Preceding constraint C<sub>n</sub>
**input** : An edge e<sub>n</sub> between some l<sub>n</sub> and some l<sub>n+1</sub>
**input** : A point μ<sub>n+1</sub> of some C<sub>n+1</sub> "before time elapsing"
**output** : A point μ<sub>n</sub> of (l<sub>n</sub>, C<sub>n</sub>) that can reach μ<sub>n+1</sub> in 0-time via e<sub>n</sub>
/* Cancel resets from l<sub>n</sub> to l<sub>n+1</sub> */
1 C'<sub>n</sub> ← {μ<sub>n+1</sub>}↓<sub>V\e<sub>n</sub>.R</sub>
/* intersect with C<sub>n</sub> (mainly for the invariant I(l<sub>n</sub>)) */
2 C'<sub>n</sub> ← C'<sub>n</sub> ∩ C<sub>n</sub>
/* intersect with guard between l<sub>n</sub> to l<sub>n+1</sub> */
3 C'<sub>n</sub> ← C'<sub>n</sub> ∩ e<sub>n</sub>.g
/* Pick a point μ in C'<sub>n</sub> */
4 μ<sub>n</sub> ← exhibitPoint(C'<sub>n</sub>)
5 return μ<sub>n</sub>

# D Exhibiting deadlocks

## D.1 Exhibiting parametric deadlocks

*findPdeadlock* is given in Algorithm 9.

<caption>**Algorithm 9: findPdeadlock(r):** Exhibition of a parametric deadlock within a symbolic run</caption>

**input** : A symbolic run r
**output** : A pair made of a parameter valuation λ, and a symbolic state s such that λ cannot take the edge following s along r; or **none** if no such valuation exists
1 **for** i = 0 **to** |r| − 1 **do**
2 &nbsp;&nbsp;&nbsp;&nbsp; (l<sub>i</sub>, C<sub>i</sub>) ← stateAt(r, i)
3 &nbsp;&nbsp;&nbsp;&nbsp; (l<sub>i+1</sub>, C<sub>i+1</sub>) ← stateAt(r, i + 1)
4 &nbsp;&nbsp;&nbsp;&nbsp; /* If some valuations cannot pass the edge */
&nbsp;&nbsp;&nbsp;&nbsp; **if** C<sub>i+1</sub>↓<sub>P</sub> ⊊ C<sub>i</sub>↓<sub>P</sub> **then**
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; /* Pick such a valuation */
5 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; λ ← exhibitPoint(C<sub>i</sub>↓<sub>P</sub> \ C<sub>i+1</sub>↓<sub>P</sub>)
6 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; **return** (λ, (l<sub>i</sub>, C<sub>i</sub>))
7 &nbsp;&nbsp;&nbsp;&nbsp; **return** none

*findPdeadlock* attempts at exhibiting a parameter valuation that cannot pass one of the edges of a symbolic run *r*. In other words, it tries to exhibit a parameter valuation that is member of a polyhedron at state *i*, but not anymore at *i* + 1; therefore, there exists a concrete run in $\lambda(A)$ equivalent to *r* up to position *i*, but this does not hold for *i* + 1.
Precisely, we test whether there is a restriction in the parameter valuations between *i* and *i* + 1 (line 4 in Algorithm 9). If so, we just pick one valuation in the difference (line 5).

## D.2 Exhibiting non-parametric deadlocks

*findVdeadlock* is given in Algorithm 10.

**Algorithm 10: findVdeadlock(r):** Exhibition of a variable deadlock within a symbolic run
***
**input** : A symbolic run **r**
**output** : A pair made of a variable valuation **μ**, and a symbolic state **s** such that **μ** cannot take the edge following **s** along **r**; or **none** if no such valuation exists
***
1 **for** *i* = 0 **to** |**r**| − 1 **do**
2 &nbsp;&nbsp;&nbsp;&nbsp;(*l*<sub>*i*</sub>, **C**<sub>*i*</sub>) ← stateAt(**r**<sub>0</sub>, *i*)
3 &nbsp;&nbsp;&nbsp;&nbsp;(*l*<sub>*i*+1</sub>, **C**<sub>*i*+1</sub>) ← stateAt(**r**<sub>*i*</sub>, *i* + 1)
4 &nbsp;&nbsp;&nbsp;&nbsp;/* Get the transition guard */
5 &nbsp;&nbsp;&nbsp;&nbsp;*g* ← edgeAt(**r**<sub>*i*</sub>, *g*)
6 &nbsp;&nbsp;&nbsp;&nbsp;/* If some variable valuations cannot pass the edge */
7 &nbsp;&nbsp;&nbsp;&nbsp;if **C**<sub>*i*</sub> \ (tp(*g*, *f*(*l*<sub>*i*</sub>)) ∧ I(*l*<sub>*i*</sub>)) ≠ **false** then
8 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;/* Pick such a valuation */
8 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;**μ** ← exhibitPoint(**C**<sub>*i*</sub> \ (tp(*g*, *f*(*l*<sub>*i*</sub>)) ∧ I(*l*<sub>*i*</sub>)))
8 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;return (**μ**<sub>*</sub>, (*l*<sub>*i*</sub>, **C**<sub>*i*</sub>))
8 &nbsp;&nbsp;&nbsp;&nbsp;return **none**
***

The crux of Algorithm 10 is at line 6, where we select a point in the polyhedron which cannot intersect the guard, even after time elapsing or, put it differently, we compute the difference between the original polyhedron $C_i$ and the guard $g$ to which we applied time past, then again intersected with the location invariant.

## E Proof of Proposition 1

**Proposition 1 (recalled).** Let $\mathcal{A}$ be a PLMA with accepting locations $F$. Assume $\exists\lambda: \lambda(\mathcal{A})$ reaches some $\ell_T \in F$. Then, assuming a BFS computation of $\mathcal{PZG}(\mathcal{A})$, exemplify $(\mathcal{A})$ terminates, and outputs at least one positive run.

*Proof.* First, let us prove that some state $(\ell_T, \mathbf{C})$ will indeed be found in $\mathcal{PZG}(\mathcal{A})$, for some $\ell_T \in F$. Assume there exists a concrete run of length $n$ in $\lambda(\mathcal{A})$ reaching $\ell_T$. Then, since the parametric zone graph of $\mathcal{A}$ is discrete, sharing similar edges (up to valuation $\lambda$), then there exists an equivalent symbolic run of $\mathcal{A}$ of same length $n$ reaching $(\ell_T, \mathbf{C})$, for some $\mathbf{C}$. Assuming a
breadth-first search exploration of *PZG(A)*, this state will eventually be computed. (This may not be the case assuming a *depth*-first search exploration, as the exploration could be stuck in a symbolic path of infinite length, therefore never meeting (*l*<sub>*T*</sub>, *C*).)

Second, let us prove that exemplify3 terminates—which is essentially easy. Part 1 is straightforward: exhibiting a point (line 2 in Algorithm 2) does not pose any termination problem, and the reconstruction of the positive run (line 3) is done backwards, with a guarantee of termination. So exemplify3 is guaranteed to exhibit a (positive) concrete run.

Concerning parts 2a and 2b of Algorithm 2, there is no guarantee that a parametric deadlock (line 5), nor a non-parametric deadlock (line 12) can be found—this explains the lack of theoretical guarantee for a negative run exhibition. However, the search for such a deadlock is a simple analysis (Algorithms 9 and 10) of the symbolic run, of finite length, and therefore terminates. In addition, the negative run reconstruction (Algorithm 3) is also guaranteed to terminate, as this is a simple finite iteration over the symbolic run length. This guarantees termination of exemplify3.

## F Proof sketch of Proposition 2

**Proposition 2 (recalled).** Let *A* be a PLMA and *r* be a symbolic run of *λ*(*A*) with a parameter valuation *λ*. Assume there is a concrete negative run due to parametric (resp. non-parametric) deadlock with the same discrete actions as *r*. Then, assuming a BFS computation of *PZG(A)*, exemplify3(*A*, *r*) outputs a concrete negative run due to parametric (resp. non-parametric) deadlock.

*Proof.* From the fact that our method is *symbolically complete*: since our PZG contains all continuous (parameter and variables) valuations, if such a concrete negative run due to parametric (resp. non-parametric) deadlock with the same discrete actions as *r* exists, then it will be found during a backward analysis from the target location. Note that the result only holds because of the BFS computation assumption. A DFS computation might never meet the target state, and therefore not be able to subsequently find the negative concrete run.

## G Detailed raw results

### G.1 Runs for Fig. 10

The positive runs are given graphically in Figs. 12a to 12d. The negative runs are given graphically in Figs. 12e to 12h.

In all subsequent graphics, not only the signals, but also the *clocks* are given. Notably, in Figs. 12a to 12d the third signal is irrelevant (this corresponds to the global time, which obviously increases linearly at rate 1 without reset), and the last one is the (unique) variable *v*.
<figure><img src="image_13.png" /><figcaption>Fig. 12: A non-parametric specification over Booleans (Fig. 10): examples</figcaption></figure>

## G.2 Runs for Figs. 1a and 2

Note that Figs. 3a to 3c correspond to a (manual) representation in LATEX of Figs. 13a, 13b and 13f respectively.

## G.3 Runs for Figs. 1b and 2

A graphical representation of all positive runs is given in Fig. 14, while two negative runs are given in Fig. 15.
<figure><img src="image_14.png" /><figcaption>Fig. 13: Positive runs for Figs. 1a and 2</figcaption></figure>
<figure><img src="image_15.png" /><figcaption>Fig. 14: Positive runs for Figs. 1b and 2</figcaption></figure>
<figure><img src="image_16.png" /><figcaption>Fig. 15: Negative runs for Figs. 1b and 2</figcaption></figure>