Parametric Verification: An Introduction

TL;DR

This paper introduces the field of parametric verification for concurrent systems, covering formal concepts, models, approaches, and practical tools for analyzing systems with unknown or variable parameters.

Contribution

It provides a comprehensive overview of parametric verification methods, models, and tools, along with references for further research in the area.

Findings

Coverage of various models like Parametric Timed Automata and Petri Nets

Introduction of Action Synthesis for property enforcement

Availability of practical tools and tutorials online

Abstract

This paper constitutes a short introduction to parametric verification of concurrent systems. It originates from two 1-day tutorial sessions held at the Petri nets conferences in Toru\'n (2016) and Zaragoza (2017). The paper presents not only the basic formal concepts tackled in the video version, but also an extensive literature to provide the reader with further references covering the area. We first introduce motivation behind parametric verification in general, and then focus on different models and approaches, for verifying several kinds of systems. They include Parametric Timed Automata, for modelling real-time systems, where the timing constraints are not necessarily known a priori. Similarly, Parametric Interval Markov Chains allow for modelling systems where probabilities of events occurrences are intervals with parametric bounds. Parametric Petri Nets allow for compact representation of systems, and cope with different types of parameters. Finally, Action Synthesis aims at enabling or disabling actions in a concurrent system to guarantee some of its properties. Some tools implementing these approaches were used during hands-on sessions at the tutorial. The corresponding practicals are freely available on the Web.

Tables

Table 1. Table 1 : Decidability of the emptiness problems for PTAs and subclasses

Class	U-PTAs	bL/U-PTAs		L/U-PTAs	bIP-PTAs	IP-PTAs	bPTAs	PTAs
		closed	open
EF	[Hun+02]	[ALR16]	open	[Hun+02]	[ALR16]	[ALR16]	[Mil00]	[AHV93]
AF	open	[ALR16]		[JLR15]	[ALR16]	[ALR16]	[ALR16]	[JLR15]
EG	open	[AL17]	[AL17]	[AL17]	open		[AL17]
AG	[AL17]	[ALR16]	open	[AL17]	[ALR16]
TCTL	[ALR18]	[ALR16]		[JLR15]	[ALR16]		[Mil00]	[AHV93]
EC	[AL17]	[AL17]	open	[AL17]	open		[AL17]
ED	open	[AL17]			open		[AL17]	[And16]
LgP	open	[AM15]			open		[AM15]
TrP	open	[AM15]			open		[AM15]

Table 2. Table 2 : Un(decidability) and complexity results for the universal parametric problems

Class	Reachability	S. Unboundness	Coverability
PPN	Undecidable [Dav+15]	Undecidable [Dav+15]	Undecidable [Dav+15]
preT-PPN	Undecidable [Dav17]	ExpSpace-c [Dav+17]	ExpSpace-c [Dav+17]
postT-PPN	Undecidable [Dav17]	ExpSpace-c[Dav17]	ExpSpace-c [Dav+15]
P-PPN	open	ExpSpace-c[Dav17]	ExpSpace-c [Dav+15]
distinctT-PPN	Undecidable [Dav17]	ExpSpace-c[Dav17]	ExpSpace-c [Dav+15]

Table 3. Table 3 : Un(decidability) and complexity results for the existential parametric problems

Class	Reachability	S. Unboundedness	Coverability
PPN	Undecidable [Dav+15]	Undecidable [Dav+15]	Undecidable [Dav+15]
preT-PPN	Undecidable [Dav17]	ExpSpace-c[Dav17]	ExpSpace-c [Dav+15]
postT-PPN	Undecidable [Dav17]	ExpSpace-h[Dav17]	ExpSpace-c [Dav+15]
P-PPN	Decidable [Dav+15]	ExpSpace-h[Dav17]	ExpSpace-c [Dav+15]
distinctT-PPN	Undecidable [Dav17]	ExpSpace-h[Dav17]	ExpSpace-c [Dav+17]

Table 4. Table 4 : Results for the synthesis problem

Class	Reachability	S. Unboundedness	Coverability
PPN	✕	✕	✕
preT-PPN	✕	✓	✓
postT-PPN	✕	✓	✓
P-PPN	open	✓	✓
distinctT-PPN	✕	✕	✕

Equations

$$\varphi :=\varphi \wedge \varphi |\neg \varphi |lt\bowtie 0\text{,}$$

$$w^{\prime }|v\models C^{\nearrow }\text{ iff }\exists w:X\to {\mathbb{R}}_{+},\exists d\in {\mathbb{R}}_{+}\text{ s.t. }{w}^{\prime }|v\models C\wedge w^{\prime }=w+d\text{.}$$

$${\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{press}}^{[1..6]}\ {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{cup}}\ {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{coffee}}\big{(}{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{idle}}^{?}\ {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{press}}^{[1..6]}\ {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{cup}}\ {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{coffee}}\big{)}^{*}$$

$$\displaystyle{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{idle}}\ ({\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{press}}\ {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{add\_sugar}})^{[1..6]}\ {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{cup}}\ {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{preparing\_coffee}}\ {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{coffee}}\ {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{done}}$$

$$\displaystyle\big{(}({\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{idle}}\ {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{idle}})^{?}\ ({\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{press}}\ {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{add\_sugar}})^{[1..6]}\ {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{cup}}\ {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{preparing\_coffee}}\ {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{coffee}}\ {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{done}}\big{)}^{*}$$

$$C^{\prime}=\big{(}[(C\land g)]_{R}\land I(l^{\prime})\big{)}^{\nearrow}\land I(l^{\prime})$$

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

$$\begin{gathered} LC(s,S^{\prime })=\left[\sum _{s^{\prime }\in S^{\prime }}\text{Up}({\varphi }_P(s,s^{\prime }))\ge 1\right]\cap \left[\sum _{s^{\prime }\in S^{\prime }}\text{Low}({\varphi }_P(s,s^{\prime }))\le 1\right] \\ \cap \left[\bigcap _{s^{\prime }\in S^{\prime }}\text{Low}({\varphi }_P(s,s^{\prime }))\le \text{Up}({\varphi }_P(s,s^{\prime }))\right] \end{gathered}$$

$$\begin{gathered} {\text{Cons}}_n^X(s)=\left[\bigcap _{s^{\prime }\in \text{Succ}(s)\setminus X}{\text{Cons}}_{n-1}(s^{\prime })\right]\cap \left[LC(s,\text{Succ}(s)\setminus X)\right] \\ \cap \left[\bigcap _{s^{\prime }\in X}\text{Low}({\varphi }_P(s,s^{\prime }))=0\right] \end{gathered}$$

$$\varphi :=p|\neg \varphi |\varphi \vee \varphi |E_{\alpha }X\varphi |E_{\alpha }G\varphi |E_{\alpha }^{\omega }G\varphi |E_{\alpha }(\varphi U\varphi ),$$

$$f_{E_Y^{\omega }G\varphi }(s)=f_{\varphi }(s)\cap {\text{parPre}}_Y^{\exists }(f_{E_Y^{\omega }G\varphi })(s),$$

$$f_{E_{Y}G\varphi }(s)=f_{\varphi }(s)\cap ({\text{parPre}}_Y^{\exists }(f_{E_Y^{\omega }G\varphi })(s)\cup f_{\neg E_{Y}X\text{true}}(s)).$$

$$f_{E_Y(\varphi U\psi )}(s)=f_{\psi }(s)\cup (f_{\varphi }(s)\cap {\text{parPre}}_Y^{\exists }(f_{E_Y(\varphi U\psi )})(s)).$$

Full text

We first introduce motivation behind parametric verification in general, and then focus on different models and approaches, for verifying several kinds of systems. They include Parametric Timed Automata, for modelling real-time systems, where the timing constraints are not necessarily known a priori. Similarly, Parametric Interval Markov Chains allow for modelling systems where probabilities of events occurrences are intervals with parametric bounds. Parametric Petri Nets allow for compact representation of systems, and cope with different types of parameters. Finally, Action Synthesis aims at enabling or disabling actions in a concurrent system to guarantee some of its properties. Some tools implementing these approaches were used during hands-on sessions at the tutorial. The corresponding practicals are freely available on the Web.

1 Introduction to parametric verification

We first introduce the motivation for performing parametric verification. Several formal models can be considered, depending on the characteristics of the system and its properties the designer wants to address. We will also discuss the problems of interest in such a framework. At the end of this section, we will give pointers to some additional and complementary material.

The reader is assumed to have basic knowledge of Petri nets and/or automata and their associated verification techniques, since they constitute the basis of the formal models we address in a parametric setting.

1.1 Why parameters and of what kind?

Parameters provide several facilities for easily modelling complex systems:

Dimensioning: systems often exhibit components that occur as multiple copies of the same structure or similar ones. For example, a wireless sensor network is composed of a certain number of identical sensors. At the design phase, the exact number of sensors might be unknown and would therefore be a parameter. 2. 2.

Choice of actions: different actions in the system might be possible in a given state. The designer having several possibilities in mind would model them and analyse the behaviour of the system with these actions enabled or disabled. In this case, the enabledness of each individual action is considered as a parameter. 3. 3.

Design choices: different system characteristics can be taken into account at the design phase so as to be evaluated. For example, when designing an electronic system, one might have the choice between different components, available of course at different prices, each providing its specific characteristics, such as a better or worse response time. In such a case, the designer may want to construct a single model, and use these timing characteristics as a parameter so as to evaluate which is the best possible choice according to his/her needs.

To handle the cases described, different kinds of parameters are used. They will influence the type of a formal model and verification techniques chosen. In the three previous cases, parameters would be:

Instances numbering allow for counting identical components in the system. 2. 2.

Controllable actions can be enabled or disabled, as opposed to the other ones which are always available for the system. 3. 3.

Time or probabilities provide means to handle different characteristics of the actual system components.

Therefore, many kinds of parameters can be considered according to the problem at hand.

1.2 Modelling languages

Among the popular traditional languages for modelling concurrent systems are automata and Petri nets, and their numerous extensions.

Unfortunately, these modelling languages are not completely suited to handle the systems of our interest. Indeed, numbering instances of components is easily achieved with high-level Petri nets such as Coloured Petri Nets (CPNs). In CPNs, the Petri net is enriched with data carried by tokens and modified when firing transitions. These data can very well be a numbering of an instance. Nevertheless, the number of instances is fixed a priori, as opposed to a parameter. Therefore, when the designer wants to analyse several configurations of the system, first the model is built for a given number of instances, then analysed, the number is changed, the model analysed again, and so on.

In Petri nets or automata, there is no specific handling of controllable actions. Hence, to test several options in the design, each of them must be modelled and analysed individually.

Finally, timed versions of Petri nets and automata are widely used, but suffer from the same defaults: values must be known in advance.

Hence, with traditional modelling languages, values are to be set before the analysis is performed, and the process must be repeated for all possible values. It is thus a tedious process which boils down to testing all values one by one, taking a huge amount of time.

1.3 Problems of interest in a parametric setting

The major objective for introducing parameters is to circumvent this repetition of analysis, by introducing parameters in the models. Furthermore, the analysis techniques are suited to find constraints on parameters such that desired properties are satisfied (e.g. the property is satisfied for all values of the parameter $p$ between 1 and 10) or even synthesize the set of all such parameters valuations.

The first advantage of this approach is that answering these questions provides all possible values in a single analysis step. Second, the set of parameters obtained can be infinite (e.g. $p>5$), a result that cannot in general be obtained with an enumerative approach.

1.4 Sources and references

Several sources of information are available to the reader, that provide additional details on the theoretical background, further examples, etc. Among these:

• •

the video of the tutorial presentation: youtube.com/playlist?list=PL9SOLKoGjbeqNcdQVqFpUz7HYqD1fbFIg;

• •

the slides of the tutorial: imitator.fr/tutorials/PN17/;

• •

the exercises with IMITATOR (imitator.fr/tutorials/PN17/) and Roméo (romeo.rts-software.org/doc/tutorial.html);

• •

the extensive literature that is referenced.

Outline.

In Section 2, we first consider parameters as unknown constants in timed automata, i.e. Parametric Timed Automata [AHV93]. We review decidability results, and report on decidable subclasses. Then, in Section 3, we consider parameters as unknown probabilities in Parametric Interval Markov Chains [DLP16]. Section 4 deals with parameters that are unknown numbers of tokens in Petri nets, yielding Parametric Time Petri Nets [Dav+15, Dav+17]. As a last formalism, we also consider in Section 5 the synthesis of actions (seen as Boolean parameters) [KMP15, KP15]. Finally we review some verification tools in Section 6.

2 Parametric Timed Automata

Classical qualitative model checking, implemented in powerful tools used successfully in industry, falls short when quantitative aspects of systems such as time, energy, probabilities, etc., are to be verified. Timed automata [AD94] allow for modeling and verifying time critical concurrent systems. This seminal work [AD94] received the CAV conference award in 2008, and since then numerous works have extended the formalism of timed automata.

However, despite of some success, (timed) model checking can be seen as slightly disappointing. There are two main reason of that:

the binary response to properties satisfaction may not be informative enough, and 2. 2.

the insufficient abstraction to cater for tuning and scalability of systems.

Adding parameters offers a higher level of abstraction by allowing unknown constants in a model. Parameters can be used to model unknown timing constants of timed systems. This approach has the following advantages:

• •

it becomes possible to verify a system at an earlier design stage, when not all timing constants are known with full certainty.

• •

it allows designers to cope with uncertainty even at runtime: some timings constants (e.g. periods of a real-time system) may be known up to a given precision only (e.g. given with an interval of confidence), and parameters can model this imprecision.

Parametric timed automata [AHV93] are an extension of timed automata where timing constants can become unknown, i.e. parameters. They represent a particularly expressive formalism: in fact, its expressiveness is Turing-complete [ALR16] and all non-trivial problems related to parametric timed automata are undecidable. For example, the mere existence of a parameter valuation for which there exists a run reaching some location is undecidable (see e.g. [And19a] for a survey).

Parametric timed automata suffer from negative decidability results, but they still remain a quite powerful formalism. They can be used to address robustness (in the sense of possibly infinitesimal variations of timing constants [BMS13]), to model and verify systems with uncertain constants, and to synthesize suitable (possibly unknown) valuations so that the system meets its specification.

In addition, several recent decidability results for subclasses of parametric timed automata (e.g. [BL09, BO14, JLR15, Ben+15, AL17]) has made this formalism more promising, while new algorithmic and heuristic techniques (e.g. [KP12, JLR15, And+15, Aşt+16, Li+17, And+19]) has made the parametric verification for some classes of problems more scalable and complete, or more often terminating.

Verification with parametric timed automata has had important outcomes in various areas, with verification of case studies such as the root contention protocol [Hun+02], Philip’s bounded retransmission protocol [Hun+02], a 4-phase handshake protocol [KP12], the alternating bit protocol [JLR15], an asynchronous circuit commercialised by ST-Microelectronics [Che+09], (non-preemptive) schedulability problems [JLR15], a distributed prospective architecture for the flight control system of the next generation of spacecrafts designed at ASTRIUM Space Transportation [Fri+12], and even analysis of music scores [FJ13].

In this section, we recall the syntax and semantics of parametric timed automata (Section 2.2) and their subclasses (Section 2.3). We introduce theoretical problems of interest (Section 2.4), and review decidability results (Section 2.5).

2.1 Basic notions

Let $\mathbb{N}$, $\mathbb{Z}$, $\mathbb{Q}_{+}$, and $\mathbb{R}_{+}$ denote the sets of non-negative integers, integers, non-negative rational numbers, and non-negative real numbers, respectively.

We first define the notions necessary to deal with clocks. We begin with clock valuations.

Definition 1 (clock valuation)

Let $X=\{x_{1},\dots,x_{H}\}$ be a finite set of clocks, i.e. real-valued variables that evolve at the same rate.

A clock valuation is a function $w:X\rightarrow\mathbb{R}_{+}$.

We identify a clock valuation $w$ with the point $(w(x_{1}),\dots,w(x_{H}))$.

The following notations allow for specifying null clocks, and adding simultaneously the same delay to all clocks.

Notation 1** (clock operations)**

**

• •

We write $X=\vec{0}$ for $\bigwedge_{1\leq i\leq H}x_{i}=0$.

• •

We also use a special zero-clock $x_{0}$, always equal to 0 (as in e.g. **[Hun+02]**).

• •

Given $d\in\mathbb{R}_{+}$, $w+d$ denotes the valuation such that $(w+d)(x)=w(x)+d$, for all $x\in X$.

• •

Given $R\subseteq X$, we define the reset of a valuation $w$, denoted by $[w]_{R}$, as follows: $[w]_{R}(x)=0$ if $x\in R$, and $[w]_{R}(x)=w(x)$ otherwise.

The systems considered comprise a priori unknown timing constants that are thus parameters to be synthesized according to the targeted property.

Definition 2 (timing parameter valuation)

Let $P=\{p_{1},\dots,p_{M}\}$ be a set of timing parameters, i.e. unknown timing constants.

A timing parameter valuation $v$ is a function $v:P\rightarrow\mathbb{Q}_{+}$.

We identify a valuation $v$ with the point $(v(p_{1}),\dots,v(p_{M}))$.

Clocks and parameters are used together and thus can be combined.

Notation 2** (clocks and parameters valuations combined)**

Given a timing parameter valuation $v$ and a clock valuation $w$, we denote by $w|v$ the valuation over $X\cup P$ such that for all clocks $x$, $w|v(x)=w(x)$ and for all timing parameters $p$, $w|v(p)=v(p)$.

The expressions on clocks can concern clock themselves, but also involve parameters and constant delays.

Notation 3** (linear terms)**

**

• •

In the following, let $\mathit{lt}$ denote a linear term over $X\cup P$ of the form $\sum_{1\leq i\leq H}\gamma_{i}x_{i}+\sum_{1\leq j\leq M}\beta_{j}p_{j}+d$, with $x_{i}\in X$, $p_{j}\in P$, and $\gamma_{i},\beta_{j},d\in\mathbb{Z}$.

• •

Let $\mathit{plt}$ denote a parametric linear term over $P$, that is a linear term without clocks (i.e., $\gamma_{i}=0$ for all $i$).

The synthesis of parameters leads to expressing constraints on their values in order to guarantee that the model satisfies the expected properties.

Definition 3 (constraints on clocks and timing parameters)

A constraint $C$ over $X\cup P$ is defined by the following grammar:

[TABLE]

where ${\bowtie}\in\{<,\leq,\geq,>\}$, $\mathit{lt}$ is a linear term.

Definition 4 (constraint satisfaction)

A valuation $w|v$ satisfies a constraint $C$, denoted $w|v\models C$, if the expression obtained by replacing in $C$ each timing parameter by its valuation as in $v$ evaluates to true.

Zones allow for defining convex sets of clocks and timing parameters values.

Definition 5 (zones and parametric guards)

A zone $C$ is a constraint such that each of its linear conjuncts can be written in the form $x_{i}-x_{j}\bowtie\mathit{plt}$, where $x_{i},x_{j}\in X\cup\{x_{0}\}$. A parametric guard $g$ is a zone such that each of its linear conjuncts can be written in the form $x_{i}\bowtie\mathit{plt}$.

Definition 6 (satisfiability)

Given a zone $C$, $w|v\models C$ indicates that valuating each clock variable $x$ with $w(x)$ and each timing parameter $p$ with $v(p)$ within $C$, evaluates to true. Zone $C$ is satisfiable if $\exists w,v\text{ s.t.\ }w|v\models C$.

Time elapsing can be obtained by adding a new variable to all clocks, ensuring that this variable is non-negative, and eliminating it (see, e.g. [And+09]).

Definition 7 (time elapsing of a zone)

The time elapsing of a zone $C$, denoted by $C^{\nearrow}$, is the constraint over $X\cup P$ obtained from $C$ by delaying all clocks by any arbitrary amount of time.

That is,

[TABLE]

2.2 Syntax and semantics

2.2.1 Syntax

Definition 8 (parametric timed automaton [AHV93])

A parametric timed automaton (PTA) is a tuple $\mathcal{A}=(\Sigma,L,l_{0},F,X,P,I,E)$, where:

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

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

$l_{0}\in L$ is the initial location, 4. 4.

$F\subseteq L$ is a set of final or accepting locations, 5. 5.

$X$ is a finite set of clocks, 6. 6.

$P$ is a finite set of parameters, 7. 7.

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

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

Given a parameter valuation $v$, we denote by $v(\mathcal{A})$ the non-parametric timed automaton where all occurrences of each parameter $p_{i}$ have been replaced by $v(p_{i})$. If $v(\mathcal{A})$ is such that all constants in guards and resets are integers, then $v(\mathcal{A})$ is a timed automaton [AD94]. In the following, we refer to any structure $v(\mathcal{A})$ as a timed automaton, by assuming a rescaling of the constants: by multiplying all constants in $v(\mathcal{A})$ by the least common multiple of their denominators, we obtain an equivalent (integer-valued) timed automaton.

Example 1

Consider the coffee machine in Fig. 1, modelled using a PTA with 4 locations, 2 clocks ({\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{1}} and {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}) and 3 parameters ({\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{1}},{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}},{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{3}}). Invariants are boxed. The only accepting location (with a double border) is $\mathrm{done}$. Observe that all guards and invariants are simple constraints.

The machine can initially be idle for an arbitrarily long time. Then, whenever the user presses the (unique) button (action {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{press}}), the PTA enters location $\mathrm{add\_sugar}$, resetting both clocks. The machine can remain in this location as long as the invariant ({\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}}) is satisfied; there, the user can add a dose of sugar by pressing the button (action {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{press}}), provided the guard ({\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{1}}\geq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{1}}) is satisfied, which resets {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{1}}. That is, the user cannot press twice the button (and hence add two doses of sugar) within a time less than {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{1}}. Then, {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}} time units after the machine left the idle mode, a cup is delivered (action {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{cup}}), and the coffee is being prepared; eventually, {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}} time units after the machine left the idle mode, the coffee (action {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{coffee}}) is delivered. Then, after 10 time units, the machine returns to the idle mode—unless a user again requests a coffee by pressing the button.

2.2.2 Concrete Semantics

Definition 9 (Concrete semantics of a TA)

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

• •

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

• •

$s_{0}=(l_{0},\vec{0})$, and

• •

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

• –

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

• –

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

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

Given a TA $v(\mathcal{A})$ with concrete semantics $(S,s_{0},{\rightarrow})$, we refer to the states of $S$ as the concrete states of $v(\mathcal{A})$. A (concrete) run of $v(\mathcal{A})$ is a possibly infinite alternating sequence of concrete states of $v(\mathcal{A})$ and edges starting from the initial concrete state $s_{0}$ of the form $s_{0}\stackrel{{\scriptstyle e_{0}}}{{\mapsto}}s_{1}\stackrel{{\scriptstyle e_{1}}}{{\mapsto}}\cdots\stackrel{{\scriptstyle e_{m-1}}}{{\mapsto}}s_{m}\stackrel{{\scriptstyle e_{m}}}{{\mapsto}}\cdots$, such that for all $i=0,1,\dots$: $e_{i}\in E$, and $(s_{i},e_{i},s_{i+1})\in{\mapsto}$. Given a state $s=(l,w)$, we say that $s$ is reachable (or that $v(\mathcal{A})$ reaches $s$) if $s$ belongs to a run of $v(\mathcal{A})$. By extension, we say that $l$ is reachable in $v(\mathcal{A})$, if there exists a state $(l,w)$ that is reachable. By extension, given a set of locations $T\subseteq L$ ($T$ stands for “target”), we say that $T$ is reachable in $v(\mathcal{A})$, if there exists a location $l\in T$ that is reachable in $v(\mathcal{A})$. Given a set of locations $T\subseteq L$, we say that a run stays in $T$ if all of its states $(l,w)$ are such that $l\in T$.

A maximal run is a run that is either infinite (i.e. contains an infinite number of discrete transitions), or that cannot be extended by a discrete transition. A maximal run is deadlocked if it is finite, i.e. contains a finite number of discrete transitions. By extension, we say that a TA is deadlocked if it contains at least one deadlocked run.

Example 2

Consider again the PTA modeling a coffee machine in Fig. 1. Let $v$ be the parameter valuation such that v({\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{1}})=1, v({\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}})=5 and v({\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{3}})=8.

Given a clock valuation $w$, we denote it by (w({\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{1}}),w({\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}})). For example, $(0,4.2)$ denotes that w({\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{1}})=0 and w({\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}})=4.2.

The following sequence is a concrete run of $v(\mathcal{A})$.

\big{(}{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{idle}},(0,0)\big{)}\stackrel{{\scriptstyle{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{press}}}}{{\mapsto}}\big{(}{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{add\_sugar}},(0,0)\big{)}\stackrel{{\scriptstyle{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{press}}}}{{\mapsto}}\big{(}{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{add\_sugar}},(0,1.78)\big{)}\stackrel{{\scriptstyle{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{press}}}}{{\mapsto}}\big{(}{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{add\_sugar}},(0,4.2)\big{)}\stackrel{{\scriptstyle{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{cup}}}}{{\mapsto}}\big{(}{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{preparing\_coffee}},(0.8,5)\big{)}\stackrel{{\scriptstyle{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{coffee}}}}{{\mapsto}}\big{(}{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{done}},(0,8)\big{)}\stackrel{{\scriptstyle{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{press}}}}{{\mapsto}}\big{(}{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{add\_sugar}},(0,0)\big{)}

As an abuse of notation, we write above each arrow the action name (instead of the edge), as edges are unnamed in Fig. 1.

This concrete run is not maximal (it could be extended).

2.2.3 Language of timed automata

Let $(l_{0},w_{0})\stackrel{{\scriptstyle e_{0}}}{{\mapsto}}(l_{1},w_{1})\stackrel{{\scriptstyle e_{1}}}{{\mapsto}}\cdots\stackrel{{\scriptstyle e_{m-1}}}{{\mapsto}}(l_{m},w_{m})\stackrel{{\scriptstyle e_{m}}}{{\mapsto}}\cdots$ be a (finite or infinite) run of a TA $v(\mathcal{A})$. The associated untimed word is $\sigma_{0}\sigma_{1}\cdots\sigma_{m}\cdots$, where $\sigma_{i}$ is the action of edge $e_{i}$, for all $i\geq 0$; the associated trace111This is a non-standard definition of traces (compared to e.g. [Gla90]), but we keep this term as it is used in e.g. [And+09, AM15]. is $l_{0}\sigma_{0}l_{1}\sigma_{1}l_{2}\cdots\sigma_{m}l_{m+1}\cdots$

Given a run $(l_{0},w_{0})\stackrel{{\scriptstyle e_{0}}}{{\mapsto}}(l_{1},w_{1})\stackrel{{\scriptstyle e_{1}}}{{\mapsto}}\cdots\stackrel{{\scriptstyle e_{m-1}}}{{\mapsto}}(l_{m},w_{m})$, we say that this run is accepting if $l_{m}\in F$.

We define the untimed language as the set of all untimed words associated with accepting runs of a TA.

Definition 10 (untimed language of a TA)

Given a PTA $\mathcal{A}=(\Sigma,L,l_{0},F,X,P,I,E)$, and a parameter valuation $v$, the untimed language of $v(\mathcal{A})$, denoted by $\mathsf{UL}(v(\mathcal{A}))$, is the set of untimed words associated with all accepting runs of $v(\mathcal{A})$.

We define the trace set as the set of traces associated with the accepting runs.

Definition 11 (trace set of a TA)

Given a PTA $\mathcal{A}=(\Sigma,L,l_{0},F,X,P,I,E)$, and a parameter valuation $v$, the trace set of $v(\mathcal{A})$ is the set of traces associated with all accepting runs of $v(\mathcal{A})$.

Example 3

Consider again the PTA $\mathcal{A}$ modeling a coffee machine in Fig. 1. Let $v$ be the parameter valuation such that v({\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{1}})=1, v({\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}})=5 and v({\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{3}})=8.

The untimed language of $v(\mathcal{A})$ can be described as follows:

[TABLE]

where {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{\sigma}}^{[a,b]}, {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{\sigma}}^{?}, {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{\sigma}}^{*} denote between $a$ and $b$ occurrences, zero or one occurrence, and zero or more occurrence(s) of {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{\sigma}}, respectively.

The trace set of $v(\mathcal{A})$ can be described as follows:

[TABLE]

2.2.4 Symbolic semantics

Let us now recall the symbolic semantics of PTAs (see e.g. [Hun+02, And+09, JLR15]).

Definition 12 (Symbolic state)

A symbolic state is a pair $(l,C)$ where $l\in L$ is a location, and $C$ its associated parametric zone.

Definition 13 (Symbolic semantics)

Given a PTA $\mathcal{A}=(\Sigma,L,l_{0},F,X,P,I,E)$, the symbolic semantics of $\mathcal{A}$ is the labelled transition system called parametric zone graph $\mathcal{PZG}=(E,\mathbf{S},\mathbf{s}_{0},{\Rightarrow})$, with

• •

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

• •

\mathbf{s}_{0}=\big{(}l_{0},(\bigwedge_{1\leq i\leq H}x_{i}=0)^{\nearrow}\land I(l_{0})\big{)}, and

• •

\big{(}(l,C),e,(l^{\prime},C^{\prime})\big{)}\in{\Rightarrow} if $e=(l,g,\sigma,R,l^{\prime})$ and

[TABLE]

with $C^{\prime}$ satisfiable.

That is, in the parametric zone graph, nodes are symbolic states, and arcs are labelled by edges of the original PTA.

If \big{(}(l,C),e,(l^{\prime},C^{\prime})\big{)}\in{\Rightarrow}, we write $\mathsf{Succ}(\mathbf{s},e)=(l^{\prime},C^{\prime})$.

A graphical illustration of the computation of $\mathsf{Succ}$ is given in Fig. 2.222This figure comes from [AS13], itself coming from an adaptation of a figure by Ulrich Kühne. Starting from the parametric zone $C$, it is intersected with guard $g$, leading to the parametric values that allow for taking the transition. Then the necessary clocks are reset. However, for the transition to be taken, the new values thus obtained must satisfy the invariant of the target location, $I(l^{\prime})$. After this, when in $l^{\prime}$, time can elapse as long as the invariant still holds, leading to the new zone $C^{\prime}$.

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

Example 4

Consider again the coffee machine example in Fig. 1. A (non-maximal) symbolic run is as follows:

\big{(}{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{idle}},{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{1}}={\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}\land{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{1}}\geq 0\big{)}\stackrel{{\scriptstyle{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{press}}}}{{\Rightarrow}}\big{(}{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{add\_sugar}},{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{1}}={\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}\land 0\leq{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}}\big{)}

\stackrel{{\scriptstyle{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{press}}}}{{\Rightarrow}}\big{(}{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{add\_sugar}},{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{1}}\leq{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}-{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{1}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}}\land 0\leq{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}}\big{)}

\stackrel{{\scriptstyle{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{press}}}}{{\Rightarrow}}\big{(}{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{add\_sugar}},2\times{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{1}}\leq{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}-{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{1}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}}\land 0\leq{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}}\big{)}

\stackrel{{\scriptstyle{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{cup}}}}{{\Rightarrow}}\big{(}{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{preparing\_coffee}},2\times{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{1}}\leq{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}-{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{1}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}}\land{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}}\leq{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{3}}\big{)}

\stackrel{{\scriptstyle{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{coffee}}}}{{\Rightarrow}}\big{(}{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{done}},0\leq{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{1}}\leq 10\land{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}-{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{1}}={\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{3}}\land 2\times{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{1}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{3}}\big{)}

\stackrel{{\scriptstyle{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{press}}}}{{\Rightarrow}}\big{(}{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{add\_sugar}},{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{1}}={\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}\land 0\leq{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}}\land 2\times{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{1}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{3}}\big{)}

(For sake of readability, we use action names instead of edges along the transitions.)

The parametric zone graph of this example is infinite.

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

Two important results (see e.g. [Hun+02]) relate the concrete and the symbolic semantics, and are recalled below using our syntax. They provide a sort of equivalence between symbolic parametric zones and concrete runs. That is, they guarantee that the zones correspond to feasible runs (correctness) and that each run is represented by a zone (completeness).

Lemma 1 ([Hun+02, Proposition 3.17])

For each parameter valuation $v$ and clock valuation $w$, if there is a symbolic run in $\mathcal{A}$ reaching state $(l,C)$, with $w\models v(C)$, then there is an equivalent concrete run in $v(\mathcal{A})$ reaching state $(l,w)$.

Lemma 2 ([Hun+02, Proposition 3.18])

For each parameter valuation $v$ and clock valuation $w$, if there is a concrete run in $v(\mathcal{A})$ reaching state $(l,w)$, then there is an equivalent symbolic run in $\mathcal{A}$ reaching a state $(l,C)$ such that $w\models v(C)$.

2.3 Subclasses of PTAs

Lower-bound/upper-bound parametric timed automata (L/U-PTAs), proposed in [Hun+02], restrict the use of parameters in the model.

Definition 14 (L/U-PTA)

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

In [BL09], two additional subclasses are introduced: L-PTAs (resp. U-PTAs) are PTAs with only lower-bound (resp. upper-bound) parameters.

L/U-PTAs enjoy a well-known monotonicity property [Hun+02]: increasing upper-bound parameters or decreasing lower-bound parameters can only add behaviours.

Example 5

Consider again the coffee machine in Fig. 1, modelled using a PTA $\mathcal{A}$. This PTA is not an L/U-PTA; indeed, in the guard {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}={\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}} (resp. {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}={\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{3}}), {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}} (resp. {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{3}}) is compared with clocks both as a lower-bound and as an upper-bound. (Recall that $=$ stands for $\leq$ and $\geq$.)

However, if one replaces {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}={\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}} with {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}} and {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}={\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{3}} with {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{3}}, then $\mathcal{A}$ becomes an L/U-PTA with lower-bound parameter {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{1}} and upper-bound parameters \{{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}},{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{3}}\}. Note that equalities are not forbidden in L/U-PTAs (e.g. {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{1}}=10), but only equalities involving parameters are.

Several case studies fit into the class of L/U-PTAs: the root contention protocol, the bounded retransmission protocol and the Fischer mutual exclusion protocol are all modelled with L/U-PTAs in [Hun+02]; in [Hun+02, KP12], both the Fischer mutual exclusion protocol and a producer-consumer are verified using L/U-PTAs. Interestingly, the two case studies of the seminal paper on PTAs [AHV93] (viz. a toy train gate controller model and a model of Fischer mutual exclusion protocol) are also L/U-PTAs, although the concept of L/U-PTAs had not yet been proposed at that time. In addition, most models of asynchronous circuits with bi-bounded delays (i.e. where each delay between the change of an input signal and the change of the corresponding output is a parametric interval) can be modelled using L/U-PTAs.

We will also consider bounded PTAs, i.e. PTAs with a bounded parameter domain that assigns to each parameter an infimum and a supremum, both integers.

Definition 15 (bounded PTA)

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

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

We define similarly bounded L/U-PTAs.

2.4 Decision and computation problems

2.4.1 TCTL

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

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

[TABLE]

A reads “always”, E reads “exists”, and U reads “until”.

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

Definition 16 (Semantics of TCTL)

Given a TA $v(\mathcal{A})$, the following clauses define when a state $s_{i}$ of its timed transition system $(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\textsf{E}{}\varphi\textsf{U}{}_{\bowtie c}\psi$ if there is a maximal run $\rho$ in $v(\mathcal{A})$ with $\sigma=s_{i}\stackrel{{\scriptstyle e_{i}}}{{\mapsto}}\cdots\stackrel{{\scriptstyle e_{j-1}}}{{\mapsto}}s_{j}$ ($i<j$) a prefix of $\rho$ s.t. $s_{j}\models\psi$, $\mathsf{time}(\sigma)\bowtie c$, and $\forall k,i\leq k<j:s_{k}\models\varphi$ 2. 2.

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

where, given a concrete run $\rho$, $\mathsf{time}(\rho)$ gives the total sum of the delays $d$ along $\rho$.

In $\textsf{E}{}\varphi\textsf{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 $\mathcal{A}$ and a TCTL formula $\varphi$, we write $v(\mathcal{A})\models\varphi$ when $s_{0}\models\varphi$.

2.4.2 Decision problems

Emptiness and universality of the valuations set.

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

$\mathcal{P}$**-emptiness problem:

**Input: A PTA $\mathcal{A}$ and an instance $\phi$ of $\mathcal{P}$

Problem: Is the set of parameter valuations $v$ such that $v(\mathcal{A})$ satisfies $\phi$ empty?

$\mathcal{P}$**-universality problem:

**Input: A PTA $\mathcal{A}$ and an instance $\phi$ of $\mathcal{P}$

Problem: For all parameter valuations $v$, does $v(\mathcal{A})$ satisfy $\phi$?

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

• •

reachability (EF333The names “EF”, “AF”, “EG” come from the TCTL syntax, and are consistent with the notations introduced in [JLR15] and subsequently used in further papers (such as [ALR16, AL17]). ): given a TA $v(\mathcal{A})$, is there at least one run of $v(\mathcal{A})$ that reaches a given location? That is, EF-emptiness asks: “is the set of parameter valuations $v$ such that the TA $v(\mathcal{A})$ reaches a given location empty?” And EF-universality asks: “are all parameter valuations such that the corresponding TA reaches a given location?”

• •

unavoidability (AF): given a TA $v(\mathcal{A})$, do all runs of $v(\mathcal{A})$ eventually reach a given location?

• •

EG: given a TA $v(\mathcal{A})$ and a subset $T$ of its locations, is there at least one maximal run of $v(\mathcal{A})$ that always stays in $T$?

• •

AG: given a TA $v(\mathcal{A})$ and a subset $T$ of its locations, do all runs of $v(\mathcal{A})$ stay in $T$?

• •

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

• •

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

Note that AF-emptiness is equivalent to EG-universality, while AG-emptiness is equivalent to EF-universality.

We will finally consider the following two additional emptiness problems:

**Language-preservation-emptiness problem:

**Input: A PTA $\mathcal{A}$ and a parameter valuation $v^{\prime}$

Problem: Is the set of parameter valuations $v$ such that $v\neq v^{\prime}$ and for which $v(\mathcal{A})$ has the same untimed language as $v^{\prime}(\mathcal{A})$ empty?

**Trace-preservation-emptiness problem:

**Input: A PTA $\mathcal{A}$ and a parameter valuation $v^{\prime}$

Problem: Is the set of parameter valuations $v$ such that $v\neq v^{\prime}$ and for which $v(\mathcal{A})$ has the same set of traces as $v^{\prime}(\mathcal{A})$ empty?

2.4.3 Computation problem

Additionally, we define the following computation problem:

$\mathcal{P}$**-synthesis problem:

**Input: A PTA $\mathcal{A}$ and an instance $\phi$ of $\mathcal{P}$

Problem: Compute the parameter valuations such that $v(\mathcal{A})$ satisfies $\phi$.

Example 6

Let us exemplify some decision and computation problems for the coffee machine PTA in Fig. 1. Assume the unique target location is $\mathrm{done}$, i.e. T=\{{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{done}}\}.

EF-emptiness asks whether the set of parameter valuations that can reach location $\mathrm{done}$ for some run is empty, i.e. there is an execution in which the coffee is not delivered. This is false (e.g. {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{1}}=1, {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}}=2, {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{3}}=3 can reach $\mathrm{done}$).

EF-universality asks whether all parameter valuations can reach location $\mathrm{done}$ for some run, i.e. all executions allow for delivering the coffee, regardless of the parameters valuation. This is false (no parameter valuation such that {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}}>{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{3}} can reach $\mathrm{done}$).

AF-emptiness asks whether the set of parameter valuations that can reach location $\mathrm{done}$ for all runs is empty, i.e. if there is some parameters valuation for which coffee delivery is not guaranteed. This is false (e.g. {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{1}}=1, {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}}=2, {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{3}}=3 cannot avoid $\mathrm{done}$).

EF-synthesis consists in synthesizing all valuations for which a run reaches location $\mathrm{done}$, i.e. identifies all parameters valuations for which a coffee will eventually be delivered. The resulting set of valuations is 0\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{3}}\leq 10\land{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{1}}\geq 0.

2.5 Decidability

2.5.1 The general class of PTAs

With the rule of thumb that all problems are undecidable for PTAs, we review the decidability of the aforementioned problems.

• •

EF-emptiness was shown to be undecidable [AHV93], with different flavours and settings: for a single bounded parameter [Mil00], for a single rational-valued or integer-valued parameter [Ben+15], with only one clock compared to parameters [Mil00], or with strict constraints only [Doy07].

• •

AF-emptiness was shown undecidable in [JLR15].

• •

AG-emptiness was shown undecidable in [ALR16].

• •

EG-emptiness (as well as EC and ED) were shown undecidable in [AL17].

• •

The language and trace-preservation problems were shown undecidable in [AM15].

A complete survey is available in [And19a].

Following the very negative results for PTAs, subclasses have been proposed. We review some in the following.

2.5.2 The class of L/U-PTAs

A main decidability result.

The first (and main) positive result for L/U-PTAs is the decidability of the EF-emptiness problem [Hun+02]. L/U-PTAs benefit from the following interesting monotonicity property: increasing the value of an upper-bound parameter or decreasing the value of a lower-bound parameter necessarily relaxes the guards and invariants, and hence can only add behaviours. Therefore, checking the EF-emptiness of an L/U-PTA can be achieved by replacing all lower-bound parameters with 0, and all upper-bound parameters with a sufficiently large constant; this yields a non-parametric TA, for which emptiness is PSPACE-complete [AD94]. This procedure is not only sound but also complete.

Undecidability results.

The first undecidability results for L/U-PTAs are shown in [BL09]: the constrained EF-emptiness problem and constrained EF-universality problem (for infinite runs acceptance properties) are undecidable for L/U-PTAs. By constrained it is meant that some parameters of the L/U-PTA can be constrained by an initial linear constraint, e.g. {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{1}}\leq 2\times{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}}+{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{3}}. Indeed, using linear constraints, one can constrain an upper-bound parameter to be equal to a lower-bound parameter, and hence build a 2-counter machine using an L/U-PTA. However, when no upper-bound parameter is compared to a lower-bound parameter (i.e. when no initial linear inequality contains both an upper-bound and a lower-bound parameter), these two problems become decidable [BL09]. The exact decidability frontier may have not been found yet: the case where a lower-bound parameter is constrained to be less than or equal to an upper-bound parameter fits in none of the considered cases.

A second negative result is shown in [JLR15]: the AF-emptiness problem is undecidable for L/U-PTAs. This restricts again the use of L/U-PTAs, as AF is essential to show that all possible runs of a system eventually reach a (good) state.

Third, in [AM15], the language- and trace-preservation problems were shown to be undecidable for L/U-PTAs.

Model-checking L/U-PTAs.

In [BL09], a parametric extension of the dense-time linear temporal logic $\mathsf{MITL}_{0,\infty}$ (denoted “$\mathsf{PMITL}_{0,\infty}$”) is proposed; when parameters are used only as lower or upper bound in the formula (to which we refer as L/U-$\mathsf{PMITL}_{0,\infty}$), satisfiability and model checking are PSPACE-complete; this is obtained by translating the formula into an L/U-automaton and checking an infinite acceptance property.

Then, in [DLN15], an extension of MITL allowing parametric linear expressions in bounds is proposed (yielding PMITL). Two sets of (integer-valued) parameter valuations are considered:

the set of valuations for which a PMITL formula is satisfiable, i.e. for which there exists a timed sequence (possibly belonging to a given L/U-PTA) satisfying it, and 2. 2.

the set of valuations for which a PMITL formula is valid, i.e. for which all timed sequences (possibly belonging to a given L/U-PTA) satisfy it.

Under some assumptions, the emptiness and universality of the valuation set for which a PMITL property is satisfiable or valid (possibly w.r.t. a given L/U-PTA) are decidable, and EXPSPACE-complete. Essential assumptions for decidability include the fact that parameters should be used with the same polarity (positive or negative coefficient, as lower or upper bound in the intervals) within the entire PMITL formula, and each interval can only use parameters in one of the endpoints. Additional assumptions include that no interval of the PMITL formula should be punctual (nor empty), and linear parametric expressions are only used in right endpoints of the intervals (single parameters can still be used as left endpoints). In addition, two fragments of PMITL are showed to be in PSPACE, including one that allows for expressing parameterized response (“if an event occurs, then another event shall occur within some possibly parametric time interval”).

Finally, we showed that the emptiness-problem using nested quantifiers (i.e. beyond EF, EG, AF, AG) automatically leads to the undecidability, even for the very restricted class of U-PTAs with a single parameter (that can even be integer-valued) [ALR18]. In other words, the nested TCTL emptiness problem is undecidable for U-PTAs. We may wonder if the timed aspect of TCTL (and notably the urgency required by the TCTL formula $\textsf{EG}\textsf{AG}_{=0}$) is responsible for the undecidability. In fact, it is not, and we could modify the proof to show that CTL itself leads to undecidability, i.e. that EGAX-emptiness is undecidable.

Intractability of the synthesis.

A very disappointing result concerning L/U-PTAs is shown in [JLR15]: despite decidability of the underlying decision problems (EF-emptiness and EF-universality), the solution to the EF-synthesis problem for L/U-PTAs, if it can be computed, cannot be represented using a formalism for which the emptiness of the intersection with equality constraints is decidable. The proof relies on the undecidability of the constrained emptiness problem of [BL09]. A very annoying consequence is that such a solution cannot be represented as a finite union of polyhedra (since the emptiness of the intersection with equality constraints is decidable).

Liveness.

The EG-emptiness problem stands at the frontier between decidability and undecidability for the class of L/U-PTAs: while this problem is decidable for L/U-PTAs with a bounded parameter domain with closed bounds, it becomes undecidable if either the assumption of boundedness or of closed bounds is lifted [AL17].

The deadlock-existence emptiness problem is undecidable, even for the restricted class of closed bounded L/U-PTAs [AL17].

In contrast to deadlock-freeness that is consistently undecidable, and to EG-emptiness for which the frontier between decidability and undecidability is thin, the existence of a parameter valuation for which there exists at least one infinite run (EC-emptiness) is consistently decidable for L/U-PTAs [AL17].

2.5.3 The power of integer points

Following works related integer clock and parameter valuations with decidability in [JLR15], we introduced in [ALR16] integer-points parametric timed automata (IP-PTAs for short), i.e. a subclass of PTAs in which any symbolic state contains at least one integer point.

Definition 17

A PTA $\mathcal{A}$ is an integer points PTA (in short IP-PTA) if, in any reachable symbolic state $(l,C)$ of $\mathcal{A}$, $C$ contains at least one integer point, i.e. $\exists v:P\to\mathbb{N},\exists w:X\to\mathbb{N}\text{ s.t. }w|v\models C$.

Example 7

Consider the PTA in Fig. 3(a), containing two clocks {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{1}} and {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x_{2}}, and one parameter {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p}. This PTA is not an IP-PTA. Indeed, as can be seen on its parametric zone graph, the (unique) symbolic state with location {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{l_{3}}} contains only {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p}=\frac{1}{2}, and this symbolic state therefore contains no integer point.

In contrast, the PTA in Fig. 3(b) is an IP-PTA: each zone in its parametric zone graph contains an integer valuation of all parameters. The coffee machine in Fig. 1 (which has an infinite parametric zone graph) is also an IP-PTA.

In [ALR16], we studied the expressiveness of IP-PTAs: while the class of IP-PTAs is incomparable with the class of L/U-PTAs, any non-strict L/U-PTA, i.e. with only non-strict inequalities, is an IP-PTA.

Concerning decidability, the only non-trivial general class with a decidability result for EF-emptiness is L/U-PTAs [Hun+02]. We extended this class, by proving that EF-emptiness is decidable for bounded IP-PTAs [ALR16]. However, other studied problems turned out to be undecidable.

2.5.4 Summary

Table 1 summarises the decidability results. It gives from left to right the (un)decidability for U-PTAs, bounded L/U-PTAs (with either closed or open bounds), L/U-PTAs, bounded IP-PTAs, IP-PTAs, bounded PTAs, and PTAs. We review the emptiness of TCTL subformulas (EF, AF, EG, AG), full TCTL, cycle-existence, deadlock-existence and language- and trace-preservation. Decidability is given in green, whereas undecidability is given in italic red. Our contributions are emphasized in bold using a plain background, whereas existing results are depicted using a light background. When several papers in the literature proved the same result, we only give the earliest result, and not necessarily the best (in terms of number of clocks and parameters, or complexity).

Perspective: open subclasses

L-PTAs and U-PTAs [BL09] are very open classes, in the sense that the only known decidability results come from the larger class of PTAs, and no undecidability result was known—with the exception of our recent result concerning TCTL-emptiness [ALR18]. To summarize, the EG-emptiness, AG-emptiness and AF-emptiness problems, as well as the language- and trace-preservation problems, are all undecidable for (general) L/U-PTAs, but remain open for L-PTAs and U-PTAs. Similarly, the EF-synthesis problem (shown intractable for L/U-PTAs in [JLR15] despite the decidability of the EF-emptiness problem) remains open for rational-valued L- and U-PTAs, and would significantly increase the interest of these subclasses if it was shown to be computable.

3 Parametric Interval Markov Chains

Parametric probabilities are useful to capture imprecisions, robustness and dimensioning issues. Hence, in this section we consider Parametric Interval Markov Chains (PIMC).

3.1 Introduction to Parametric Markov Chains

Fig. 4 contains an example of the different flavours of Markov Chains we are addressing in this section. Fig. 4(a) is a Markov chain (MC). As in an automaton, there are states and transitions between them, but these are labelled by probabilities for the transition to occur. For example, from state {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{0}}}, there is a probability of $0.7$ to go to state {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{1}}} and of $0.3$ to go to state {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{2}}}. Therefore, the sum of all probabilities labelling transitions exiting a state must be $1$.

When probabilities are not known in advance, it might still be possible to know an interval to which they belong. Hence, we introduce Interval Markov Chains (IMC), as pictured in Fig. 4(b). The transitions are then no more labelled by a fixed probability but an interval meaning that the probability should be between the lower and the upper bound of the interval. For example, the probability to move from state {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{1}}} to state {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{3}}} is between $0.3$ and $0.5$. The MC in Fig. 4(a) can be seen as an implementation of the IMC in Fig. 4(b) which stands as a specification. Notice that state {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{4}}} does not appear in Fig. 4(a), which is equivalent to having a transition from state {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{2}}} to state {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{4}}} with a probability [math]. Once a probability is chosen in an interval, it imposes constraints on the other probabilities outgoing the same state since they must add up to $1$. An IMC is said to be consistent if it admits at least one implementation.

When the upper or lower bounds are unknown, it is convenient to use parameters. Fig. 4(c) shows a Parametric Interval Markov Chain (PIMC). As compared with the IMC of Fig. 4(b), some of the bounds are replaced with parameters {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p} and {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}q}. Notice that the same parameter occurs at several places in the PIMC, therefore imposing constraints on the interval. For example, from state {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{1}}}, it is possible to stay in this state with a probability between {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}q} and $1$, or to move to state {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{3}}} with a probability between $0.3$ and the same {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}q}. When assigning a valuation to all parameters in a PIMC, we obtain an IMC.

3.2 Markov Chains definitions

We now formally define the different Markov Chain models. These definitions are detailed in [DLP16].

Definition 18 (Markov Chain)

A Markov Chain is a tuple $\mathcal{M}=(S,s_{0},M,A,\linebreak[4]V)$, where $S$ is a finite set of states containing the initial state $s_{0}$, $A$ is a set of atomic propositions, $V:S\rightarrow 2^{A}$ is a labelling function, and $M:S\times S\rightarrow[0,1]$ is a probabilistic transition function such that $\forall s\in S,\sum_{t\in S}M(s,t)=1$.

We now introduce the notation of parameters, and interval ranges that will be used throughout this section. A parameter $p\in P$ is a variable ranging through the interval $[0,1]$. A valuation for $P$ is a function $\psi:P\rightarrow[0,1]$ that associates values with each parameter in $P$. We write $\texttt{Int}_{[0,1]}(P)$ for the set of all closed parametric intervals of the form $[x,y]$ with $x,y\in[0,1]\cup P$. When $P=\emptyset$, we write $\texttt{Int}_{[0,1]}=\texttt{Int}_{[0,1]}(\emptyset)$ to denote closed intervals with real-valued endpoints. Given an interval $I$ of the form $I=[a,b]$, $\texttt{Low}(I)$ and $\texttt{Up}(I)$ respectively denote the lower and upper endpoints of $I$, i.e. $a$ and $b$. Given an interval $I=[a,b]\in\texttt{Int}_{[0,1]}$, we say that $I$ is well-formed whenever $a\leq b$.

The definition of Interval Markov Chains is adapted from [Del+12].

Definition 19 (Interval Markov Chain [Del+12])

An Interval Markov Chain is a tuple $\mathcal{I}=(S,s_{0},\phi,A,V)$, where $S$, $s_{0}$, $A$ and $V$ are as for MCs, and $\phi:S\times S\rightarrow\texttt{Int}_{[0,1]}$ is a transition constraint that associates with each potential transition an interval of probabilities.

The following definition recalls the notion of satisfaction introduced in [Del+12]. Satisfaction (also called implementation in some cases) allows to characterise the set of MCs represented by a given IMC specification. Satisfaction abstracts from the syntactic structure of transitions in IMCs: a single transition in the implementation MC can contribute to satisfaction of more than one transition in the specification IMC, by distributing its probability mass against several transitions. Similarly many MC transitions can contribute to the satisfaction of just one specification transition. This crucial notion is embedded in the so-called correspondence function $\delta$ introduced below. Informally, such a function is given for all pairs of states $(t,s)$ in the satisfaction relation, and associates with each successor state $t^{\prime}$ of $t$ – in the implementation MC – a distribution over potential successor states $s^{\prime}$ of $s$ – in the specification IMC – specifying how the transition $t\rightarrow t^{\prime}$ contributes to the transition $s\rightarrow s^{\prime}$.

Definition 20 (Satisfaction Relation [Del+12])

Let $\mathcal{I}=(S,s_{0},\phi,A,V^{I})$ be an IMC and $\mathcal{M}=(T,t_{0},M,A,V^{M})$ be a MC. A relation $\mathcal{R}\subseteq T\times S$ is a satisfaction relation if whenever $t\mathcal{R}s$,

the labels of $s$ and $t$ agree: $V^{M}(t)=V^{I}(s)$, 2. 2.

there exists a correspondence function $\delta:T\rightarrow(S\rightarrow[0,1])$ such that

1. (a)

for all $t^{\prime}\in T$ such that $M(t,t^{\prime})>0$, $\delta(t^{\prime})$ is a distribution on $S$, 2. (b)

for all $s^{\prime}\in S$, we have $(\sum_{t^{\prime}\in T}M(t,t^{\prime})\cdot\delta(t^{\prime})(s^{\prime}))\in\phi(s,s^{\prime})$, and 3. (c)

for all $t^{\prime}\in T$ and $s^{\prime}\in S$, if $\delta(t^{\prime})(s^{\prime})>0$, then $(t^{\prime},s^{\prime})\in\mathcal{R}$.

We say that state $t\in T$ satisfies state $s\in S$ (written $t\models s$) iff there exists a (minimal) satisfaction relation containing $(t,s)$ and that $\mathcal{M}$ satisfies $\mathcal{I}$ (written $\mathcal{M}\models\mathcal{I}$) iff $t_{0}\models s_{0}$.

The set of MCs satisfying a given IMC $\mathcal{I}$ is written $[{\!}[\mathcal{I}]{\!}]$. Formally, $[{\!}[\mathcal{I}]{\!}]=\{\mathcal{M}\ |\ \mathcal{M}\models\mathcal{I}\}$.

Definition 21

An IMC $\mathcal{I}$ is consistent iff $[{\!}[\mathcal{I}]{\!}]\neq\emptyset$.

Although the satisfaction relation abstracts from the syntactic structure of transitions, we recall the following result from [Del15], that states that whenever a given IMC is consistent, it admits at least one implementation that strictly respects its structure.

Theorem 3.1 ([Del15])

An IMC $\mathcal{I}=(S,s_{0},\phi,A,V)$ is consistent iff it admits an implementation of the form $\mathcal{M}=(S,s_{0},M,A,V)$ where, for all reachable states $s$ in $\mathcal{M}$, it holds that $M(s,s^{\prime})\in\phi(s,s^{\prime})$ for all $s^{\prime}$.

In the following, we say that state $s$ is consistent in the IMC $\mathcal{I}=(S,s_{0},\phi,A,V)$ if there exists an implementation $\mathcal{M}=(S,s_{0},M,A,V)$ of $\mathcal{I}$ in which state $s$ is reachable with a non-zero probability.

We now recall to the notion of Parametric Interval Markov Chain, previously introduced in [Del15].

Definition 22 (Parametric Interval Markov Chain)

A Parametric Interval Markov Chain is a tuple $\mathcal{I}^{P}=(S,s_{0},\phi_{P},A,V,P)$, where $S$, $s_{0}$, $A$ and $V$ are as for IMCs, $P$ is a set of variables (parameters) ranging over $[0,1]$ and $\phi_{P}:S\times S\rightarrow\texttt{Int}_{[0,1]}(P)$ associates with each potential transition a (parametric) interval.

Given a pIMC $\mathcal{I}^{P}=(S,s_{0},\phi_{P},A,V,P)$ and a parameter valuation $\psi:P\rightarrow[0,1]$, we write $\psi(\mathcal{I}^{P})$ for the IMC obtained by replacing $\phi_{P}$ by the function $\phi:S\times S\rightarrow\texttt{Int}_{[0,1]}$ defined by $\forall s,s^{\prime}\in S,\phi(s,s^{\prime})=\psi(\phi_{P}(s,s^{\prime}))$. The IMC $\psi(\mathcal{I}^{P})$ is called an instance of pIMC $\mathcal{I}^{P}$.

Finally, we say that a MC $\mathcal{M}=(T,t_{0},M,A,V^{M})$ implements pIMC $\mathcal{I}^{P}$, written $\mathcal{M}\models\mathcal{I}^{P}$, iff there exists an instance $\mathcal{I}$ of $\mathcal{I}^{P}$ such that $\mathcal{M}\models\mathcal{I}$. We write $[{\!}[\mathcal{I}^{P}]{\!}]$ for the set of MCs implementing $\mathcal{I}^{P}$ and say that a pIMC is consistent iff its set of implementations is not empty.

3.3 Consistency of PIMCs

When considering IMCs, one question of interest is to decide whether it is consistent without computing its set of implementations. This problem has been addressed in [Del+12, Del15], yielding polynomial decision algorithms and procedures that produce one implementation when the IMC is consistent. The same question holds for pIMCs, although in a slightly different setting. [Del15] proposed a polynomial algorithm for deciding whether a given pIMC is consistent, in the sense that it admits at least one parameter valuation for which the resulting IMC is consistent.

In order to decide whether a given IMC is consistent, we need to address the set of potential successors of a given state $s$. Let $\texttt{Succ}(s)$ be the set of states that can be reached from $s$ with a probability interval not reduced to $[0,0]$: $\texttt{Succ}(s)=\{s^{\prime}\in S\ |\ \phi_{P}(s,s^{\prime})\neq[0,0]\}$.

We now introduce the notion of $n$-consistency in the IMC setting and then adapt this notion to pIMCs. In practice, $n$-consistency is defined by induction over the structure of $\mathcal{I}$.

Definition 23 ($n$-consistency)

Let $\mathcal{I}=(S,s_{0},\phi,A,V)$ be an IMC and let $D:S\rightarrow\texttt{Dist}(S)$ be a function that assigns a distribution on $S$ to each state of $\mathcal{I}$. State $s\in S$ is $(n,D)$-consistent iff for all $s^{\prime}\in S$, $D(s)(s^{\prime})\in\phi(s,s^{\prime})$, and, for $n>0$, $D(s)(s^{\prime})>0$ implies $s^{\prime}$ is $(n-1,D)$-consistent.

We say that $s$ is $n$-consistent if there exists $D:S\rightarrow\texttt{Dist}(S)$ such that $s$ is $(n,D)$-consistent.

Definition 23 is thus equivalent to the following intuitive inductive definition: a state $s$ is $n$-consistent iff there exists a distribution $\rho$ satisfying all of its outgoing probability intervals and such that for all $s^{\prime}\in S$, $\rho(s^{\prime})>0$ implies that $s^{\prime}$ is $(n-1)$-consistent.

Theorem 3.2

Given an IMC $\mathcal{I}=(S,s_{0},\phi,A,V)$, $\mathcal{I}$ is consistent iff $s_{0}$ is $|S|$-consistent.

Example 8

Let us consider the example in Fig. 4(b). All states but {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{4}}} are [math]-consistent. Indeed it is possible to find probabilities within the exiting intervals that add up to $1$. It is not the case for state {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{4}}}, which has a probability of $0.6$ to which we should add one that is at least $0.5$, so the sum is at least $1.1$. Then, for state {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{2}}} to be $1$-consistent, it must not have {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{4}}} has a successor. This is possible by choosing [math] as the probability to go from {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{2}}} to {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{4}}}. In the remaining two intervals, choosing probability $0.5$ leads to a sum of $1$. Therefore, state {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{2}}} is $1$-consistent. One can check that all states but {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{4}}} are $n$-consistent, for all $n$.

For the problem of consistency of pIMCs, the aim is not only to decide whether a given pIMC is consistent, but also to synthesise all parameter valuations that ensure consistency of the resulting IMC. For this purpose, we adapt the notion of $n$-consistency defined above to pIMCs.

We first define the local consistency of a state w.r.t. some subset $S^{\prime}$ of its successors: the sum of upper bounds should be greater than $1$, the sum of lower bounds smaller than $1$, and all successors in $S^{\prime}$ have a valid interval.

$LC(s,S^{\prime})=\left[\sum_{s^{\prime}\in S^{\prime}}\texttt{Up}(\phi_{P}(s,s^{\prime}))\geq 1\right]\cap\left[\sum_{s^{\prime}\in S^{\prime}}\texttt{Low}(\phi_{P}(s,s^{\prime}))\leq 1\right]\\ \cap\left[\bigcap_{s^{\prime}\in S^{\prime}}\texttt{Low}(\phi_{P}(s,s^{\prime}))\leq\texttt{Up}(\phi_{P}(s,s^{\prime}))\right]$

Let us start by fixing a set of states $X$ that we want to avoid and then compute the set of valuations $\texttt{Cons}_{n}^{X}(s)$ that ensure $n$-consistency of $s$ through a distribution $\rho$ that avoids states from $X$. Formally, $\texttt{Cons}_{n}^{X}(s)$ is defined as: let $\texttt{Cons}^{X}_{0}(s)=LC(s,\texttt{Succ}(s)\setminus X)\cap\left[\bigcap_{s^{\prime}\in X}\texttt{Low}(\phi_{P}(s,s^{\prime}))=0\right]$ and for $n\geq 1$,

$\texttt{Cons}^{X}_{n}(s)=\left[\bigcap_{s^{\prime}\in\texttt{Succ}(s)\setminus X}\texttt{Cons}_{n-1}(s^{\prime})\right]\cap\left[LC(s,\texttt{Succ}(s)\setminus X)\right]\\ \cap\left[\bigcap_{s^{\prime}\in X}\texttt{Low}(\phi_{P}(s,s^{\prime}))=0\right]$

The set of valuations ensuring $n$-consistency is then the union, for all potential choices of $X$, of $\texttt{Cons}_{n}^{X}(s)$. We need to choose $X$ as a subset of the set $Z(s)$ of states which can be avoided, by transitions that have [math] or a parameter as lower bound. Therefore, we define $\texttt{Cons}_{n}(s)=\bigcup_{X\subseteq Z(s)}\texttt{Cons}^{X}_{n}(s)$.

Theorem 3.3

Given a pIMC $\mathcal{I}^{P}=(S,s_{0},\phi_{P},A,V,P)$ and a parameter valuation $\psi:P\rightarrow[0,1]$, we have $\psi\in\texttt{Cons}_{|S|}(s_{0})$ iff the IMC $\psi(\mathcal{I}^{P})$ is consistent.

Example 9

It is easily shown that the consistency of the PIMC in Fig. 4(c) is [({\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}q}\leq 0.7)\cap({\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}q}\geq 0.3)]\cup({\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}q}=1).

This section has shown the crucial property of consistency in both parametric and non-parametric interval Markov chains. It thus sets the necessary elements before model checking such probabilistic models.

3.4 Further reading

The definitions and properties stated in this section are detailed in [DLP16]. They were revised in [PP18], where both inductive and co-inductive definitions of consistency are given, implemented with forward and backward algorithms. [DLP16] also addresses some properties: consistent avoidability, existential and universal consistent reachability.

4 Parametric Petri Nets

We now consider a parametric extension of Petri nets in which the weights of the arcs can be parameters. This extension was mainly studied in the Ph.D. thesis of Nicolas David [Dav17] and many of those results can also be found in [Dav+15, Dav+17].

Example 10

In order to illustrate the usefulness of this parameterised formalism, we consider the example, taken from [Dav17], of a financial loan. It is modelled in Fig. 5.

In the general case, a client has a certain amount of money, say {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}a}, and is ensured to get income {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}b} every month. To finance his project, the client needs to define with the bank the amount loaned {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}c}, the duration of reimbursement {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}d} (in months) and the amount of each reimbursement {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}e}. At the end of the process, the bank expects to get back the initial amount loaned {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}c} plus the interest {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}f}. The amount of money possessed by the client is depicted in place {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{funds}}. The signature of the contract is symbolised through the firing of transition {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{grantLoan}} which imposes to the bank to loan an amount {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}c} for a term of {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}d} months. Each month, we can fire {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{reimburse}}: the client receives its own income {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}b} that is added to its capital in {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{funds}} and in parallel an amount {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}e} is reimbursed to the bank. When we consider that the reimbursement is finished, we fire {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{endLoan}} that removes the token from {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{lock_{1}}} and allows us to enable the transitions of the second part of this example. We can then check if the bank can get its money back by testing if {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{loanOk}} can be marked and if the bank can get the interest by checking {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{interestOk}} can be marked or both by checking if {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{loanFinished}} can be marked.

With this example in mind, we now proceed to the corresponding formal definitions.

Definition 24 (Parametric Petri Net [Dav+15])

A (marked) parametric Petri Net (PPN) is a tuple $\mathcal{N}=(\mathsf{P},\mathsf{T},\mathbb{P},\mathsf{Pre},\mathsf{Post},m_{0})$ where $\mathsf{P}$ is a finite set of places, $\mathsf{T}$ is a finite set of transitions such that $\mathsf{P}\cap\mathsf{T}=\emptyset$, $\mathbb{P}$ is a finite set of parameters, $\mathsf{Pre}:\mathsf{P}\times\mathsf{T}\rightarrow\mathbb{N}\cup\mathbb{P}$ is the backward incidence function, $\mathsf{Post}:\mathsf{P}\times\mathsf{T}\rightarrow\mathbb{N}\cup\mathbb{P}$ is the forward incidence function, $m_{0}\in\mathbb{N}^{P}$ is the initial marking.

Let $\mathcal{N}$ be a parametric Petri net. A valuation $\vec{v}$ of the parameters of $\mathcal{N}$ is a mapping from $\mathbb{P}$ to $\mathbb{N}$.

We denote by $\vec{v}(\mathcal{N})$ the Petri net obtained by replacing all parameters by the value they are given by $\vec{v}$.

A marking of a (non-parametric) Petri net is a mapping from $\mathsf{P}$ to $\mathbb{N}$. Markings can be compared component by component: $m\geq m^{\prime}$ if $\forall p\in\mathsf{P},m(p)\geq m^{\prime}(p)$.

A transition $t\in\mathsf{T}$ is enabled by marking $m$ if for all $p\in\mathsf{P}$, $m(p)\geq\mathsf{Pre}(p,t)$. A transition $t$ enabled by marking $m$ can be fired, leading to a new marking $m^{\prime}$ defined by $\forall p\in\mathsf{P},m^{\prime}(p)=m(p)-\mathsf{Pre}(p,t)+\mathsf{Post}(p,t)$. We note $m\overset{t}{\rightarrow}m^{\prime}$.

A run in the Petri net is a possibly infinite alternating sequence of markings and transitions $m_{1}t_{1}m_{2}\ldots$ such that $m_{1}=m_{0}$ and for all $i\geq 1$, $m_{i}\overset{t_{i}}{\rightarrow}m_{i+1}$.

4.1 Problems of interest

We extend classic problems defined for Petri nets to the parametric setting. These problems are reachability, coverability, and (un)boundedness.

A marking $m$ is reachable if there exists a finite run $m_{1}t_{1}m_{2}\ldots t_{n}m_{n+1}$ such that $m_{n+1}=m$.

A marking $m$ is coverable if there exists a reachable marking $m^{\prime}$ such that $m^{\prime}\geq m$.

A (non-parametric) Petri net is $k$-bounded if for all reachable markings $m$, we have $\forall p\in\mathsf{P},m(p)\leq k$. It is bounded if there exists some $k$ such that it is $k$-bounded. If a net is not bounded, we say it is unbounded and then for all $B\geq 0$ there exists a place $p$ and a reachable marking $m$ such that $m(p)>B$.

Similarly a Petri net is simultaneously $X$ unbounded [Dem13], for some subset $X$ of $\mathsf{P}$, if for all $B\geq 0$, there exists a reachable marking $m$ such that for all places $p\in X$, we have $m(p)>B$.

We consider two associated parametric decision problems: the existential and the universal problems. In the former we want to decide the existence of a parameter valuation for which some property holds, and in the latter we want to decide if it holds for all the possible parameter valuations. The property in question can be any of those defined above.

For instance, the existential parametric reachability problem asks, given a target marking $m$, if there exists a parameter valuation $\vec{v}$ such that $m$ is reachable in $\vec{v}(\mathcal{N})$. Similarly, the universal coverability problem asks, given a target marking $m$, if for all valuations $\vec{v}$ of the parameters, $m$ is coverable in $\vec{v}(\mathcal{N})$.

We finally define synthesis problems, in which we want to effectively compute the set of all parameter valuations for which some property holds. Note that if we can effectively compute this set, and check its emptiness or universality, then we can also solve the two decision problems above.

4.2 Undecidability Results for Parametric Petri Nets

We start with a few negative results.

Theorem 4.1 ([Dav+15])

The existential and universal parametric coverability, reachability, and (simultaneous) unboundedness problems are undecidable.

This theorem is proved by reducing the halting, and counter-boundedness problems for 2-counter machines [Min67] to those parametric problems for parametric Petri nets. We encode the value of each counter as the number of tokens in a place and we use parametric arcs to test for emptiness of that place (i.e. counter value [math]).

As a consequence, we need to consider meaningful subclasses for which we might obtain some decidability results.

4.3 Subclasses of Parametric Petri Nets

The basic observation guiding us in defining interesting subclasses of PPNs is that, in the 2-counter machine reduction briefly outlined above, we need both a post arc with a parametric weight $a$ and a pre arc with the same parametric weight $a$.

We thus define preT-PPNs, postT-PPNs, and distinctT-PPNs according to whether the parameters are allowed only in pre arcs, in post arcs, or in both but not with the same parameters.

Definition 25 (preT- and postT-PPNs)

A preT-PPN (resp. postT-PPN) is a PPN in which the $\mathsf{Post}$ (resp. $\mathsf{Pre}$) function has the form $\mathsf{P}\times\mathsf{T}\rightarrow\mathbb{N}$.

Definition 26 (distincT-PPNs)

A distinctT-PPN is a PPN in which the set of parameters used in the $\mathsf{Pre}$ function and the set of those used in the $\mathsf{Post}$ function are disjoint.

We could also consider classic Petri nets in which the initial marking is parameterised. The corresponding formalism is called P-PPN. Such a parametric initial marking is easily simulated with an initial transition that has parametric weights in its post arcs and sets the initial marking. Interestingly, it can also be proved that postT-PPNs can be (weakly) simulated by P-PPNs [Dav+15].

Fig. 6 [Dav+15] summarises this hierarchy of subclasses.

4.4 Global Results

We now summarise the current state-of-the art for the study of PPNs. Table 2 gives the decidability results and whenever relevant the complexities for the universal problems, while Table 3 gives them for the existential problems.

In order to establish the decidability results, we use a variety of techniques. The most basic is that preT- and postT-PPNs have a strong monotonicity property [Dav+15]: increasing (resp. decreasing) the value of parameters in a postT-PPN (resp. preT-PPN) can only add behaviours. Second we can reduce universal coverability in preT-PPNs to simultaneous unboundedness, and existential coverability in postT-PPNs to coverability in the $\omega$ Petri nets of [Gee+15]. Both of these reductions can be found in [Dav+17]. Finally, we can adapt the Karp & Miller algorithm [KM69] to preT- and postT-PPNs [Dav17].

Table 4 presents results for the synthesis problem [Dav+17]. In the cases where we can compute the set of adequate valuations (✓), we mostly rely on the use of an algorithm to compute upward-closed sets by Valk and Jantzen [VJ85]. The negative results (✕) come from the fact that the emptiness or the universality of the set cannot be decided as a direct consequence of the undecidability results above, so there is little hope to find a useful representation of that set. The case of distinctT-PPNs is similar in so far as if we can compute the solution and test its intersection with equality constraints we can solve the synthesis problem for any PPN, by replacing parameters used both in pre and post arcs by different parameters (which gives a distinctT-PPN) and then constraining the solution set with equality constraints on these different parameters.

4.5 Conclusion

Parametric Petri nets are a powerful formalism to model flexible systems. In the general case, the interesting problems are undecidable but still useful subclasses can be obtained by restricting the use of parameters. For most of these subclasses, it is possible to actually synthesise the values of the parameters such that the net is unbounded, or such that some marking is coverable. It would nevertheless be interesting to design semi-algorithms or incomplete algorithms for the most expressive cases that do not fit in this restricted setting. A problem also remains open, i.e. the decidability of universal reachability for Petri nets with a parameterised initial marking.

5 Action synthesis

One of the classical approaches to verification and specification of concurrent systems employs Kripke structures as models and branching-time logics such as CTL as property description languages. In contrast to the models presented earlier, Kripke structures allow only for specifying sequential behaviours. Advanced data structures such as Binary Decision Diagrams [Bry86] (BDDs) together with algorithms based on fixed-point specification of CTL enable efficient verification of models whose state spaces exceed $10^{20}$ [Bur+90]. Here, we extend Action-Restricted Computation Tree Logic ARCTL [PR06] and its models with parameters, to obtain a framework that benefits from BDD-based fixed-point algorithms.

5.1 Mixed Transition Systems

Mixed Transition Systems [PR06] (MTS) are essentially Kripke structures with transitions labelled by actions.

Definition 27 (MTS)

Let $\mathit{AP}$ be a set of propositional variables. A Mixed Transition System is a 5-tuple $\mathcal{M}=(\mathcal{S},{s^{0}},{\mathcal{A}},{\mathcal{T}},{\mathcal{L}})$, where:

• •

$\mathcal{S}$ is a finite set of states, and ${s^{0}}\in\mathcal{S}$ is the initial state,

• •

${\mathcal{A}}$ is a non-empty finite set of actions,

• •

${\mathcal{T}}\subseteq\mathcal{S}\times{\mathcal{A}}\times\mathcal{S}$ is a transition relation,

• •

${\mathcal{L}}:\mathcal{S}\to 2^{\mathit{AP}}$ is a (state) valuation function.

We write $s\stackrel{{\scriptstyle a}}{{\to}}s^{\prime}$ if $(s,a,s^{\prime})\in{\mathcal{T}}$. Let $B\subseteq{\mathcal{A}}$ and $\pi=(s_{0},a_{0},s_{1},a_{1},\ldots)$ be a finite or infinite sequence of interleaved states and actions. By $|\pi|$ we denote the number of states in $\pi$ if $\pi$ is finite, and $\omega$ if $\pi$ is infinite. A sequence $\pi$ is a path over $B$ iff $s_{i}\stackrel{{\scriptstyle a_{i}}}{{\to}}s_{i+1}$ and $a_{i}\in B$ for each $i<|\pi|$ and either $\pi$ is infinite or its final state does not have a $B$-successor state in $\mathcal{S}$, i.e. $\pi=(s_{0},a_{0},s_{1},a_{1},\ldots,s_{m})$ for some $m\in\mathbb{N}$ and there is no $s^{\prime}\in\mathcal{S}$ and $a\in B$ such that $s_{m}\stackrel{{\scriptstyle a}}{{\to}}s^{\prime}$. By $\pi_{i}$ we denote the $i$–th state of $\pi$ for all $i\in\mathbb{N}$.

The set of all paths over $B$ in $\mathcal{M}$ is denoted by ${\Pi}(\mathcal{M},B)$, and the set of all paths $\pi\in{\Pi}(\mathcal{M},B)$ starting from a given state $s\in\mathcal{S}$ is denoted by ${\Pi}(\mathcal{M},B,s)$. We typically omit the symbol $\mathcal{M}$, writing ${\Pi}(B)$ and ${\Pi}(B,s)$. By ${\Pi}^{\omega}(B)$ and ${\Pi}^{\omega}(B,s)$ we mean the corresponding sets restricted to the infinite paths only.

Example 11 (MTS)

A MTS with \mathit{AP}=\{{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathbf{p}},{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathbf{safe}}\}, {\mathcal{A}}=\{{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{left}},{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{right}},{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{forw.}},{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{back}}\}, and initial state {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{0}}} is shown in Fig. 7. The path \pi=({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{0}}},{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{left}},{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{1}}},{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{right}},{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{4}}}) belongs to {\Pi}(\{{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{left}},{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{right}}\}), but not to the set {\Pi}(\{{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{left}},{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{right}},{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{back}}\}). The reason is that while $\pi$ is a maximal path over \{{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{left}},{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{right}}\}, it is not maximal over \{{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{left}},{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{right}},{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{back}}\} as it can be extended e.g. into the infinite path \pi^{\prime}=({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{0}}},{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{left}},{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{1}}},{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{right}},{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{4}}},{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{back}},{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{0}}},{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{left}},{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{1}}},{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{right}},{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{4}}},{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{back}},{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{0}}},\ldots)\in{\Pi}(\{{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{left}},{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{right}},{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{back}}\}).

5.2 Parametric Action-Restricted CTL

The main difference between ARCTL and CTL is that in ARCTL each path quantifier is subscripted with a set of actions, e.g. E_{\{{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{left}},{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{right}}\}}G(E_{\{{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{forw.}}\}}F{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathbf{safe}}) may be read as “there exists a path over {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{left}} and {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{right}}, on which it holds globally that a state satisfying $\mathbf{safe}$ is reachable along some path over {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{forw.}}”.

Parametric ARCTL (pmARCTL) extends ARCTL by allowing free variables in place of sets of actions, e.g. E_{Y}G(E_{Z}F{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathbf{safe}}) is a formula of pmARCTL, where $Y$ and $Z$ are free variables.

Definition 28 (pmARCTL syntax)

Let ${\mathcal{A}}$ be a finite set of actions, $\mathcal{X}$ a finite set of variables, $\mathit{AP}$ a set of propositional variables, and ${\mathit{ActSets}}=2^{\mathcal{A}}\setminus\{\emptyset\}$. The set of formulae of pmARCTL is defined by the following grammar:

[TABLE]

where $p\in\mathit{AP}$ and $\alpha\in{\mathit{ActSets}}\cup\mathcal{X}$.

The basic path quantifiers and modalities of pmARCTL have the same meaning as in CTL. The superscript ω restricts the quantification to the infinite paths, whereas the subscript α restricts the quantification to the paths over $\alpha$.

The semantics of pmARCTL is defined w.r.t. parameter valuations, i.e. functions $\upsilon\colon\mathcal{X}\to{\mathit{ActSets}}$. $\mathit{ParVals}$ denotes the set of all parameter valuations. For conciseness, for $\upsilon\in\mathit{ParVals}$ we write $\upsilon(\alpha)=B$ if $\alpha=B\subseteq{\mathcal{A}}$ and $\upsilon(\alpha)=\upsilon(Y)$ if $\alpha=Y\in\mathcal{X}$. Moreover, we assume that $O^{\epsilon}=O$, for $O\in\{E,A,{\Pi}\}$.

Definition 29 (pmARCTL semantics)

Let $\mathcal{M}=(\mathcal{S},{s^{0}},{\mathcal{A}},{\mathcal{T}},{\mathcal{L}})$ be an MTS and $\upsilon\in\mathit{ParVals}$ a parameter valuation. The relation $\models_{\upsilon}$ is defined as follows:

• •

$s\models_{\upsilon}p$ iff $p\in{\mathcal{L}}(s)$,

• •

$s\models_{\upsilon}\neg\phi$ iff $s\not\models_{\upsilon}\phi$,

• •

$s\models_{\upsilon}\phi\lor\psi$ iff $s\models_{\upsilon}\phi$ or $s\models_{\upsilon}\psi$,

• •

$s\models_{\upsilon}E_{\alpha}X\phi$ iff $|\pi|>1$ and $\pi_{1}\models_{\upsilon}\phi$, for some $\pi\in{\Pi}(\upsilon(\alpha),s)$,

• •

$s\models_{\upsilon}E^{r}_{\alpha}G\phi$ iff $\pi_{i}\models_{\upsilon}\phi$ for all $i<|\pi|$, for some $\pi\in{\Pi}^{r}(\upsilon(\alpha),s)$,

• •

$s\models_{\upsilon}E_{\alpha}(\phi\;U\psi)$ iff $\pi_{i}\models_{\upsilon}\psi$ for some $i<|\pi|$ and $\pi_{j}\models_{\upsilon}\phi$ for all $0\leq j<i$, for some $\pi\in{\Pi}(\upsilon(\alpha),s)$,

where $p\in\mathit{AP}$, $\phi,\psi\in\textnormal{pmARCTL}$, $r\in\{\omega,\epsilon\}$, and $\alpha\in{\mathit{ActSets}}\cup\mathcal{X}$.

Example 12

For the MTS in Fig. 7 we have {\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{s_{0}}}\models_{\upsilon}E_{Y}G(E_{Z}F{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathbf{safe}}) iff {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathit{forw.}}\in\upsilon(Z).

5.3 Parameter Synthesis for pmARCTL

In this subsection we show how to recursively characterise pmARCTL using the basic operator of parametric pre-image. These equivalences give rise to fixed-point algorithms that can be implemented using BDDs.

Let $\phi\in\textnormal{pmARCTL}$. Our goal is to construct the function $f_{\phi}\colon\mathcal{S}\to 2^{\mathit{ParVals}}$ s.t. for all $s\in\mathcal{S}$ we have $s\models_{\upsilon}\phi\text{ iff }\upsilon\in f_{\phi}(s)$. In other words, the set $f_{\phi}(s)$ consists of all the parameter valuations that make $\phi$ true in state $s$. Let us show how to build this function recursively, case by case. We omit the treatment of non-parametric modalities as the classical non-parametric methods of symbolic verification carry here with minimal alterations [HR04, RL07].

Boolean Connectives and Non-parametric Modalities.

For each $p\in\mathit{AP}$, $\phi,\psi\in\textnormal{pmARCTL}$ we have $f_{p}(s)=\mathit{ParVals}$ if $p\in{\mathcal{L}}(s)$ and $f_{p}(s)=\emptyset$ otherwise; $f_{\neg\phi}(s)=\mathit{ParVals}\setminus f_{\phi}(s)$; and $f_{\phi\lor\psi}(s)=f_{\phi}(s)\cup f_{\psi}(s)$.

Parametric Pre-image and NeXt.

Let $f\colon\mathcal{S}\to 2^{\mathit{ParVals}}$ be a function. The parametric pre-image of $f$ w.r.t. $Y\in\mathcal{X}$ is defined as the function $\textnormal{parPre}^{\exists}_{Y}(f):\mathcal{S}\to 2^{\mathit{ParVals}}$ s.t. $\textnormal{parPre}^{\exists}_{Y}(f)(s)=\left\{\upsilon\;|\;\exists_{s^{\prime}\in\mathcal{S}}\;\exists_{a\in\upsilon(Y)}\;s\stackrel{{\scriptstyle a}}{{\to}}s^{\prime}\land\upsilon\in f(s^{\prime})\right\}$ for each $s\in\mathcal{S}$. Intuitively, for each $\phi\in\textnormal{pmARCTL}$ in $\textnormal{parPre}^{\exists}_{Y}(f_{\phi})(s)$ we collect all the parameter valuations $\upsilon$ s.t. some state $s^{\prime}$ satisfying $s^{\prime}\models_{\upsilon}\phi$ can be reached by firing in $s\in\mathcal{S}$ an action from $\upsilon(Y)$. We therefore have $f_{E_{Y}X\phi}=\textnormal{parPre}^{\exists}_{Y}(f_{\phi})(s)$

Parametric Temporal Modalities.

We employ the following equations to deal with two versions of the Globally modality:

[TABLE]

The following equation characterises the Until modality:

[TABLE]

We refer to [KMP15, KP15] on how to turn the above equations into fixed-point algorithms and implement them using BDDs. In all the cases, the returned result of running the overall synthesis algorithm for $\phi\in\textnormal{pmARCTL}$ is the BDD that represents $f_{\phi}$. This structure can be then queried for individual parameter valuations; for a certain class of formulae it is possible to synthesise minimal parameter valuations using prime implicants.

As a closing note let us mention that the emptiness problem for pmARCTL, i.e. the question whether $f_{\phi}({s^{0}})\neq\emptyset$ for $\phi\in\textnormal{pmARCTL}$ is known to be NP-complete [KMP15].

6 Tools

In this section, we finally briefly review tools related to the aforementioned formalisms.

6.1 IMITATOR

IMITATOR [And+12] is a software tool for parametric verification and robustness analysis of PTAs augmented with integer variables and stopwatches. Parameters can be used both in the model and in the properties. Verification capabilities include reachability-synthesis, deadlock-freeness-synthesis [And16], non-Zeno model checking [And+17], minimal-time synthesis [And+19], and trace-preservation-synthesis. IMITATOR is fully written in OCaml, and makes use of the Parma Polyhedra Library [BHZ08]. It also features distributed capabilities to run over a cluster.

IMITATOR comes with a benchmarks library available under an open source license [And19].

IMITATOR was successfully used in several application domains such as parametric schedulability analysis of a prospective architecture for the flight control system of the next generation of spacecrafts designed at ASTRIUM Space Transportation [Fri+12], formal timing analysis of music scores [FJ13], verification of software product lines [Lut+17], monitoring logs from the automotive domain against parametric properties [AHW18], and was used to propose a solution to a challenge related to a distributed video processing system by Thales [SAL15].

6.1.1 Related tools

The first tool to support modelling and verification using parametric timed automata was HyTech [HHW97]. In fact, HyTech supports linear hybrid automata (including clocks, parameters, stopwatches and general continuous variables); it can compute the state space, and perform operations (such as intersection, convex hull, difference) between sets of symbolic states. Therefore, it can be used to perform parametric model checking using reachability checking [Ace+98]. HyTech is not maintained anymore, but can still be found online in the form of a standalone binary for Linux.444https://embedded.eecs.berkeley.edu/research/hytech/

In [Hun+02], an extension of Uppaal implementing parametric difference bound matrices (PDBMs) and hence allowing for verification using PTAs is mentioned. However, this tool does not seem to be available anywhere online.

PHAVer [Fre08] is a tool for verifying safety properties of hybrid systems. It notably relies on exact arithmetic (with unlimited precision) using the Parma Polyhedra Library [BHZ08]; on the other hand, it also supports approximations.

SpaceEx [Fre+11] can be seen as a successor of PHAVer, and also tackles verification of reachability properties for hybrid systems. Parameters are not natively supported, but can be encoded using variables that are arbitrarily set up upon system start, and then remain subsequently constant (with a 0-slope). SpaceEx seems to have a lot of interesting recent developments.

PSyHCoS [And+13] allows the synthesis of parameters for a parametric extension of the process algebra Stateful timed CSP [Sun+13], itself a timed extension of Hoare’s communicating sequential processes [Hoa85]. When compared to other formalisms such as (parametric) timed automata, (parametric) stateful timed CSP has the advantage of giving the designer the ability to specify hierarchical systems.

Finally, Symrob is not strictly a tool for synthesis, but allows robustness measurement for timed automata [San15].

6.2 Roméo

Roméo [Lim+09] is a model-checking tool for a selection of hybrid extensions of Petri nets, enriched with discrete variables. In particular, it supports parametric time Petri nets, a formalism shown to be close to PTAs in terms of expressiveness [Bér+05, TLR09]. Roméo allows the use of parametric linear expressions in the time intervals of the transitions, and the addition of linear constraints on the parameters to restrict their domain. Roméo provides a simulator and an integrated model-checker supporting a subset of parametric TCTL (including reachability-synthesis and unavoidability-synthesis), in which “Until” modalities cannot be nested. It also features optimal cost reachability and parameter synthesis for cost-bounded reachability. Roméo implements in particular an original algorithm for integer parameter synthesis using a symbolic (continuous) representation [JLR15]. Roméo is mainly written in C++, and makes use of the Parma Polyhedra Library [BHZ08]. It has been successfully used in a few and diverse case-studies including the analysis of resilience properties in oscillatory biological systems [AMI16]; the synthesis of environment requirements for an aerial video tracking system [Par+16]; and the analysis of operational scenarios modelling in the DGA OMOTESC project [Sei09].

6.3 Spatula

Spatula [Kna, KMP15] implements the theory of action synthesis outlined in Section 5. The tool is written in C++ and employs CUDD library [Som] for representing and manipulating BDDs. Spatula accepts models represented as networks of automata written in a simplified C-like input language and pmARCTL as property description language. The result of synthesis for a given property is a BDD that represents all the valuations that make the property true. Spatula can also list all the minimal valuations (w.r.t. bitwise comparison) for the existential part of the logic.