11institutetext:  Aarhus University, Aarhus, Denmark
11email<EMAIL_ADDRESS>22institutetext: LIPN, CNRS UMR 7030,
Université Sorbonne Paris Nord, Villetaneuse, France
22email: {Baptiste.Fievet<EMAIL_ADDRESS>
# On-The-Fly Algorithm for Reachability in
Parametric Timed Games (Extended Version) ††thanks: This work was partially
supported by CNRS international PhD programme, the CNRS International Research
Network CLoVe and Innovationsfonden Danmark’s DIREC project SIoT (Secure
Internet of Things).

Mikael Bisgaard Dahlsen-Jensen 11 0000-0003-0641-7635 Baptiste Fievet 22
0000-0002-4925-1105
Laure Petrucci 22 0000-0003-3154-5268 Jaco van de Pol 11 0000-0003-4305-0625

###### Abstract

Parametric Timed Games (PTG) are an extension of the model of Timed Automata.
They allow for the verification and synthesis of real-time systems, reactive
to their environment and depending on adjustable parameters. Given a PTG and a
reachability objective, we synthesize the values of the parameters such that
the game is winning for the controller. We adapt and implement the On-The-Fly
algorithm for parameter synthesis for PTG. Several pruning heuristics are
introduced, to improve termination and speed of the algorithm. We evaluate the
feasibility of parameter synthesis for PTG on two large case studies. Finally,
we investigate the correctness guarantee of the algorithm: though the problem
is undecidable, our semi-algorithm produces all correct parameter valuations
“in the limit”.

##  1 Introduction

The seminal model of Timed Automata (TA) [1] equips finite automata with real-
valued clocks, to verify real-time reactive systems. Numerous extensions of TA
have been proposed. Timed Games (TG) [17] distinguish controllable and
uncontrollable actions, to study the interaction of a controller with its
environment (e.g. the plant, an attacker, or a system-under-test). Here, we
focus on reachability objectives, which require a strategy for the controller
to schedule controllable actions such that — no matter which and when
uncontrollable actions are executed by the environment — a desirable state is
reached.

Since precise timing constraints are not always known, one might replace
concrete values by symbolic parameters, to study a whole family of timed
systems. This leads to the model of Parametric Timed Automata (PTA) [2]. The
problem is to find (some or all) values for the parameters such that the
system satisfies a desired property. Most problems on PTA are undecidable [3],
in particular the reachability problem. Several decidable fragments are known,
e.g. by restricting the number of clocks or the positions of the parameters,
as in L/U PTA [13].

This paper tackles the parameter synthesis problem for Parametric Timed Games
(PTG) [14] with reachability objectives. We provide the first implementation
of a semi-algorithm for PTG parameter synthesis. It operates on-the-fly, i.e.
it starts solving the game while the symbolic state space is being generated.
To avoid the generation of the full, potentially infinite, state space, we
also implement several state space reductions. These improve the termination
and efficiency of parameter synthesis. In particular, we lift
inclusion/subsumption from TA to PTG, generalize coverage pruning and losing
state propagation from TG to PTG, and we port cumulative pruning from PTA to
PTG.

Interestingly, unlike the situation in PTA [5] and TG [10], the algorithm for
PTG is not guaranteed to terminate, even if the symbolic state space is
finite. But we claim that if the algorithm terminates, it produces the precise
constraints under which there exists a winning strategy. If the algorithm does
not terminate, the stronger guarantee holds, that (in the limit) it produces
all valid parameter valuations, provided the waiting list is handled fairly.

The implementation allows us to study the feasibility of parameter synthesis
for larger case studies in PTG. In particular, we synthesize parameters for
the correctness of a game version of the Bounded Retransmission Protocol [12]
and a parametric version of the Production Cell [18, 10]. We measure the
effectiveness of the individual pruning heuristics on these case studies. It
appears that the state space reduction techniques are essential for feasible
parameter synthesis.

#### Related Work.

For TG, Maler et al. [17] proposed a strategy synthesis algorithm based on
classical reachability games, handling the uncountable set of clock values
using symbolic regions. Cassez et al. [10] improved the efficiency of TG
strategy synthesis by an on-the-fly algorithm, and working with symbolic
zones, represented by DBMs as implemented in UPPAAL Tiga [8]. Previous work on
PTG initially focused on decidable subcases, like the case for bounded
integers [15] and the fragment of L/U PTG [14, 16]. The latter two papers also
provide semi-algorithms for general PTG, either based on backward fixed points
[16], or an on-the-fly algorithm [14], directly extending the work on Timed
Games [10]. That paper leaves an implementation of the algorithm (and hence an
evaluation on larger case studies) as future work. Our implementation extends
the infrastructure of Imitator [4], which so far could only handle PTA. The
symbolic data structure is based on Parma’s convex Polyhedra Library [7].

#### Contributions.

(1) We provide the first implementation of a parameter synthesis algorithm for
PTG (Sec. 4), and integrate this on-the-fly algorithm in the Imitator toolset
[4] (Sec. 6).

(2) We devise and implement several pruning heuristics to speed up parameter
synthesis (Sec. 5).

(3) We evaluate the feasibility of parameter synthesis for PTG on two large
case studies, and measure the effect of the various pruning techniques (Sec.
6).

(4) We carefully introduce the model (Sec. 2) and solution principles (Sec.
3), pointing out several semantic subtleties, and find that the semi-algorithm
yields all valid parameters in the limit (Sec. 4).

##  2 Model of Parametric Timed Games

A Parametric Timed Game (PTG) is a structure based on timed automata (TA).
Similarly to classical automata, it is composed of locations connected by
discrete transitions. Moreover, it is equipped with clocks. Locations are
associated a condition on clock valuations (invariant) that must be satisfied
while staying in the location. An action in a timed automaton is either to
take a discrete transition or to let some time pass. Discrete transitions have
a guard that must be satisfied in order to take the transition. In a
parametric setting, these conditions use linear terms over clocks and
parameters. Parameters hold an unspecified value, and remain constant during a
run. A discrete transition also has a subset of clocks which are reset when
the transition is taken.

In a two-player timed game, discrete transitions are partitioned between
controllable transitions and uncontrollable environment transitions.

######  Definition 1 (PTG)

A _Parametric Timed Game_ is a tuple of the form
$G=(L,X,P,Act,T_{c},T_{u},\ell_{0},Inv)$ such that

  * •

$L$, $X$, $P$, $Act$ are sets of _locations_ , _clocks_ , _parameters_ ,
_transition labels_.

  * •

$T=T_{c}\cup T_{u}$ is the set of _transitions_ in
$L\times\mathcal{G}(X,P)\times Act\times\mathcal{P}(X)\times L$, partitioned
into sets $T_{c}$ of _controllable_ and $T_{u}$ of _uncontrollable_
transitions of the form
$({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}},g,{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{a}},Y,{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell^{\prime}}})$;
${\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}}$,
${\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell^{\prime}}}$
are source and target locations; $g\in\mathcal{G}(X,P)$ is the guard (see Def.
4);
${\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{a}}$
is the label; $Y$ is the set of clocks to reset.

  * •

${\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell_{0}}}$
is the initial location.

  * •

$Inv\;:\;L\to\mathcal{G}(X,P)$ associates an _invariant_ with each location.

###### Example 1

${\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{preparing\\_coffee}}$${\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{coffee\\_served}}$${\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{adding\\_sugar}}$${\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{idle}}$$\begin{subarray}{c}{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{ask\\_coffee}}\\\
{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{y}}:=0\end{subarray}$$\begin{subarray}{c}{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{y}}<{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{1}}}\\\
{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{ask\\_sugar}}\\\
{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{x}}:=0\end{subarray}$$\begin{subarray}{c}{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{take\\_coffee}}\end{subarray}$$\begin{subarray}{c}{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{3}}}<{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{y}}<{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{4}}}\\\
{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{serve\\_coffee}}\end{subarray}$$\begin{subarray}{c}{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{x}}={\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{2}}}\\\
{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{sugar\\_added}}\end{subarray}$
Figure 1: Parametric Timed Game of the coffee machine.

Fig. 1 shows the example of a coffee machine. The controller represents the
coffee machine and the environment represents the user. Uncontrollable
transitions are depicted as dashed arcs. From
${\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{idle}}$,
the user can
${\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{ask\\_coffee}}$.
It resets clock
${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{y}}$
that will measure the time since the demand. The machine is then
${\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{preparing\\_coffee}}$.
Action
${\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{serve\\_coffee}}$
can happen after
${\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{3}}}$
(parameter featuring the time to pour the coffee) and no later than
${\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{4}}}$
after the request. While the coffee is being prepared, the user may
${\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{add\\_sugar}}$.
Adding sugar does not interrupt the pouring of the coffee and lasts
${\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{2}}}$.
The coffee cannot be served while sugar is being added. A situation that may
arise is that sugar is being added to the coffee when the time limit
${\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{4}}}$
is met, making it impossible for the coffee to be served on time. To avoid
this issue,
${\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{ask\\_sugar}}$
is disabled after waiting
${\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{1}}}$.

Our goal is to synthesize the constraints on parameters
${\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{1}}}$
to
${\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{4}}}$
for the coffee to be timely served. Hence, the initial location is set to
${\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{preparing\\_coffee}}$,
with both clocks at $0$. One possible solution to the problem is
${\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{1}}}+{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{2}}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{4}}}\wedge{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{3}}}<{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{4}}}$.

###  2.1 Semantics of Parametric Timed Games

A _state_ of a PTG consists of a location and a valuation of clocks and
parameters.

######  Definition 2 (valuations)

A _clock valuation_ is a function $v_{X}\in\mathbb{R}_{\geq 0}^{X}$ assigning
a positive real value to each clock. A _parameter valuation_
$v_{P}\in\mathbb{Q}_{\geq 0}^{P}$ assigns a positive rational value to each
parameter. A _valuation of the game_ $G$ is a pair $v=(v_{X},v_{P})$. The set
of all valuations of the game is denoted $V=\mathbb{R}_{\geq
0}^{X}\times\mathbb{Q}_{\geq 0}^{P}$.

A _guard_ is a constraint that can be satisfied by some valuations of the
game.

######  Definition 3 (linear terms)

A _linear term_ over $P$ is a term defined by the following grammar:
$plt\;:=\;k\;|\;k{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p}}\;|\;plt+plt$
where $k\in\mathbb{Q}$ and
${\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p}}\in
P$.

######  Definition 4 (guards)

The set of _guards_ $\mathcal{G}(X,P)$ is the set of formulas defined
inductively by the following grammar:

$\phi\;:=\top\;|\;\phi\land\phi\;|\;{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{x}}\sim
plt\;|\;plt^{\prime}\sim plt\enspace,$

where
${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{x}}\in
X$, ${\sim}\in\\{<;\leq;=;\geq;>\\}$ and $plt$, $plt^{\prime}$ are linear
terms over $P$.

We now introduce the notion of _zone_ which will be used to solve a PTG.

######  Definition 5 (zones)

The set of _parametric zones_ $\mathcal{Z}(X,P)$ is the set of formulas
defined inductively by the following grammar:

$\phi\;:=\;\top\;|\;\phi\land\phi\;|\;{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{x}}\sim
plt\;|\;{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{x}}-{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{y}}\sim
plt\;|\;plt^{\prime}\sim plt\enspace,$

where
${\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{x}},{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{y}}\in
X$, ${\sim}\in\\{<;\leq;=;\geq;>\\}$ and $plt$ and $plt^{\prime}$ are linear
terms over $P$.

Function $v_{P}$ is naturally extended to linear terms on parameters, by
replacing each parameter in the term with its valuation. With $v\models\phi$,
we denote that valuation $v=(v_{X},v_{P})$ _satisfies_ a guard or a zone
$\phi$, which is defined in the expected manner. Zones, guards and invariants
can also be seen as a convex set in the space of valuations of the game by
considering those valuations that satisfy the condition.

Transitions modify clock valuations by letting time pass or resetting clocks.

######  Definition 6 (time delays)

Let $v=(v_{X},v_{P})$ be a valuation of the game and $\delta\geq 0$ a delay.

  * •

$\forall{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{x}}\in
X:(v_{X}+\delta)({\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{x}})=v_{X}({\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{x}})+\delta$

  * •

$v+\delta=(v_{X}+\delta,v_{P})$

######  Definition 7 (clock resets)

Let $v=(v_{X},v_{P})$ be a valuation of the game and $Y\subseteq X$.
$v_{X}[Y:=0]$ is the valuation obtained by resetting the clocks in $Y$, i.e.:

  * •

$\forall{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{x}}\in
Y:v_{X}[Y:=0]({\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{x}})=0$
and
$\forall{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{x}}\in
X\setminus
Y:v_{X}[Y:=0]({\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{x}})=v_{X}({\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{x}})$

  * •

$v[Y:=0]=(v_{X}[Y:=0],v_{P})$

We can now define the semantics of a Parametric Timed Game.

######  Definition 8 (state)

A _state_ of a PTG is a pair
$({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}},v)$
where
${\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}}$
is a location and $v$ a valuation of the game satisfying its invariant:
$v\models
Inv({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}})$.
The _state space_ is then
$\mathbb{S}=\\{({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}},v)\in
L\times V\;|\;v\models
Inv({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}})\\}=\underset{{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}}\in
L}{\bigcup}\;\\{{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}}\\}\times
Inv({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}})\enspace.$

From a state in this state space, timed and discrete transitions can happen.

######  Definition 9 (timed and discrete transitions)

Let $\delta\in\mathbb{R}_{\geq 0}$ be a time delay. A _timed transition_ is a
relation ${\to^{\delta}}\in\mathbb{S}\times\mathbb{S}$ s.t.
$\forall({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}},v),({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell^{\prime}}},v^{\prime})\in\mathbb{S}:({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}},v)\to^{\delta}({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell^{\prime}}},v^{\prime})$
iff
${\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}}={\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell^{\prime}}}$
and $v^{\prime}=v+\delta$.

Let
$t=({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}},g,{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{a}},Y,{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell^{\prime}}})\in
T$ be a transition. A _discrete transition_ is a relation
${\to^{t}}\in\mathbb{S}\times\mathbb{S}$ s.t.
$\forall({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}},v),({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell^{\prime}}},v^{\prime})\in\mathbb{S}:({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}},v)\to^{t}({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell^{\prime}}},v^{\prime})$
iff $v\models g$ and $v^{\prime}=v[Y:=0]$.

Let $\vec{0}$ be the clock valuation where all clocks have value $0$. The set
of possible initial states of the PTG is
$\xi_{0}=\\{({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell_{0}}},(\vec{0},v_{P}))\;|\;v_{P}\in\mathbb{Q}_{\geq
0}^{P}:(\vec{0},v_{P})\models
Inv({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell_{0}}})\\}$.

######  Definition 10 (run)

A _run_ of the PTG $G$ is a finite or infinite sequence of states
$s_{0}s_{1}s_{2}\ldots$ s.t. $s_{0}\in\xi_{0}$ and $\forall
i\in\mathbb{N},\;s_{2i}\to^{\delta}s_{2i+1}\to^{t}s_{2i+2}$.
$\mathcal{R}(G)$denotes the set of runs, and $\mathcal{R}(G)(s)$ the set of
those starting from state $s$.

A run alternates between (potentially null) delays and discrete transitions,
avoiding runs that let only time pass. However, there might still be Zeno runs
where infinitely many discrete transitions are taken in a finite amount of
time. When there is no ambiguity, we omit $G$ in the notations.

###### Example 2

Let us consider again the coffee machine in Fig. 1. Assume the parameter
valuations are:
$v_{P}({\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{1}}})=5$,
$v_{P}({\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{2}}})=2$,
$v_{P}({\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{3}}})=5$
and
$v_{P}({\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{4}}})=6$.
Let
$v_{X}=(v_{X}({\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{x}}),v_{X}({\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{y}}))$.
We get the sequence:
$({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{preparing\\_coffee}},((0,0),v_{P}))\to^{4}({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{preparing\\_coffee}},((4,4),v_{P}))\to^{{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{ask\\_sugar}}}({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{adding\\_sugar}},((0,4),v_{P}))\to^{2}\\\
({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{adding\\_sugar}},((2,6),v_{P}))\to^{{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{sugar\\_added}}}({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{preparing\\_coffee}},((2,6),v_{P}))\enspace.$

######  Definition 11 (history)

A _history_ is a finite prefix of a run. The set of histories of game $G$ is
denoted $\mathcal{H}(G)$, and those starting in state $s$ by
$\mathcal{H}(G)(s)$.

The notion of coverage allows for capturing all states that can occur up to
some time, without a discrete transition.

######  Definition 12 (coverage)

Let $s,s^{\prime}\in\mathbb{S}$ and $\delta\geq 0$ such that
$s\to^{\delta}s^{\prime}$. The _coverage_ of the timed transition is the set
of intermediate states traversed:
$\mathit{Cover}(s\to^{\delta}s^{\prime})=\\{s^{\prime\prime}\in\mathbb{S}\;|\;\exists\delta^{\prime}:0\leq\delta^{\prime}\leq\delta\;\land\;s\to^{\delta^{\prime}}s^{\prime\prime}\\}\enspace.$

The coverage of state $s$ is the set of states obtained from $s$ with timed
transitions only:
$\mathit{Cover}(s)=\\{s^{\prime}\in\mathbb{S}\;|\;\exists\delta\geq
0\;s\to^{\delta}s^{\prime}\\}\enspace.$

The coverage of a run $r=s_{0}s_{1}s_{2}\ldots$ is the union of the coverage
of its timed transitions. When finite, it includes the coverage of its last
state $ls(r)$ :
$\mathit{Cover}(r)=\Big{(}\underset{i\in\mathbb{N}}{\bigcup}\;\mathit{Cover}(s_{2i}\to^{\delta}s_{2i+1})\Big{)}\cup\mathit{Cover}\big{(}ls(r)\big{)}\enspace.$

######  Definition 13 (reachability objective and winning runs)

Let ${R}\subseteq L$ be a _reachability objective_. The set of _winning runs_
$\Omega_{Reach}({R})$ is the subset of runs that visit ${R}$:
$\Omega_{Reach}({R})=\\{r\in\mathcal{R}\;|\;\exists\,{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}}\in{R},\exists
v\in
V:({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}},v)\in\mathit{Cover}(r)\\}\enspace.$

###### Example 3

In the coffee machine, the objective is to reach from the initial location
${\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{prepare\\_coffee}}$
the location
${\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{coffee\\_served}}$.
The reachability objective is thus
${R}=\\{{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{coffee\\_served}}\\}$,
and the set of winning runs is
$\Omega_{Reach}(\\{{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{coffee\\_served}}\\})\enspace.$

###  2.2 Strategies in Parametric Timed Games

We introduce a definition of a strategy that deviates from [10], where at each
moment, a player decides to either wait, or take a discrete transition. So
their strategy returns values in $T\cup\\{wait\\}$. The problem with their
strategy is that it is not always clear what should happen: for instance,
given a delay $\delta$, a history $h=s_{0}\to^{\delta}s_{1}$ and a strategy
$\sigma$, where $\sigma(h)=wait$ for $0<\delta\leq 1$ and $\sigma(h)=t$ for
$\delta>1$, it is not clear when transition $t$ happens: there is no minimal
$\delta>1$. Although this works formally, it is less clear what the allowed
behaviour of the winning player is precisely. For that reason, in our
definition of strategy, players must decide in advance which delay they will
take. This makes the definition more constructive, clarifying what move the
winning player will actually take (i.e. perform an action or decide to wait
for some particular time) and in the end simplifies the definition of what is
winning.

Furthermore, following [10], the definition of strategy is asymmetric for
controller and environment: If both wish to do a discrete transition, we
provide priority to the environment; this corresponds to the safest situation
from a software controller point of view. Another subtle asymmetry is that the
controller cannot assume that the environment will take some uncontrollable
transition, even when waiting any longer would violate the location invariant.
While this is in line with the formal definition of strategy in TG [10],
experiments with UPPAAL Tiga [8] reveal that in that tool, an uncontrollable
discrete transition is actually forced when reaching the boundary of violating
an invariant.

######  Definition 14 (strategy)

A _controller strategy_ $\sigma_{c}$ (resp. _environment strategy_
$\sigma_{e}$) models decision-making. It is a function, depending on a
history, deciding either to wait some amount of time (possibly infinite) or to
take a discrete transition: $\sigma_{c}:\mathcal{H}\to\mathbb{R}_{\geq
0}^{\infty}\cup T_{c}$, $\sigma_{e}:\mathcal{H}\to\mathbb{R}_{\geq
0}^{\infty}\cup T_{u}$ s.t. $\forall h\in\mathcal{H}$ and
$\sigma\in\\{\sigma_{c},\sigma_{e}\\}$,

  1. 1.

If
$\sigma(h)=({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}},g,{\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{a}},Y,{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell^{\prime}}})\in
T$
then
$ls(h)=({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}},v)$
such that $v\models g$ and $v[Y:=0]\models
Inv({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell^{\prime}}})$

  2. 2.

If $(\sigma(h)=\delta\in\mathbb{R}_{\geq 0})$ and the transition
$\to^{\delta}$ is available in ls(h)
then $\sigma(h\to^{\delta}s)\in T$

where $h\to^{\delta}s$ denotes the history obtained by adding the delay
$\delta$ at the end of $h$.

A strategy can return a discrete transition if its guard is satisfied and the
resulting state satisfies the destination invariant (1). To respect the
alternation between timed and discrete transitions, we require that a strategy
which returns a finite delay $\delta\geq 0$ on a history returns a discrete
transition after the delay (if the run did not stop by violating an
invariant)(2).

A controller strategy $\sigma_{c}$ and an environment strategy $\sigma_{e}$
can be combined into a global strategy $\sigma_{(\sigma_{c},\sigma_{e})}$ as
follows. If both players try to take a transition, we consider that the
controller cannot guarantee his transition will be taken, thus the environment
chooses. If one player decides on a discrete transition while the other
decides to wait, the discrete transition is taken. If both players decide to
wait, we wait for the smallest delay.

######  Definition 15 (global strategy)

Let $\sigma_{c}$ be a controller strategy and $\sigma_{e}$ an environment
strategy. For all $h\in\mathcal{H}$, the global strategy
$\sigma_{(\sigma_{c},\sigma_{e})}$ is defined by:

  * •

$\sigma_{e}(h)=t_{u}\in
T_{u}\implies\sigma_{(\sigma_{c},\sigma_{e})}(h)=t_{u}$

  * •

$\sigma_{c}(h)=t_{c}\in T_{c}\land\sigma_{e}(h)=\delta\geq
0\implies\sigma_{(\sigma_{c},\sigma_{e})}(h)=t_{c}$

  * •

$\sigma_{c}(h)=\delta\geq 0\land\sigma_{e}(h)=\delta^{\prime}\geq
0\implies\sigma_{(\sigma_{c},\sigma_{e})}(h)=min(\delta,\delta^{\prime})$

###### Example 4

Let us look at possible strategies in location
${\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{preparing\\_coffee}}$
of the running example. The machine can choose
${\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{serve\\_coffee}}$
while the user can select
${\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{ask\\_sugar}}$.
If both want to do an action, the strategy chooses
${\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{ask\\_sugar}}$,
thus giving priority to the user. If only one of them wants to take an action
and the other waits, the action is taken. Hence, the machine can do
${\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{serve\\_coffee}}$
if the user is waiting. This is the expected behavior of a coffee machine and
its user.

The global strategy induces a unique run, introducing null delays between two
discrete transitions to guarantee the alternation with timed transitions.

######  Definition 16 (run induced by a global strategy)

Let an initial state $s_{0}$ and a global strategy $\sigma$ be given. The _run
induced by strategy_ $\sigma$ is the unique $r_{\sigma}=s_{0}s_{1}s_{2}\ldots$
obtained by:

  * •

If $i$ is even, the next transition is a timed transition :

    * –

If $\sigma(\langle s_{0},\ldots,s_{i}\rangle)=t\in T$ a delay $0$ is added:
$s_{i}\to^{0}s_{i+1}\to^{t}s_{i+2}$

    * –

If $\sigma(\langle s_{0},\ldots,s_{i}\rangle)$ returns a delay $\delta\geq 0$
and there is a unique state $s$ such that $s_{i}\to^{\delta}s$ (invariant not
violated), then $s_{i+1}=s$.

    * –

Otherwise, the invariant is violated and the run ends.

  * •

If $i$ is odd, the next transition is a discrete transition. By the properties
of a strategy $\sigma(\langle s_{0},\ldots,s_{i}\rangle)$ returns a transition
$t$ such that there is a unique state $s$ where $s_{i}\to^{t}s$. Then,
$s_{i+1}=s$.

######  Definition 17 (winning strategy)

A controller strategy $\sigma_{c}$ is said to be _winning_ from a state
$s\in\mathbb{S}$ w.r.t. a reachability objective ${R}$ if and only if all runs
starting in $s$ and _adhering to_ $\sigma_{c}$ are winning w.r.t. the
objective. State $s$ is said to be winning if there exists a winning strategy
from it.

Run $r$ is _adhering to_ a controller strategy $\sigma_{c}$ if there exists an
environment strategy $\sigma_{e}$, such that
$r=r_{\sigma_{(\sigma_{c},\sigma_{e})}}$.

The question we now aim to answer is: Given a Parametric Timed Game $G$ and a
Reachability Objective ${R}$, is there a winning controller strategy from the
initial state? The question depends on the value of the parameters. So, more
precisely, we are interested in the question: _For which parameter valuations
is the corresponding initial state winning?_

##  3 Solving the Game

In this section, we introduce necessary elements for solving a game. We first
describe the symbolic state space on which the algorithm operates. Then we
characterize the set of winning states as a nested fixed point.

###  3.1 Parametric Zone Graph

Since clock valuations assign real numbers, the timed transition system of a
PTG has an uncountable number of states. Zones (cf. Def. 5) are a practical
tool to regroup these states in more manageable sets. Recall that zones (like
guards and invariants) are conjunctions of simple constraints on valuations,
and can be viewed as sets of valuations. Our algorithms operate on symbolic
states
$\xi=({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}},Z)$,
which consist of a location and a zone. We require that $Z\subseteq
Inv({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}})$.
For instance, the set of initial states of a PTG $\xi_{0}$ (cf. Def. 10) can
be described by the symbolic state
$({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell_{0}}},Inv({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell_{0}}})\wedge\bigwedge_{{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{x}}\in
X}{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}\mathrm{x}}=0)$.

In the notation, we identify a symbolic state
$({\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell}},Z)$
with its semantics as the set of concrete states: $\\{(l,v)\mid v\vDash
Z\\}\subseteq\mathbb{S}$. We will write $\xi.\ell$ to denote the (common)
location of a symbolic state $\xi$. Zones are closed under the following
operations, which we extend to symbolic states:

  * •

Intersection between sets

  * •

Temporal successors: $\xi^{\nearrow}=\\{s^{\prime}\in\mathbb{S}\mid\exists
s\in\xi,s\to^{\delta}s^{\prime}\\}$

  * •

Temporal predecessors: $\xi^{\swarrow}=\\{s^{\prime}\in\mathbb{S}\mid\exists
s\in\xi,s^{\prime}\to^{\delta}s\\}$

  * •

Discrete successors: $Succ(t,\xi)=\\{s^{\prime}\in\mathbb{S}\mid\exists
s\in\xi,s\to^{t}s^{\prime}\\}$

  * •

Discrete predecessors: $Pred(t,\xi)=\\{s^{\prime}\in\mathbb{S}\mid\exists
s\in\xi,s^{\prime}\to^{t}s\\}$

  * •

Projection onto parameters: $\xi{\downarrow_{P}}=\\{v_{P}\mid\exists
v_{X},\ell,\,(\ell,(v_{X},v_{P}))\in\xi\\}$

These operations can be implemented by standard operations on convex polyhedra
[7]. We also use union, set complement and set difference, which can return
non-convex shapes. These are represented as unions of zones, still denoting
sets of concrete states. All previous operations are extended to unions of
zones.

Our algorithms operate on the Parametric Zone Graph (PZG). The PZG of a PTG is
not guaranteed to be finite, so our algorithms are in fact semi-algorithms.

######  Definition 18 (Parametric Zone Graph)

Given a PTA of the form
$G=(L,X,P,Act,T_{c},T_{u},{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell_{0}}},Inv)$,
its _Parametric Zone Graph_ is defined as the tuple
$(\Xi,\xi_{0}^{\nearrow},\Rightarrow^{t}_{c},\Rightarrow^{t}_{u})$, where
$\Xi\subseteq 2^{\mathbb{S}}$; $\forall\xi,\xi^{\prime}\in\Xi$ we have
$\xi\Rightarrow^{t}_{c}\xi^{\prime}$ if $\xi^{\prime}=Succ(t,\xi)^{\nearrow}$
and $t\in T_{c}$; and $\xi\Rightarrow^{t}_{u}\xi^{\prime}$ if
$\xi^{\prime}=Succ(t,\xi)^{\nearrow}$ and $t\in T_{u}$.

###  3.2 Alternating Fixed Point Property

The algorithm works by alternating between exploring new states and back-
propagating winning-state information from discovered winning states, starting
from target states. The exploration relies on a fixed point property of the
set $Reach(\xi_{0})$, defined as all symbolic states in some run from an
initial state in $\xi_{0}$:

######  Lemma 1 (from [14])

$Reach(\xi_{0})$ is the smallest set $S$ containing $\xi_{0}^{\nearrow}$ such
that $\forall t\in T,\;Succ(t,S)^{\nearrow}\subseteq S$.

Similarly, the set of winning states $W({R})$ of the PTG with reachability
objective ${R}$ can be computed as a fixed point. Intuitively, we can win the
game if we can take a temporal transition (without being diverted by an
uncontrollable action leading us to a non-winning state) to a state that is
either directly winning, or has a controllable transition to a winning state.
We formalize this with three operators on sets of states. Let $W$ be the set
of winning states of the game.

We call $\mathit{WinningMoves}(S)=\\{s\in\mathbb{S}\mid\exists t\in
T_{c},s^{\prime}\in S,\;s\to^{t}s^{\prime}\\}$ the set of states that have
access to a controllable action leading to $S$. When applied to $W$, it gives
us the states with a controllable action to reach $W$, from which we have a
winning strategy. $\mathit{WinningMoves}(S)$ is increasing in $S$. It can be
computed using the previous operators as
$\mathit{WinningMoves}(S)=\bigcup_{t_{c}\in T_{c}}Pred(t_{c},S)\enspace.$

We call $\mathit{Uncontrollable}(S)=\\{s\in\mathbb{S}\mid\exists t\in
T_{u},s^{\prime}\notin S,\;s\to^{t}s^{\prime}\\}$ the set of states where an
uncontrollable action leads to a state outside $S$. When applied to $W$, it
gives us the states where the environment can derail us into a state outside
$W$, from which we have no winning strategy. $\mathit{Uncontrollable}(S)$ is
decreasing in $S$. It can be computed from the operators from the previous
subsection by $\mathit{Uncontrollable}(S)=\bigcup_{t_{u}\in
T_{u}}Pred(t_{u},\mathbb{S}\backslash S)\enspace.$

Finally, we call $\mathit{SafePred}(S_{1},S_{2})$ the set of states that can
reach $S_{1}$ by a temporal transition while avoiding $S_{2}$. Since it aims
to be applied to reach winning moves while avoiding uncontrollable actions, if
a state is in the intersection of $S_{1}$ and $S_{2}$, priority is given to
the environment and the state is not considered safe.
$\mathit{SafePred}(S_{1},S_{2})=\\{s\in\mathbb{S}\mid\exists s^{\prime}\in
S_{1},s\to^{\delta}s^{\prime}\land\mathit{Cover}(s\to^{\delta}s^{\prime})\cap
S_{2}=\emptyset\\}$. $\mathit{SafePred}(S_{1},S_{2})$ is increasing in $S_{1}$
and decreasing in $S_{2}$.

Thanks to the work of Cassez et al. [10], $\mathit{SafePred}$ can be computed
between zones using the precedent operations and extended to union of zones:

######  Lemma 2 (from [10] for TG, [16] for PTG)

$\mathit{SafePred}(S_{1},S_{2})=(S_{1}^{\swarrow}\backslash
S_{2}^{\swarrow})\cup((S_{1}\cap(S_{2}^{\swarrow}))\backslash
S_{2})^{\swarrow}$
$\mathit{SafePred}(\underset{i}{\bigcup}S_{1i},\underset{j}{\bigcup}S_{2j})=\underset{i}{\bigcup}\big{(}S_{1i}^{\swarrow}\cap\underset{j}{\bigcap}\mathit{SafePred}(S_{1i}\big{)},S_{2j})$

We can now formulate the fixed point property followed by $W$.

######  Lemma 3 ()

$W({R})$ is the smallest set $S$ containing ${R}$ such that
$\mathit{SafePred}(S\cup\mathit{WinningMoves}(S),\mathit{Uncontrollable}(S))\subseteq
S\enspace.$

###### Proof

See Appendix 0.A.

##  4 Algorithm and Correctness

Algorithm 1 For PTG
$G=(L,X,P,Act,T_{c},T_{u},{\color[rgb]{0.4,0.4,0.65}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,0.65}\mathrm{\ell_{0}}},Inv)$
and reachability objective ${R}$, returns the set of all parameter valuations
that win the game.

1:$\mathit{Explored},\mathit{WaitingUpdate},\mathit{WaitingExplore}\leftarrow\emptyset,\emptyset,\\{\xi_{0}^{\nearrow}\\}$
$\triangleright$ Symbolic state sets

2:$\mathit{Win}:=\\{\\}$ $\triangleright$ Map from symbolic states to unions
of zones

3:$\mathit{Depends}:=\\{\\}$ $\triangleright$ Map from symbolic states to sets
of symbolic states

4:$\mathit{WinningParam}:=False$

5:

6:function solvePTG

7: while $\lnot$terminate( ) do

8: Choose either explore( ) or update( )

9: return $\mathit{WinningParam}$

10:

11:procedure explore

12: $\xi\leftarrow extract(\mathit{WaitingExplore})$

13: for $t$ transition from $\xi$ : do

14: $\xi^{\prime}:=Succ(t,\xi)^{\nearrow}$

15:
$\mathit{Depends}[\xi^{\prime}]\leftarrow\mathit{Depends}[\xi^{\prime}]\cup\\{\xi\\}$

16: if $\xi^{\prime}$ not in $\mathit{Explored}$ then

17:
$\mathit{WaitingExplore}\leftarrow\mathit{WaitingExplore}\cup\\{\xi^{\prime}\\}$

18: if $\xi.\ell\in{R}$ then

19: $\mathit{Win}[\xi]\leftarrow\xi$

20:
$\mathit{WaitingUpdate}\leftarrow\mathit{WaitingUpdate}\cup\mathit{Depends}[\xi]$

21: $\mathit{WaitingUpdate}\leftarrow\mathit{WaitingUpdate}\cup\\{\xi\\}$

22: $\mathit{Explored}\leftarrow\mathit{Explored}\cup\\{\xi\\}$

23:

24:procedure update

25: $\xi\leftarrow extract(\mathit{WaitingUpdate})$

26:
$Uncontrollable\leftarrow\underset{\\{(\xi^{\prime},t)\mid\xi\Rightarrow^{t}_{u}\xi^{\prime}\\}}{\bigcup}Pred(t,\xi^{\prime}\setminus\mathit{Win}[\xi^{\prime}])$

27:
$\mathit{WinningMoves}\leftarrow\underset{\\{(\xi^{\prime},t)\mid\xi\Rightarrow^{t}_{c}\xi^{\prime}\\}}{\bigcup}Pred(t,\mathit{Win}[\xi^{\prime}])$

28:
$\mathit{NewWin}:=\mathit{SafePred}(Win[\xi]\cup\mathit{WinningMoves},\>Uncontrollable)\>\cap\>\xi$

29: if $\mathit{NewWin}\not\subseteq\mathit{Win}[\xi]$ then

30:
$\mathit{WaitingUpdate}\leftarrow\mathit{WaitingUpdate}\cup\mathit{Depends}[\xi]$

31: $\mathit{Win}[\xi]\leftarrow\mathit{Win}[\xi]\cup\mathit{NewWin}$

32:
$\mathit{WinningParam}\leftarrow(\mathit{Win}[\xi]\cap\xi_{0}){\downarrow_{P}}$

33:

34:function terminate

35: return
$\mathit{WaitingExplore}=\emptyset\land\mathit{WaitingUpdate}=\emptyset$

We can now introduce the algorithm for parameter synthesis for PTG. Alg. 1
explores the state space and creates a map of symbolic states connected by a
discrete transition through the operation $Succ(t_{s},\\_)^{\nearrow}$.
Simultaneously, any newly found winning states in a symbolic state $\xi$,
starting from the target locations, are propagated by marking the predecessors
of $\xi$ for an update. To update a symbolic state $\xi$, we compute
$\mathit{SafePred}({\mathit{Win}\cup\mathit{WinningMoves}(\mathit{Win})},$
$\mathit{Uncontrollable}(\mathit{Win}))$ within $\xi$ and add the result to
$\mathit{Win}[\xi]$. If new winning states are found, we mark $\xi$
predecessors for an update.

The algorithm is non-deterministic: it does not describe how we choose between
explore and update, and which symbolic state in the waiting lists to explore
or update. These choices are left abstract on purpose, as optimization
opportunities. A fair strategy would be to join $\mathit{WaitingExplore}$ and
$\mathit{WaitingUpdate}$ in a single queue, whose head determines which
operation to apply next. In our implementation, we prioritized back-
propagation from $\mathit{WaitingUpdate}$.

###  4.1 Invariants and Correctness

Recall that the algorithm works on a zone graph. We are looking for subsets of
winning states within symbolic states. The same state may appear in different
symbolic states and may not have the same status in each instance. Therefore,
the set $W_{temp}$, the winning states found by the algorithm so far, and $W$,
the set of all winning states, also take into account the symbolic state
considered. Formally, $W$ consists of all pairs $(\xi,s)$ where $s$ is a
winning state contained in the symbolic state $\xi$, and
$W_{temp}=\underset{\xi\in\mathit{Explored}}{\bigcup}\\{\xi\\}\times
Win[\xi]$.

######  Theorem 4.1 ()

These invariants hold during the execution of the algorithm:

  1. 1.

$\xi_{0}^{\nearrow}\in\mathit{Explored}$.

  2. 2.

$\forall\xi\in\mathit{Explored},t\in T,\xi^{\prime}$, if
$\xi\Rightarrow^{t}\xi^{\prime}$, then
$\xi^{\prime}\in{\mathit{WaitingExplore}\cup\mathit{Explored}}$

  3. 3.

$\forall\xi\in\mathit{Explored}$, if $\xi.l\in{R}$,
$\\{\xi\\}\times\xi\subseteq W_{temp}$.

  4. 4.

$W_{temp}\subseteq W$.

  5. 5.

$\forall\xi\in\mathit{Explored}$, we have either
$\xi\in\mathit{WaitingUpdate}$ or
$\mathit{SafePred}(W_{temp}\cup\mathit{WinningMoves}(W_{temp}),\>\mathit{Uncontrollable}(W_{temp}))\cap(\\{\xi\\}\times\xi)\subseteq
W_{temp}$.

###### Proof

See Appendix 0.B.

Invariant 4 guarantees that even if the algorithm times out the winning states
found by the algorithm are indeed winning. Furthermore, if the algorithm
terminates and the waiting lists are empty, we can apply the fixed point
properties of $Reach(\xi_{0})$ and $W$, and $W_{temp}$ corresponds exactly to
$W$ over the explored symbolic states that cover $Reach(\xi_{0})$.

######  Theorem 4.2 ()

Alg. 1 is correct (when it terminates).

###### Proof

See Appendix 0.B.

###### Example 5

For the coffee machine, the PZG is only finite after applying inclusion
subsumption (Sec. 5). However, even on this finite PZG, Alg. 1 does not
terminate, but keeps reporting solutions at 32. In fact, it produces
increasingly more general solutions, including
$n\,{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{2}}}\geq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{1}}}$
(for any $n>0$). If we bound these parameters in the initial specification,
for intance
${\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{2}}}\geq
1\wedge{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{1}}}\leq
5$, our algorithm synthesizes the extra constraints
${\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{1}}}+{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{2}}}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{4}}}\wedge{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{3}}}<{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}\mathrm{p_{4}}}$,
as expected.

###### Theorem 4.3

Provided the waiting lists are treated fairly, any explored winning state is
discovered as winning by the algorithm eventually.

######  Proof (sketch)

For a classical TG, we can represent the underlying TA as a finite classical
automaton (e.g. the region graph). On this automaton, we can define a (finite)
turn-based reachability game equivalent to the initial TG. Hence, we can use
the notion of _discrete distance to target_ in a reachability game,
corresponding to the smallest number of discrete transitions in which a
controller can ensure to reach a target. This is equivalent to solving a _Min-
Cost Reachability game_ as studied in [9] where delay transitions have weight
$0$ and discrete transitions have weight $1$. The game graph is finite and the
weights non-negative, so the discrete distance to target of a winning state is
positive and finite.

While the same construction is not necessarily finite in a PTG, any state of a
PTG is a state $(\ell,(v_{P},v_{X}))$ of the TG, where all parametric linear
terms in guards have been replaced by their valuation through $v_{P}$.
Therefore, this result extends to winning states of a PTG.

Let $s$ be an explored winning state of the PTG and $n$ its distance to
target. We only need to explore states reachable in $n$ discrete transitions
from $s$. By invariant 2 from Thm. 4.1, when all states reachable in $k$
discrete transitions are explored, all states reachable in $k+1$ discrete
transitions are either already explored or in the exploration waiting list.
Assuming fairness of the waiting lists, at some time they have all been
explored. Therefore, at some time, all states reachable from $s$ in $n$
discrete steps have been explored.

When all states reachable in $n$ discrete steps have been explored, all target
states within are discovered. Those are states with distance to target $0$.
For $0\leq k<n$, when all winning states reachable in less than $n-k$ discrete
transitions from $s$ and with a distance to target less than $k$ are
discovered, then all winning states reachable in less than $n-(k+1)$ discrete
transitions from $s$ and with a distance to target less than $k+1$ are
discoverable by update. Using the invariant (5) of Thm. 4.1, those states are
either already discovered as winning or they are in the update waiting list.
Assuming fairness of the waiting lists, at some time they have all been
discovered winning. Applying this recurrence until $k=n$, we get that there is
a time where $s$ is discovered winning.

We can guarantee: (1) All winning parameter valuations reported in 32 are
correct, since the algorithm satisfies the invariants of Thm. 4.1. (2) Every
winning parameter valuation will eventually be reported, provided the waiting
lists are treated fairly. Hence, Alg. 1 is “sound and complete in the limit”
[5].

##  5 Optimizations

Algorithm 2 Adding optimizations to the explore procedure

1:procedure explore

2: $\xi\leftarrow extract(\mathit{WaitingExplore})$

3: if $\xi{\downarrow_{P}}\subseteq\mathit{WinningParam}$ then
$\triangleright$ Cumulative Pruning

4: return

5: if $\xi.\ell\in{R}$ then

6: $\mathit{Win}[\xi]\leftarrow\xi$

7:
$\mathit{WaitingUpdate}\leftarrow\mathit{WaitingUpdate}\cup\mathit{Depends}[\xi]$

8: if $\mathit{controller\\_deadlock}(\xi)\;\land\;\mathit{Win}[\xi]\neq\xi$
then $\triangleright$ Losing state propagation

9:
$\mathit{WaitingUpdate}_{L}\leftarrow\mathit{WaitingUpdate}_{L}\cup\mathit{Depends}[\xi]$

10: if $\mathit{Win}[\xi]=\xi\;\lor\;\mathit{controller\\_deadlock}(\xi)$ then
$\triangleright$ Coverage Pruning

11: return

12: for $t$ transition from $\xi$ : do

13: $\xi^{\prime}:=Succ(t,\xi)^{\nearrow}$

14: if
$\exists\xi^{\prime\prime}\in\mathit{Explored}:\xi^{\prime}\subseteq\xi^{\prime\prime}$
then $\triangleright$ Inclusion check

15:
$\mathit{Depends}[\xi^{\prime\prime}]\leftarrow\mathit{Depends}[\xi^{\prime\prime}]\cup\\{\xi\\}$

16: else

17:
$\mathit{Depends}[\xi^{\prime}]\leftarrow\mathit{Depends}[\xi^{\prime}]\cup\\{\xi\\}$

18:
$\mathit{WaitingExplore}\leftarrow\mathit{WaitingExplore}\cup\\{\xi^{\prime}\\}$

19:
$\mathit{WaitingUpdate}_{W}\leftarrow\mathit{WaitingUpdate}_{W}\cup\\{\xi\\}$

20:
$\mathit{WaitingUpdate}_{L}\leftarrow\mathit{WaitingUpdate}_{L}\cup\\{\xi\\}$
$\triangleright$ Losing state propagation

21: $\mathit{Explored}\leftarrow\mathit{Explored}\cup\\{\xi\\}$

We present four optimizations to the algorithm presented in Section 4. All of
them adapt optimizations from previous works, three of them (coverage pruning,
inclusion checking and losing state propagation) from Cassez et al. [10] and
one of them (cumulative pruning) from André et al. [5]. We start by updating
the exploration procedure to include the optimizations, as shown in Alg. 2.

###  5.1 Pruning

First, we present some pruning techniques, as these only require slight
modifications in the exploration procedure. To this end, we introduce the
notion of a controller deadlock state. A state is a controller deadlock state
if it has no controllable transitions. We define it as the following predicate
on symbolic states:

$\mathit{controller\\_deadlock}(\xi)=\forall t,\xi^{\prime}:\mbox{ if
}\xi\Rightarrow^{t}\xi^{\prime}\mbox{ then }t\in T_{u}$

Now, we introduce the two kinds of pruning:

  * •

Cumulative Pruning: If the projected parameters of a zone in a new symbolic
state are included in the current set of winning parameters, we can safely
prune the successors of this state. Indeed, if the only possible parameters in
the zone already are determined to be winning, no new winning parameter can be
found by exploring the successors of this state. This check can be seen in 3
and 4 of Alg. 2.

  * •

Coverage Pruning: If a symbolic state is either winning or a controllable
deadlock state, its successors can safely be pruned. Indeed, if the symbolic
state is winning, we gain nothing from exploring further. Dually, a controller
deadlock state can never become winning, since the controller has no action to
do. This check can be seen in 10 and 11 of Alg. 2.

###  5.2 Inclusion checking

Originally, checking if a symbolic state $\xi^{\prime}$ has been explored
already is done by checking if $\xi^{\prime}\in\mathit{Explored}$. The
optimization by inclusion checking instead checks if
$\exists\xi^{\prime\prime}\in\mathit{Explored}:\xi^{\prime}\subseteq\xi^{\prime\prime}$.
If this is the case, the newly discovered symbolic state can safely be
discarded since its superset has already been explored. Of course, the new
dependency that $\xi$ depends on $\xi^{\prime\prime}$ still must be added.
This optimization is done in the exploration procedure (14 to 18 of Alg. 2).

###  5.3 Losing state propagation

Losing state propagation is inspired by Cassez et al. [10] for TG. The idea is
that instead of only discovering and propagating winning states, we will now
also do the same for losing states, starting from controller deadlock states.
A map $Lose$ will maintain the currently known losing states for a given
symbolic state. Thus, each symbolic state $\xi$ can now be partitioned into
three:

  * •

Winning: $Win[\xi]$,

  * •

Losing: $Lose[\xi]$

  * •

Unknown: $\xi\setminus(Win[\xi]\cup Lose[\xi])$.

To initially mark a state as losing, we use the controller deadlock predicate
again while also making sure that the state is not winning, as shown in Alg.
2, 8 and 9. On 19 and 20, we partition the $\mathit{WaitingUpdate}$ list into
two lists for propagating winning and losing states respectively.

While pruning and inclusion checking only required the modification of the
exploration procedure, the propagation of losing states influences all of the
procedures of the original algorithm. We go through them now.

#### Update procedure.

We create a new procedure for updating losing states, which can be seen in
Alg. 3. As the dual of the original update procedure, it is almost identical.
Instead of $\mathit{Uncontrollable}$, we compute $\mathit{Controllable}$, i.e.
the union of zones where the controller can lead to a non-losing state.
Similarly, instead of $\mathit{WinningMoves}$, we compute
$\mathit{LosingMoves}$ which is the set of states where the environment can
lead to a losing state. We then compute $\mathit{NewLosing}$ which is the set
of states where the environment can lead us to a losing state while avoiding
states where _only_ controllable transitions are enabled
($\mathit{Controllable}\setminus\mathit{LosingMoves}$). Finally, we update
$Lose[\xi]$ and $\mathit{WaitingUpdate}_{L}$ accordingly.

Algorithm 3 Adding new update procedure for losing state propagation

procedure update_l

$\xi\leftarrow extract(\mathit{WaitingUpdate}_{L})$

$\mathit{Controllable}\leftarrow\underset{\\{(\xi^{\prime},t)\mid\xi\Rightarrow^{t}_{c}\xi^{\prime}\\}}{\bigcup}Pred(t,\xi^{\prime}\setminus
Lose[\xi^{\prime}])$

$\mathit{LosingMoves}\leftarrow\underset{\\{(\xi^{\prime},t)\mid\xi\Rightarrow^{t}_{u}\xi^{\prime}\\}}{\bigcup}Pred(t,Lose[\xi^{\prime}])$

$\mathit{NewLosing}:=\mathit{SafePred}(Lose[\xi]\cup\mathit{LosingMoves},\>\mathit{Controllable}\setminus\mathit{LosingMoves})\>\cap\>\xi$

if $Lose[\xi]\subsetneq\mathit{NewLosing}$ then

$\mathit{WaitingUpdate}_{L}\leftarrow\mathit{WaitingUpdate}_{L}\cup\mathit{Depends}[\xi]$;
$Lose[\xi]\leftarrow\mathit{NewLosing}$

#### Terminate function.

The terminate function is modified to allow for early termination if all
possible information is already known, i.e.
$\xi_{0}^{\nearrow}\setminus(Win[\xi_{0}^{\nearrow}]\cup
Lose[\xi_{0}^{\nearrow}])=\emptyset$. Indeed, if for all valuations we have
determined that we either win or lose, the algorithm can safely terminate.
This is shown in Alg. 4.

Algorithm 4 New Terminate with early termination if initial zone is covered

function terminate

$isEmpty\leftarrow\mathit{WaitingExplore}=\emptyset\land\mathit{WaitingUpdate}=\emptyset$

$initialZoneCovered\leftarrow(\xi_{0}^{\nearrow})\subseteq(Win[\xi_{0}^{\nearrow}]\cup
Lose[\xi_{0}^{\nearrow}])$

return $isEmpty\;\lor\;initialZoneCovered$

The final algorithm is then modified to include the new procedures and data
structures introduced. As a result, in the main loop we now have to choose
between three waiting lists instead of two: $\mathit{WaitingExplore}$,
$\mathit{WaitingUpdate}_{W}$ and $\mathit{WaitingUpdate}_{L}$.

##  6 Implementation and Experimental Evaluation

To evaluate the termination behavior and efficiency of the semi-algorithm and
the optimizations, we implement them in the Imitator toolset and measure the
performance on some realistic case studies.

###  6.1 Implementation

We have implemented our proposed algorithm and optimizations in the Imitator
model checker [4], which features a wide repertoire of synthesis algorithms
for PTA. We have extended its input language to PTG and added our PTG
parameter synthesis algorithm, including the optimizations described in Sec.
5. The source code (in OCaml) is available on
github111https://github.com/imitator-model-checker/imitator, branch: develop.

In Imitator, the user specifies a model consisting of parameters, clocks and a
network of parametric timed automata. The user can analyse the model using an
analysis or synthesis query. Imitator selects the corresponding algorithm to
use, after which it outputs the result of the query.

Our extension enables the user to specify edges in a PTA as (un)controllable,
effectively turning it into a PTG. Along with this we add a new property Win
and a corresponding algorithm AlgoPTG. In order to synthesize parameters for a
PTG one must use property := #synth Win(state_predicate), using a predicate to
define which states are winning. Usually, this predicate is simply accepting,
meaning that any state in an accepting location of the PTG is winning.

In Alg. 1 we left the choice between exploration and back-propagation to be
non-deterministic. In the implementation we choose to prioritize back-
propagation over exploration whenever possible (i.e. when
$\mathit{WaitingUpdate}$ is non-empty), otherwise we explore. This seems to
yield the fastest results in practice.

###  6.2 Experiment Design

We selected two large case studies, one PTA and one TG, and extended them to
PTGs by adding (un)controllable actions, and clock parameters, respectively.
An artifact containing instructions to run all the experiments is available
online [11].

#### Production Cell.

This case study [18] has two conveyor belts (1 / 2), a robot with two arms (A
/ B) and a press. Plates arrive at conveyor belt 1 and are taken to the press
by robot arm A, where they are processed for some time. Robot arm B takes
processed plates and removes them through conveyor belt 2.

We model systems with 1–4 plates in Imitator. In the goal location, every
plate made it safely to conveyor belt 2. If two plates collide before they are
picked up by arm A, the game is lost immediately. We assume that the rotation
speed of the robot arm, the speed of the conveyor belt and the time to press
are known constants. The aim is to synthesize a parameter MINWAIT, the minimum
time interval between two plates arriving at the conveyor belt. The maximum
time interval between two plates is fixed by an additional constant MAXWAIT.

Our PTG model is largely inspired by the TG model of Cassez et al. [10].
Besides adding parameters, we check for collisions between plates rather than
defining a maximum waiting time frame. For 2–4 plates, we create a winning and
a losing configuration of the constants; for 1 plate a collision is not
possible. The losing configurations are created by setting MAXWAIT too small,
which will deadlock the system for any value of MINWAIT.

The Imitator model for the 1-plate configuration can be seen in Appendix 0.C.

#### Bounded Retransmission Protocol.

The BRP provides reliable communication over an unreliable channel. We create
a PTG from a PTA model of the BRP [6], in turn based on a TA model [12], by
making message loss uncontrollable.

In the BRP, a sender sends message frames to a receiver, tagged with an
alternating bit, through a lossy channel. The receiver acknowledges all
frames. If the sender does not receive an acknowledgement in time, it
retransmits the message at most $k$ times, after which the sender gives up.
The goal location indicates the successful transmission of the message, or the
abort by the sender.

#### Experimental Setup.

All experiments were run on a single core of a computer with an Intel Core
i5-10400F CPU @ 2.90GHz with 16GB of RAM running Ubuntu 20.04.6 LTS. For each
implementation (basic, inclusion checking, cumulative pruning, coverage
pruning, losing state propagation) we run the experiments 5 times and report
the average time and state space size. A timeout of 2 hours is used.

###  6.3 Experimental Results

Table 1: Experimental results for different optimizations: inclusion check (inc), cumulative pruning (cm), coverage pruning (cv), losing state propagation (lp). Running time in seconds (s) and number of symbolic states (size). Green indicates the best results. | inc | inc+cm | inc+cm+cv | inc+cm+cv+lp
---|---|---|---|---
Time | Size | Time | Size | Time | Size | Time | Size
plates | Production Cell
1 | Win | 0.06s | 86 | 0.06s | 86 | 0.06s | 86 | 0.08s | 86
2 | Win | 7.19s | 746 | 7.56s | 746 | 6.60s | 701 | 7.22s | 701
Lose | 1.43s | 439 | 1.44s | 439 | 2.03s | 517 | 2.17s | 517
3 | Win | 36.7s | 1900 | 37.3s | 1900 | 24.0s | 1539 | 34.2s | 1539
Lose | 13.4s | 1372 | 13.9s | 1372 | 9.53s | 1251 | 14.2s | 1251
4 | Win | 4903s | 10755 | 4750s | 10755 | 2394s | 9350 | 3522s | 9350
Lose | 34.8s | 2605 | 35.6s | 2605 | 21.6s | 2372 | 153s | 2372
Bounded Retransmission Protocol
| 34.3s | 1042 | 32.2s | 1042 | 7.1s | 612 | 7.5s | 612

We present the results of the experiments in table 1. We do not include the
runs without optimizations as they all timed out. This indicates that
inclusion checking is the most vital optimization and should always be
enabled.

Indicated in green cells are the best results for each row. We can clearly see
that coverage pruning has the biggest effect of all the optimizations in our
experiments. Losing state propagation seems to not provide much benefit in
these experiments, as the overhead overshadows any positive effect it might
have had.

##  7 Conclusion

We provide the first implementation of parameter synthesis for Parametric
Timed Games with reachability objectives, based on an on-the-fly algorithm
[10, 15]. It appears that without additional pruning heuristics, the algorithm
cannot handle the case studies, Bounded Retransmission Protocol and Production
Cell. Inclusion subsumption is a minimal requirement to achieve any result.

Contrary to previous algorithms for PTA [5] and TG [10], the parameter
synthesis algorithm does not terminate, even if the parametric zone graph is
finite. But we found that in the limit all parameter values will be
enumerated.

We added additional pruning techniques (coverage pruning and cumulative
pruning) to further reduce the search space. These techniques generally
increased the speed. We also experimented with propagating losing states, but
in our examples the overhead of checking and propagating losing states was not
compensated by any pruning potential. Future work could study under which
circumstances the propagation of losing states could be beneficial, but also
strengthen the detection of (partially) losing states. Another venue for
future work is to study other objectives, like safety games or liveness
conditions.

#### Acknowledgment.

We thank Étienne André for his help with integrating our algorithm in the
Imitator tool set.

## References

  * [1] Rajeev Alur and David L. Dill.  A theory of timed automata.  Theoretical Computer Science, 126(2):183–235, 1994.
  * [2] Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi.  Parametric real-time reasoning.  In STOC, pages 592–601. ACM, 1993.
  * [3] Étienne André.  What’s decidable about parametric timed automata?  Int. J. Softw. Tools Technol. Transf., 21(2):203–219, 2019.
  * [4] Étienne André.  IMITATOR 3: Synthesis of timing parameters beyond decidability.  In CAV (1), volume 12759 of Lecture Notes in Computer Science, pages 552–565. Springer, 2021.
  * [5] Étienne André, Jaime Arias, Laure Petrucci, and Jaco van de Pol.  Iterative bounded synthesis for efficient cycle detection in parametric timed automata.  In TACAS, LNCS 12651, pages 311–329. Springer, 2021.
  * [6] Étienne André, Dylan Marinho, and Jaco van de Pol.  A benchmarks library for extended parametric timed automata.  In TAP@STAF, volume 12740 of Lecture Notes in Computer Science, pages 39–50. Springer, 2021.
  * [7] Roberto Bagnara, Patricia M. Hill, and Enea Zaffanella.  The parma polyhedra library: Toward a complete set of numerical abstractions for the analysis and verification of hardware and software systems.  Sci. Comp. Prog., 72(1-2):3–21, 2008.
  * [8] Gerd Behrmann, Agnès Cougnard, Alexandre David, Emmanuel Fleury, Kim Guldstrand Larsen, and Didier Lime.  Uppaal-tiga: Time for playing games!  In CAV, volume 4590 of Lecture Notes in Computer Science, pages 121–125. Springer, 2007.
  * [9] Thomas Brihaye, Gilles Geeraerts, Axel Haddad, and Benjamin Monmege.  To reach or not to reach? Efficient algorithms for total-payoff games.  In CONCUR, volume 42 of LIPIcs, pages 297–310. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015.
  * [10] Franck Cassez, Alexandre David, Emmanuel Fleury, Kim G. Larsen, and Didier Lime.  Efficient on-the-fly algorithms for the analysis of timed games.  In Martín Abadi and Luca de Alfaro, editors, CONCUR 2005 – Concurrency Theory, pages 66–80, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg.
  * [11] Mikael B. Dahlsen-Jensen, Jaco van de Pol, Laure Petrucci, and Baptiste Fievet.  Artifact for ”On-The-Fly Algorithm for Reachability in Parametric Timed Games”.  Zenodo, 10.5281/zenodo.10046945, October 2023.
  * [12] P. R. D’Argenio, J. P. Katoen, T. C. Ruys, and J. Tretmans.  The bounded retransmission protocol must be on time!  In Ed Brinksma, editor, Tools and Algorithms for the Construction and Analysis of Systems, pages 416–431, Berlin, Heidelberg, 1997\. Springer Berlin Heidelberg.
  * [13] Thomas Hune, Judi Romijn, Mariëlle Stoelinga, and Frits W. Vaandrager.  Linear parametric model checking of timed automata.  J. Log. Algebraic Methods Program., 52-53:183–220, 2002.
  * [14] Aleksandra Jovanovic, Sébastien Faucou, Didier Lime, and Olivier H. Roux.  Real-time control with parametric timed reachability games.  In IFAC WODES, pages 323–330. Elseviers, 2012.
  * [15] Aleksandra Jovanovic, Didier Lime, and Olivier H. Roux.  Synthesis of bounded integer parameters for parametric timed reachability games.  In ATVA, volume 8172 of Lecture Notes in Computer Science, pages 87–101. Springer, 2013.
  * [16] Aleksandra Jovanović, Didier Lime, and Olivier Henri Roux.  A game approach to the parametric control of real-time systems.  International Journal of Control, pages 1–12, January 2018.
  * [17] Oded Maler, Amir Pnueli, and Joseph Sifakis.  On the synthesis of discrete controllers for timed systems.  In Ernst W. Mayr and Claude Puech, editors, STACS 95, pages 229–242, Berlin, Heidelberg, 1995. Springer Berlin Heidelberg.
  * [18] Helmut Melcher and Klaus Winkelmann.  Controller synthesis for the “production cell” case study.  In Proceedings of the Second Workshop on Formal Methods in Software Practice, FMSP ’98, page 24–33, New York, NY, USA, 1998. ACM.

##  Appendix 0.A Proof of the Fixed Point Property of $W$

#### Notations.

In this part, for two histories $h=s_{0}s_{1}\ldots s_{i}$ and
$h^{\prime}=s_{i}s_{i+1}\ldots s_{j}$, we note $h\cdot h^{\prime}$ the history
$s_{0}s_{1}\ldots s_{i-1}s_{i+1}\ldots s_{j}$ if there exist
$\delta_{1},\delta_{2}\geq 0$ such that
$s_{i-1}\to^{\delta_{1}}s_{i}\to^{\delta_{2}}s_{i+1}$, and $s_{0}s_{1}\ldots
s_{i}s_{i+1}\ldots s_{j}$ if not. We call $h$ a prefix of $h\cdot h^{\prime}$
and $h^{\prime}$ a suffix. Similar notations apply by replacing $h^{\prime}$
with a run. We also define the cover of a history $h=\langle
s_{0},s_{1},\ldots s_{n}\rangle$ to be:
$\mathit{Cover}(h)=\underset{i\in\mathbb{N}}{\bigcup}\;\mathit{Cover}(s_{2i}\to^{\delta}s_{2i+1})$.

The proof of Lem. 3 uses the following Lemmas 4 and 5.

###### Lemma 4

$\mathit{SafePred}(W({R})\cup\mathit{WinningMoves}(W({R})),\mathit{Uncontrollable}(W({R})))\subseteq
W({R})\enspace.$

###### Proof

Let
$s\in\mathit{SafePred}(W({R})\cup\mathit{WinningMoves}(W({R})),\mathit{Uncontrollable}(W({R})))$.

There exists $s^{\prime}\in W({R})\cup\mathit{WinningMoves}(W({R}))$ and
$\delta\geq 0$ such that $s\to^{\delta}s^{\prime}$ and
$\mathit{Cover}(s\to^{\delta}s^{\prime})\cap\mathit{Uncontrollable}(W({R}))=\emptyset$.

We define a controller strategy $\sigma_{c}$ from $s$ such that
$\sigma_{c}(s)=\delta$. If $s^{\prime}$ is not winning, it is in
$\mathit{WinningMoves}(W)$ and thus have a controllable discrete transition
$t_{c}$ leading to a state $s^{\prime\prime}$ such that $s^{\prime\prime}$ is
in $W({R})$. In this case, we set $\sigma_{c}(s,s^{\prime})=t_{c}$.

Now, whatever the environment strategy $\sigma_{e}$, the possible first moves
of the run are limited to $s\to^{\delta}s^{\prime}$ with $s^{\prime}$ winning,
$s\to^{\delta}s^{\prime}\to^{t_{c}}s^{\prime\prime}$ with $s^{\prime\prime}$
winning or $s\to^{\delta_{i}}s_{i}\to^{t_{u}}s_{i}^{\prime}$ with
$s_{i}\in\mathit{Cover}(s\to^{\delta}s^{\prime})$ and $t_{u}\in T_{u}$. Since
$s_{i}\in\mathit{Cover}(s\to^{\delta}s^{\prime})$,
$s_{i}\notin\mathit{Uncontrollable}(W({R}))$ and so $s_{i}^{\prime}$ is
winning.

By definition, for every winning state $s_{w}$, there exists a controller
strategy $\sigma_{c}^{s_{w}}$ that is winning from $s_{w}$. We modify the
strategy $\sigma_{c}$ so that for all the histories $h_{\leq s_{w}}$ described
above ending in a winning state $s_{w}$, the controller continues the run with
the strategy $\sigma^{s_{w}}_{c}$.

For every history $h$ starting in $s_{w}$, we modify strategy $\sigma_{c}$ so
that $\sigma_{c}(h_{\leq s_{w}}\cdot h)=\sigma^{s_{w}}_{c}(h)$. If
$\sigma_{c}^{s_{w}}(\langle s_{w}\rangle)=\delta_{2}\geq 0$ and $h_{\leq
s_{w}}=h_{<s_{w}}\cdot\langle s_{w}^{\prime},s_{w}\rangle$ with
$s_{w}^{\prime}$ and $s_{w}$ the last two states of $h_{\leq s_{w}}$ such that
there exists $\delta_{1}\geq 0$ with $s_{w}^{\prime}\to^{\delta_{1}}s_{w}$, we
modify $\sigma_{c}(h_{<s_{w}})$ to return $\delta_{1}+\delta_{2}$.

Let $\sigma_{e}$ be an environment strategy, $r$ be the run resulting from
$\sigma_{e}$ and $\sigma_{c}$ and $h_{\leq s_{w}}$ the prefix of $r$ ending in
a winning state described above. We call $\sigma_{e}^{s_{w}}$ the environment
strategy from $s_{w}$ such that $\sigma_{e}^{s_{w}}(h)=\sigma_{e}(h_{\leq
s_{w}}\cdot h)$.

We have: $r=h_{\leq s_{w}}\cdot r_{\geq s_{w}}$ where $r_{\geq s_{w}}$ is the
run resulting from $\sigma^{s_{w}}_{c}$ and $\sigma_{e}^{s_{w}}$. Since
$\sigma^{s_{w}}_{c}$ is winning, so is $r_{\geq s_{w}}$. Its cover contains a
state with a target location and is contained in the cover of $r$. Therefore
$r$ is winning and so is $\sigma_{c}$. Finally, $s$ is winning.

###### Lemma 5

Let $S_{1},S_{2}$ such that for $i\in\\{1,2\\}$,
$\mathit{SafePred}(S_{i}\cup\mathit{WinningMoves}(S_{i}),\mathit{Uncontrollable}(S_{i}))\subseteq
S_{i}\enspace.$

Then $\mathit{SafePred}((S_{1}\cap S_{2})\cup\mathit{WinningMoves}(S_{1}\cap
S_{2}),\mathit{Uncontrollable}(S_{1}\cap S_{2}))\subseteq(S_{1}\cap
S_{2})\enspace.$

###### Proof

For $i\in\\{1,2\\}$, $S_{1}\cap S_{2}\subseteq S_{i}$. By monotonicity of
$\mathit{WinningMoves}$ and $\mathit{Uncontrollable}$, we have:
$\mathit{WinningMoves}(S_{1}\cap S_{2})\subseteq\mathit{WinningMoves}(S_{i})$
and $\mathit{Uncontrollable}(S_{1}\cap
S_{2})\supseteq\mathit{Uncontrollable}(S_{i})$. By monotonicity of
$\mathit{SafePred}$, $\mathit{SafePred}((S_{1}\cap
S_{2})\cup\mathit{WinningMoves}(S_{1}\cap
S_{2}),\mathit{Uncontrollable}(S_{1}\cap S_{2}))\subseteq$
$\mathit{SafePred}(S_{i}\cup\mathit{WinningMoves}(S_{i}),\mathit{Uncontrollable}(S_{i}))\subseteq
S_{i}$.

Thus $\mathit{SafePred}((S_{1}\cap S_{2})\cup\mathit{WinningMoves}(S_{1}\cap
S_{2}),\mathit{Uncontrollable}(S_{1}\cap S_{2}))\subseteq(S_{1}\cap S_{2})$.

See 3

###### Proof

Since the property to
$\mathit{SafePred}(S\cup\mathit{WinningMoves}(S),\mathit{Uncontrollable}(S))\subseteq
S$ for a set of states $S$ is stable by intersection, there is a smallest set
$W_{?}$ containing the target states verifying this property.

Let
$s\notin\mathit{SafePred}(W_{?}\cup\mathit{WinningMoves}(W_{?}),\mathit{Uncontrollable}(W_{?}))$,
such that $s.l\notin{R}$ and let $\sigma_{c}$ be a controller strategy from
$s$. We build an environment strategy $\sigma_{e}$ from $s$ defined
recursively on the resulting history of the combined strategy
$\sigma=(\sigma_{c},\sigma_{e})$ such that the resulting run does not enter
$W_{?}$ and thus never reaches the target state.

For $h_{0}=\langle s\rangle$ where $\mathit{Cover}(h_{0})=\\{s\\}$, the
location of $s$ is not a target and $ls(h_{0})=s\notin W_{?}$.

For $n\in\mathbb{N}$, Let $h_{2n}=\langle s_{0},s_{1},s_{2}\ldots
s_{2n}\rangle$ be a history such that there exists an environment strategy
$\sigma_{e}$ defined on the strict prefix of $h_{2n}$, $h_{2n}$ is the prefix
up to rank $2n$ of the resulting run of $\sigma=(\sigma_{c},\sigma_{e})$.
$\mathit{Cover}(h_{2n})$ does not contain a state with a target location,
$s_{2n}\notin W_{?}$. We will prove that either we can extend $\sigma_{e}$ on
$h_{2n}$ such that the resulting run of $\sigma=(\sigma_{c},\sigma_{e})$ is
$s_{0},s_{1},s_{2},\ldots s_{2n}$ and is losing, or we can extend the history
to $h_{2n+2}=h_{2n}\cdot\langle s_{2n},s_{2n+1},s_{2n+2}\rangle$ such that
$\mathit{Cover}(h_{2n})$ does not contain a state with a target location,
$s_{2n}\notin W_{?}$, and we can extend $\sigma_{e}$ on $h_{2n}$ and
$h_{2n+1}$ such that $h_{2n+2}$ is the prefix up to rank $2n+2$ of the
resulting run of $\sigma=(\sigma_{c},\sigma_{e})$.

If $\sigma_{c}(h_{2n})=\infty$, we set $\sigma_{e}(h_{2n})=\infty$ and the
resulting run ends here. The run cover is
$\mathit{Cover}(h_{2n})\cup\mathit{Cover}(s_{2n})$. By recurrence hypothesis,
$\forall s\in\mathit{Cover}(h_{2n}),\;s.l\notin{R}$. Since $s_{2n}$ is not
winning, its location is not in ${R}$ and $\forall
s\in\mathit{Cover}(s_{2n}),\;s.l\notin{R}$ thus the run is losing.

Else there is a delay $\delta\geq 0$ followed by a controllable transition
$t_{c}$ and two states $s^{\prime},s^{\prime\prime}$ such that
$s_{2n}\to^{\delta}s^{\prime}\to^{t_{c}}s^{\prime\prime}$ and if
$\sigma_{c}(h_{2n})=t_{c}$ if $\delta=0$ or $\sigma_{c}(h_{2n})=\delta$ and
$\sigma_{c}(h_{2n}\cdot\langle s_{2n},s^{\prime}\rangle)=t_{c}$. Since
$s_{2n}\notin\mathit{SafePred}(W_{?}\cup\mathit{WinningMoves}(W_{?}),\mathit{Uncontrollable}(W_{?}))$,
there are two possibilities. First, $s^{\prime\prime}\notin W_{?}$. In that
case, we set $\sigma_{e}(h_{2n})=\infty$ and we let the transition happen.
$s_{2n+1}=s^{\prime}$, $s_{2n+2}=s^{\prime\prime}$, all states in
$\mathit{Cover}(s_{2n}\to^{\delta}s_{2n+1})$ are in location
$s_{2n}.l\notin{R}$ and $s_{2n+2}\notin W_{?}$. Second possibility, there is a
state $s_{i}\in\mathit{Cover}{(s_{2n}\to^{\delta}s^{\prime})}$, a delay
$0\leq\delta_{i}\leq\delta$, an uncontrollable transition $t_{u}$ and a state
$s_{i}^{\prime}$ such that
$s_{2n}\to^{\delta_{i}}s_{i}\to^{t_{u}}s_{i}^{\prime}$ and
$s_{i}^{\prime}\notin W_{?}$. We set $\sigma_{e}(h_{2n})=\delta_{i}$ and
$\sigma_{e}(h_{2n}\cdot\langle s_{2n},s_{i}\rangle)=t_{u}$. Since
$\sigma_{e}(h_{2n})=\delta_{i}\leq\delta=\sigma_{c}(h_{2n})$, the next states
of the run are $s_{2n+1}=s_{i}$ and $s_{2n+2}=s_{i}^{\prime}$. All states in
$\mathit{Cover}(s_{2n}\to^{\delta}s_{2n+1})$ are in location
$s_{2n}.l\notin{R}$ and $s_{2n+2}\notin W_{?}$.

Thus, either the resulting run of $\sigma_{c}$ and $\sigma_{e}$ ends and is
losing, or it is infinite and its cover is the union of the covers of its
histories which does not contain states with a target location. Therefore, the
run is losing and $s$ is not in $W_{?}$.

Finally, we get $W_{?}\subseteq W({R})$ and since $W_{?}$ is the smallest set
containing the target states where
$\mathit{SafePred}(S\cup\mathit{WinningMoves}(S),\mathit{Uncontrollable}(S))\subseteq
S$ holds and since $W({R})\subseteq W_{?}$, we obtain $W({R})=W_{?}$.

##  Appendix 0.B Proof of the Correctness of the Algorithm

Recall that
$W_{temp}=\underset{\xi\in\mathit{Explored}}{\bigcup}\\{\xi\\}\times W[\xi]$.

See 4.1

To prove this theorem, we will need a few auxiliary invariants:

###### Theorem 0.B.1

The following invariants stay true throughout the execution of the algorithm :

  1. 6.

$\mathit{WaitingExplore}\cup\mathit{Explored}\subseteq Reach(\xi_{0})$

  2. 7.

$\forall\xi,\;\mathit{Depends}[\xi]=\\{\xi^{\prime}\in\mathit{Explored}\;|\;\xi^{\prime}\Rightarrow^{t}\xi\\}$

  3. 8.

$\mathit{WaitingUpdate}\subseteq\mathit{Explored}$

###### Proof

of Thms. 4.1 and 0.B.1

  1. 1.

The algorithm begins with the exploration of $\xi_{0}^{\nearrow}$ at the end
of which it is added to $\mathit{Explored}$. At no point in the algorithm do
we remove symbolic states from $\mathit{Explored}$.

  2. 2.

A symbolic state $\xi$ is added to $\mathit{Explored}$ at the end of its
exploration. During the exploration, all symbolic states $\xi^{\prime}$ such
that $\xi\Rightarrow^{t}\xi^{\prime}$ are observed by going through all
transitions $t_{s}$ from $\xi$ and computing $Succ(t_{s},\xi)^{\nearrow}$
which corresponds to the symbolic state $\xi_{s}$ such that
$\xi\Rightarrow^{t_{s}}\xi_{s}$. They are added to $\mathit{WaitingExplore}$
if they are not already part of
$\mathit{WaitingExplore}\cup\mathit{Explored}$. From there, we never remove a
symbolic state from $\mathit{Explored}$ and when we remove a symbolic state
from $\mathit{WaitingExplore}$, we do so at the end of its exploration and
thus it is added to $\mathit{Explored}$. Thus, nothing is ever removed from
$\mathit{WaitingExplore}\cup\mathit{Explored}$.

  3. 3.

A symbolic state is added to $\mathit{Explored}$ and removed from
$\mathit{WaitingExplore}$ at the end of its exploration. After that, it is
never removed from $\mathit{Explored}$ and thus can’t be added back in
$\mathit{WaitingExplore}$. It is thus explored only once during which we add
$\xi$ to $\mathit{Win}[\xi]$ if $\xi.l\in{R}$. It cannot be updated
beforehand, as $\mathit{WaitingUpdate}\subseteq\mathit{Explored}$ and
afterwards $\mathit{Win}[\xi]$ can only be modified during an update. During
an update, $\mathit{Win}[\xi]$ gets $\mathit{Win}[\xi]\cap\mathit{NewWin}$ and
thus can only grow. Thus, $\mathit{Win}[\xi]$ always contains $\xi$ if
$\xi.l\in{R}$ after its exploration.

  4. 4.

For all symbolic states $\xi$, before exploration we have
$\mathit{Win}[\xi]=\emptyset\subseteq W$. After exploration, but before the
first update, if $\xi.l\in{R}$, all state in $Symbstate$ are winning by having
a target location and $\mathit{Win}[\xi]=\xi\subseteq W$.

The operator $\mathit{SafePred}(S_{1},S_{2})$ computes temporal predecessor of
$S_{1}$ avoiding $S_{2}$. The temporal transition relation in the enhanced
game arena is $\leadsto^{\delta_{s}}\;=\;(=_{S}\times\to^{\delta_{s}})$, which
remains in the same symbolic state. Therefore:

     * •

$\mathit{SafePred}(W_{temp}\cup\mathit{WinningMoves}(W_{temp}),\>\mathit{Uncontrollable}(W_{temp}))\cap(\\{\xi\\}\times\xi)$
${}=\mathit{SafePred}((W_{temp}\cup\mathit{WinningMoves}(W_{temp}))\cap(\\{\xi\\}\times\xi),\>\mathit{Uncontr}(W_{temp})\cap(\\{\xi\\}\times\xi))$.

     * •

$\mathit{WinningMoves}(W_{temp})\cap(\\{\xi\\}\times\xi)=\underset{t_{c}\in
T_{c}}{\bigcup}Pred(t_{c},W_{temp})\cap(\\{\xi\\}\times\xi)=\underset{t_{c}\in
T_{c}(\xi)}{\bigcup}Pred(t_{c},W_{temp})$, where $T_{c}(\xi)$ are controllable
actions from $\xi$.

     * •

$\mathit{Uncontrollable}(W_{temp})\cap(\\{\xi\\}\times\xi)=\underset{t_{u}\in
T_{u}}{\bigcup}Pred(t_{u},S\backslash
W_{temp})\cap(\\{\xi\\}\times\xi)=\underset{t_{u}\in
T_{u}(\xi)}{\bigcup}Pred(t_{u},S\backslash W_{temp})$; $T_{u}(\xi)$ are
uncontrollable actions from $\xi$.

Thus, $\mathit{WinningMoves}$ corresponds to
$\mathit{WinningMoves}(W_{temp})\cap(\\{\xi\\}\times\xi)$ and
$\mathit{Uncontrollable}$ corresponds to
$\mathit{Uncontrollable}(W_{temp})\cap(\\{\xi\\}\times\xi)$, during an update
of $\xi$. By monotony, since $W_{temp}\subseteq W$, we have
$\mathit{WinningMoves}(W_{temp})$ ${}\subseteq\mathit{WinningMoves}(W)$,
$\mathit{Uncontrollable}(W)\subseteq\mathit{Uncontrollable}(W_{temp})$. Thus:

$\displaystyle\mathit{NewWin}$ $\displaystyle=\ $
$\displaystyle\mathit{SafePred}(W_{temp}\cup\mathit{WinningMoves}(W_{temp}),\>\mathit{Uncontrollable}(W_{temp}))\cap(\\{\xi\\}\times\xi)$
$\displaystyle\subseteq\ $
$\displaystyle\mathit{SafePred}(W\cup\mathit{WinningMoves}(W),\>\mathit{Uncontrollable}(W))\cap(\\{\xi\\}\times\xi)$
$\displaystyle\subseteq\ $
$\displaystyle\mathit{SafePred}(W\cup\mathit{WinningMoves}(W),\mathit{Uncontrollable}(W))$
$\displaystyle\subseteq\ $ $\displaystyle W$

We conclude that all new states added to $\mathit{Win}[\xi]$ are winning.

  5. 5.

When a Symbolic state is explored, it is added to $\mathit{WaitingUpdate}$.

During an update of $\xi$, we recall that

     * •

$\mathit{WinningMoves}$ corresponds to
$\mathit{WinningMoves}(W_{temp})\cap(\\{\xi\\}\times\xi)$ and

     * •

$Uncontrollable$ corresponds to
$\mathit{Uncontrollable}(W_{temp})\cap(\\{\xi\\}\times\xi)$ and

     * •

$\mathit{SafePred}(Win[\xi]\cup\mathit{WinningMoves},\mathit{Uncontrollable})\cap\xi$
corresponds to
$\mathit{SafePred}(W_{temp}\cup\mathit{WinningMoves}(W_{temp}),\>\mathit{Uncontrollable}(W_{temp}))\cap(\\{\xi\\}\times\xi)$.

A symbolic state $\xi$ is removed from $\mathit{WaitingUpdate}$ at the end of
an update. Adding
$\mathit{SafePred}(Win[\xi]\cup\mathit{WinningMoves},\mathit{Uncontrollable})\cap\xi$
to $\mathit{Win}[\xi]$, corresponds to adding to $W_{temp}$ the set
$\mathit{SafePred}(W_{temp}\cup\mathit{WinningMoves}(W_{temp}),\>\mathit{Uncontrollable}(W_{temp}))\cap(\\{\xi\\}\times\xi)$.

We thus have

${{\mathit{SafePred}({W_{temp}}\cup{\mathit{WinningMoves}(W_{temp})},\>\mathit{Uncontrollable}(W_{temp}))}\cap{\xi}}\subseteq{W_{temp}}\enspace$

Consequently, or simultaneously in the case of a self loop, the value of
$\mathit{SafePred}(W_{temp}\cup\mathit{WinningMoves}(W_{temp}),\>\mathit{Uncontrollable}(W_{temp}))\cap\xi$
may change only if the value of $\mathit{Win}[\xi^{\prime}]$ is modified where
$\xi\Rightarrow^{t}\xi^{\prime}$. In that case,
$\mathit{Depends}[\xi^{\prime}]=\\{\xi^{\prime\prime}\in\mathit{Explored}\;|\;\xi^{\prime\prime}\Rightarrow^{t}\xi^{\prime}\\}$
is added to $\mathit{WaitingUpdate}$. Thus, $\xi$ is added back to
$\mathit{WaitingUpdate}$.

  6. 6.

The initial value of $\mathit{WaitingExplore}\cup\mathit{Explored}$ is
$\\{\xi_{0}^{\nearrow}\\}$ which is included in $Reach(\xi_{0})$. From there,
a symbolic state $\xi^{\prime}$ is added to
$\mathit{WaitingExplore}\cup\mathit{Explored}$ when it is reachable in one
transition from a symbolic state $\xi$ being explored. $\xi$ is thus currently
in
$\mathit{WaitingExplore}\in\mathit{WaitingExplore}\cup\mathit{Explored}\subseteq
Reach(\xi_{0})$. Consequently, $\xi^{\prime}$ is also a subset of
$Reach(\xi_{0})$.

  7. 7.

$\forall\xi,\xi^{\prime}$ symbolic states such that
$\xi\Rightarrow_{t}\xi^{\prime}$, if $\xi$ enters $\mathit{Explored}$, it is
at the end of its exploration during which it is added to
$\mathit{Depends}[\xi^{\prime}]$. From there, $\xi$ is never removed from
either $\mathit{Explored}$ or $\mathit{Depends}[\xi^{\prime}]$.

  8. 8.

A symbolic state enters $\mathit{WaitingUpdate}$ either at the end of its
exploration when it is added to $\mathit{Explored}$ or from a
$\mathit{Depends}[\xi^{\prime}]$. By the previous point
$\mathit{Depends}[\xi^{\prime}]\subseteq\mathit{Explored}$.

See 4.2

###### Proof

If the algorithm terminates, the waiting lists are empty. We then have :

  * •

$\xi_{0}^{\nearrow}\in\mathit{Explored}$.

  * •

$\forall\xi\in\mathit{Explored},\forall\xi^{\prime}$ such that
$\xi\Rightarrow^{t}\xi^{\prime}:\xi^{\prime}\in\mathit{Explored}$.

We can then conclude that the union of the explored symbolic states covers
$Reach(\xi_{0})$. We also have, for all $\xi\in\mathit{Explored}$:

  * •

If $\xi.l\in{R}$, then $\\{\xi\\}\times\xi\subseteq W_{temp}$.

  * •

$W_{temp}\subseteq W$.

  * •

$\mathit{SafePred}(W_{temp}\cup\mathit{WinningMoves}(W_{temp}),\>\mathit{Uncontrol}(W_{temp}))\cap(\\{\xi\\}\times\xi)\subseteq
W_{temp}$.

From there, we have the following:

$\displaystyle\mathit{SafePred}(W_{temp}\cup\mathit{WinningMoves}(W_{temp}),\>\mathit{Uncontrollable}(W_{temp}))$
$\displaystyle=\ $
$\displaystyle\underset{\xi\in\mathit{Explored}}{\bigcup}\mathit{SafePred}(W_{temp}\cup\mathit{WinningMoves}(W_{temp}),\>\mathit{Uncontrol}(W_{temp}))\cap(\\{\xi\\}\times\xi)$
$\displaystyle\subseteq\ $ $\displaystyle W_{temp}$

Using the fixed point definition of winning states, we can conclude that
$W_{temp}$ is the set of winning states of $\mathbb{S}_{alg}$ over the
symbolic states in $\mathit{Explored}$ and thus
$\underset{\xi\in\mathit{Explored}}{\bigcup}Win[\xi]$ is the set of winning
states in the initial game restricted to
$\underset{\xi\in\mathit{Explored}}{\bigcup}\xi$, which covers
$Reach(\xi_{0})$.

Since all runs and histories of the game are defined from an initial state,
they are contained in $Reach(\xi_{0})$. Strategies of the game are defined on
histories contained in $Reach(\xi_{0})$, therefore they are strategies of the
game restricted to $Reach(\xi_{0})$ and an initial state is winning if and
only if it is winning on $Reach(\xi_{0})$.

Then, the winning constraint on the parameters is the projection of the
winning initial states on the parameters:

$\mathit{WinningParam}=\underset{\xi\in\mathit{Explored}}{\bigcup}(Win[\xi]\cap\xi_{0}){\downarrow_{P}}\enspace$

##  Appendix 0.C Imitator Model of the Production Cell

An Imitator model of the 1-plate production cell can be seen in Figs. 2, 3 and
4. The model is composed of three automata: the plate, the robot and the
broadcaster. Arrows with same color signify a synchronized action in Imitator.

Figure 2: Imitator model for the Production Cell – plate component
Figure 3: Imitator model for the Production Cell – robot component

Figure 4: Imitator model for the Production Cell – broadcaster component
(auxiliary automaton to facilitate broadcast communication)