This paper introduces a new subclass of Parametric Timed Automata with parametric clock updates, enabling decidability of the EF-emptiness problem and exact synthesis of parameter valuations for reachability.
Contribution
It defines a novel subclass of PTAs with parametric updates where EF-emptiness is decidable and allows exact synthesis, a first in extended PTAs.
Findings
01
Decidability of EF-emptiness in the new subclass.
02
Exact synthesis of parameter valuations for reachability.
03
First non-trivial subclass of extended PTAs with this property.
Abstract
We introduce a new class of Parametric Timed Automata (PTAs) where we allow clocks to be compared to parameters in guards, as in classic PTAs, but also to be updated to parameters. We focus here on the EF-emptiness problem: "is the set of parameter valuations for which some given location is reachable in the instantiated timed automaton empty?". This problem is well-known to be undecidable for PTAs, and so it is for our extension. Nonetheless, if we update all clocks each time we compare a clock with a parameter and each time we update a clock to a parameter, we obtain a syntactic subclass for which we can decide the EF-emptiness problem and even perform the exact synthesis of the set of rational valuations such that a given location is reachable. To the best of our knowledge, this is the first non-trivial subclass of PTAs, actually even extended with parametric updates, for which this…
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
\lsuperaUniversité de Lorraine, CNRS, Inria, LORIA, F-54000 Nancy, France; JFLI, CNRS, Tokyo, Japan; and National Institute of Informatics, Tokyo, Japan
,
Didier Lime\rsuperb
\lsuperbÉcole Centrale de Nantes, LS2N, CNRS, UMR 6004, Nantes, France
and
Mathias Ramparison\rsuperc
\lsupercUniversité Sorbonne Paris Nord, LIPN, CNRS, UMR 7030, F-93430, Villetaneuse, France; University of Luxembourg, Luxembourg; and Univ. Grenoble Alpes, CNRS, UMR 5104, Grenoble INP, VERIMAG, Grenoble, France
Abstract.
We introduce a new class of Parametric Timed Automata (PTAs) where we allow
clocks to be compared to parameters in guards, as in classic PTAs, but also to be updated to parameters.
We focus here on the EF-emptiness problem: “is the set of parameter valuations for which some given location is reachable in the instantiated timed automaton empty?”.
This problem is well-known to be undecidable for PTAs, and so it is for our extension.
Nonetheless, if we update all clocks each time we compare a clock
with a parameter and each time we update a clock to a parameter, we obtain
a syntactic subclass for which we can decide the EF-emptiness problem
and even perform the exact synthesis of the set of rational
valuations such that a given location is reachable. To the best of our knowledge, this is the first non-trivial subclass of PTAs, actually even extended with parametric updates, for which this is possible.
This work is partially supported by the ANR national research program PACS (ANR-14-CE28-0002) and by the ANR-NRF French-Singaporean research program ProMiS (ANR-19-CE25-0015). É. André was partially supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST
1. Introduction
Timed automata (TAs) are a powerful formalism to model and verify timed concurrent systems, both expressive enough to model many interesting systems and enjoying several decidability properties.
In particular, the reachability of a discrete state is decidable and PSPACE-complete [AD94].
In TAs, clocks can be compared with constants in guards, and can be updated to 0 (“reset”) along edges.
Timed automata may turn insufficient to verify systems where the timing constants themselves are subject to some uncertainty, or when they are simply not known at the early design stage.
Parametric timed automata (PTAs) [AHV93] address this drawback by allowing parameters (unknown constants) in the timing constraints; this high expressive power comes at the cost of the undecidability of most interesting problems (see e.g. [And19]).
In particular, the basic problem of EF-emptiness (“is the set of valuations for which a given location is reachable in the instantiated timed automaton empty?”) is “robustly” undecidable: even for a single rational-valued [Mil00] or integer-valued parameter [AHV93, BBLS15], or when only strict constraints are used [Doy07].
A famous syntactic subclass of PTAs that enjoys limited decidability is L/U-PTAs [HRSV02], where the parameters set is partitioned into lower-bound and upper-bound parameters, i. e., parameters that can only be compared to a clock as a lower-bound (resp. upper-bound).
The EF-emptiness problem is decidable for L/U-PTAs [HRSV02, BL09] and for PTAs under several restrictions [BO14]; however, most other problems
are undecidable (e.g. [BL09, Qua14, JLR15, ALR16, AL17, ALM20]) (see [And19] for a survey).
Recall that the EF-emptiness problem is decidable for L/U-PTAs [HRSV02, BL09] and for PTAs under several restrictions [BO14]; however, most other problems
are undecidable (e.g. [BL09, Qua14, JLR15, ALR16, AL17]) (see [And19] for a survey).
1.1. Contribution
We investigate parametric updates, which can model an unknown timing configuration in a system where processes need to synchronize together on common events, as in e.g. programmable controller logic programs with concurrent tasks execution.
We show that the EF-emptiness problem is decidable for PTAs augmented with parametric updates (i. e., U2P-PTA), with the additional condition that whenever a clock is compared to a parameter in a guard or updated to a parameter, all clocks must be updated (possibly to parameters)—this gives R-U2P-PTA.
This result holds when the parameters are bounded rationals in guards, and possibly unbounded rationals in updates.
Non-trivial decidable subclasses of PTAs are a rarity (to the best of our knowledge, only L/U-PTAs [HRSV02] and integer-points (IP-)PTAs [ALR16]); this makes our positive result very welcome.
In addition, not only the emptiness is decidable, but exact synthesis for bounded rational-valued parameters can be performed—which contrasts with L/U-PTAs and IP-PTAs for which synthesis was shown to be intractable [JLR15, ALR16].
About this manuscript
This is the extended version of [ALR19].
In addition to additional explanations and all proofs of our results, we added the whole new Section 7 adding stopwatches to our formalism.
1.2. Related work
Our construction is reminiscent of the parametric difference bound matrices (PDBMs) defined in [QSW17, section III.C] where the authors in this paper revisit the result of the binary reachability relation over both locations and clock valuations in TAs;
however, parameters of [QSW17] are used to bound in time a run that reaches a given location, while we use parameters directly in guards and resets along the run, which make them active components of the run specifically for intersection with parametric guards, a key point not tackled in [QSW17].
Related DBMs with an additional parameter have been studied, such as shrunk DBMs [SBM14, BMRS19] and infinitesimally enlarged DBMs [San15].
Allowing parameters in clock updates is inspired
by the updatable TA formalism defined in [BDFP04] where clocks can be updated not only to [math] (“reset”) but also to rational constants (“update”).
In [ALR18], we extended the result of [BDFP04] by allowing parametric updates (and no parameter elsewhere, e.g. in guards):
the EF-emptiness is undecidable even in the restricted setting of bounded rational-valued parameters, but becomes decidable when parameters are restricted to (unbounded) integers.
Synthesis is obviously harder than EF-emptiness: only three results have been proposed to synthesize the exact set of valuations for subclasses of PTAs, but they are all concerned with integer-valued parameters [BL09, JLR15, ALR18].
More precisely, it is possible to synthesize unbounded integers for L- or U-PTAs (L/U-PTAs with only lower-bound, or only upper-bound, parameters) [BL09];
bounded integers for PTAs [JLR15]
unbounded integers for timed automata with parametric updates [ALR18].
In contrast, we deal here with (bounded) rational-valued parameters—which makes this result the first of its kind.
The idea of updating all clocks when compared to parameters comes from our class of reset-PTAs briefly mentioned in [ALR16], but not thoroughly studied.
Finally, updating clocks on each transition in which a parameter appears is reminiscent of the initialized rectangular hybrid automata formalism defined in [HKPV98], which remains one of the few decidable subclasses of hybrid automata.
Indeed, timed automata can be defined as a subclass of initialized rectangular hybrid automata where clocks evolve at the same fixed rate, in which diagonal constraints are allowed but not systematically used in practice.
However, besides the fact that in PTAs variables (clocks) evolve at the same rate, in initialized rectangular hybrid automata variables are reset whenever one of the derivatives of those variables changes, which is not at all the condition we use for global updates in our R-U2P-PTA.
1.3. Outline
Section 2 recalls preliminaries. Section 3 presents R-U2P-PTA along with our decidability result. Sections 4 and 5 introduce operations on our p–PDBMs and our extended region automaton.
Section 6 proves the main decidability result.
Section 7 extends our results to stopwatches.
Section 8 gives a concrete application of our result.
Section 9 concludes the paper.
2. Preliminaries
Let N, Z, Q+ and R+ denote the sets of non-negative integers, integers, non-negative rational numbers and non-negative real numbers respectively.
Throughout this paper, we assume a set X={x1,…,xH} of clocks, i. e., real-valued variables evolving at the same rate.
A clock valuation is a function w:X→R+.
We write 0 for the clock valuation that assigns [math] to all clocks.
Given d∈R+, w+d (resp. w−d) denotes the valuation such that (w+d)(x)=w(x)+d (resp. (w−d)(x)=w(x)−d if w(x)−d>0, [math] otherwise), for all x∈X.
We assume a set P={p1,…,pM} of parameters, i. e., unknown constants.
A parameter valuationv is a function v:P→Q+.
We identify a valuation v with the point (v(p1),…,v(pM)) of Q+M.
Given d∈N, v+d (resp. v−d) denotes the valuation such that (v+d)(p)=v(p)+d (resp. (v−d)(p)=v(p)−d if v(p)−d>0, [math] otherwise), for all p∈P.
In the following, we assume ◃∈{<,≤} and ⋈∈{<,≤,≥,>}.
A parametric guardg is a constraint over X∪P defined as the conjunction of inequalities of the form
x⋈z, where x is a clock and z is either a parameter or a constant in Z.
A non-parametric guard is a parametric guard without parameters (i. e., over X).
Given a parameter valuation v, v(g) denotes the constraint over X obtained by replacing in g each parameter p with v(p).
We extend this notation to an expression: a sum or difference of parameters and constants.
Likewise, given a clock valuation w, w(v(g)) denotes the expression obtained by replacing in v(g) each clock x with w(x).
A clock valuation wsatisfies constraint v(g) (denoted by w⊨v(g)) if w(v(g)) evaluates to true.
We say that vsatisfiesg,
denoted by v⊨g,
if the set of clock valuations satisfying v(g) is nonempty.
We say that g is satisfiable if ∃w,v s.t. w⊨v(g).
A parametric update is a partial function u:X⇀N∪P which assigns to some of the clocks an integer constant or a parameter.
For v a parameter valuation, we define a partial function v(u):X⇀Q+ as follows:
for each clock x∈X, v(u)(x)=k∈N if u(x)=k
and v(u)(x)=v(p)∈Q+ if u(x)=p a parameter.
A non-parametric update is unp:X⇀N.
The term reset has been used for clock updates to values different from [math] in [BY03].For a clock valuation w and a parameter valuation v, we denote by [w]v(u)
the clock valuation obtained after applying v(u).
We first define a new class of parametric timed automata and then define
plain parametric timed automata and timed automata as special cases.
Definition 2.1**.**
An update-to-parameter PTA (U2P-PTA)
A is a tuple
[TABLE]
where:
(1)
Σ is a finite set of actions,
2. (2)
L is a finite set of locations,
3. (3)
ℓ0∈L is the initial location,
4. (4)
X is a finite set of clocks,
5. (5)
P is a finite set of parameters,
6. (6)
ζ is a finite set of edges e=⟨ℓ,g,a,u,ℓ′⟩
where
ℓ,ℓ′∈L are the source and target locations, g is a parametric guard, a∈Σ and
u:X⇀N∪P is a parametric update function.
An U2P-PTA is depicted in Figure 1. Note that all clocks are updated whenever there is a comparison with a parameter (as in {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{newBlock}}) or a clock is updated to a parameter (as in {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{blockSolution_{x}}}).
Given a parameter valuation v, we denote by v(A) the structure where all occurrences of a parameter pi have been replaced by v(pi).
If v(A) is such that all constants in guards and updates are integers, then v(A) is a updatable timed automaton [BDFP04]
but will be called timed automaton (TA) for the sake of simplicity in this paper.
In the following, we may denote as a timed automaton any structure v(A), by assuming a rescaling of the constants:
by multiplying all constants in v(A) by their least common denominator,
we obtain an equivalent timed automaton (with integer constants).
A bounded U2P-PTA is a U2P-PTA with a bounded parameter domain that assigns to each parameter a minimum integer bound and a maximum integer bound.
That is, each parameter pi ranges in an interval [ai,bi], with ai,bi∈N.
Hence, a bounded parameter domain is a hyperrectangle of dimension M.
A parametric timed automaton (PTA) [AHV93] is a U2P-PTA where, for any edge e=⟨ℓ,g,a,u,ℓ′⟩∈ζ, u:X⇀{0}.
Definition 2.2** (Concrete semantics of a TA).**
Given a U2P-PTA A=(Σ,L,ℓ0,X,P,ζ), and a parameter valuation v,
the concrete semantics of v(A) is given by the timed transition system (S,s0,→), with
•
S={(ℓ,w)∈L×R+H},
s0=(ℓ0,0);
•
→ consists of the discrete and (continuous) delay transition relations:
–
discrete transitions: (ℓ,w)↦e(ℓ′,w′), if (ℓ,w),(ℓ′,w′)∈S, there exists
{mathpar}
e= ⟨ℓ,g,a,u,ℓ’⟩∈ζ, w’= [w]v(u), and w⊧v(g)
–
delay transitions: (ℓ,w)↦d(ℓ,w+d), with d∈R+.
Moreover, we write (ℓ,w)⟶e(ℓ′,w′) for a combination of a delay and discrete transitions where
((ℓ,w),e,(ℓ′,w′))∈→ if
∃d,w′′:(ℓ,w)↦d(ℓ,w′′)↦e(ℓ′,w′).
Given a TA v(A) with concrete semantics (S,s0,→),
we refer to the states of S as the concrete states of v(A).
A (concrete) run of v(A) is a possibly infinite alternating sequence of concrete states of v(A) and edges starting from the initial concrete state s0 of the form
s0⟶e0s1⟶e1⋯⟶em−1sm⟶em⋯, such that for all
i=0,1,…, ei∈ζ, and (si,ei,si+1)∈→.
Given a state s=(ℓ,w), we say that s is reachable (or that v(A) reaches s) if s belongs to a run of v(A).
By extension, we say that ℓ is reachable in v(A), if there exists a state (ℓ,w) that is reachable.
Throughout this paper, let K denotes the largest constant in a given U2P-PTA, i. e., the maximum of the largest constant compared to a clock in a guard and the largest upper bound of a parameter (if the U2P-PTA is bounded).
Let us recall the notion of clock region [AD94].
Given a clock x and a clock valuation w, recall that ⌊w(x)⌋ denotes the integer part of w(x) while frac(w(x)) denotes its fractional part.
We define the same notation for parameter valuations.
Definition 2.3** (clock region).**
For two clock valuations w and w′, ∼ is an equivalence relation defined by: w∼w′ iff
(1)
for all clocks x, either ⌊w(x)⌋=⌊w′(x)⌋ or w(x),w′(x)>K;
2. (2)
for all clocks x,y with w(x),w(y)≤K,
frac(w(x))≤frac(w(y)) iff frac(w′(x))≤frac(w′(y));
3. (3)
for all clocks x with w(x)≤K, frac(w(x))=0 iff frac(w′(x))=0.
A clock regionRc is an equivalence class of ∼.
Two clock valuations in the same clock region (cf. Definition 2.3) reach the same regions by time elapsing, satisfy the same guards and can take the same transitions [AD94].
In this paper, we address the EF-emptiness problem:
given a U2P-PTA A and a location ℓ, is set of valuations v such that there is a run in v(A) reaching ℓ is empty?
More formally, the problem can be written as:
EF**-emptiness problem:
**Input: a U2P-PTA A and a location ℓ
Problem: {v∣∃s0⟶e0(ℓ1,w1)⟶e1⋯⟶em−1(ℓ,w) a run of v(A)}=∅?
3. A decidable subclass of U2P-PTAs
We now impose that, whenever a guard or an update along an edge contains parameters, then all clocks must be updated (to constants or parameters).
Our main contribution is to prove that this restriction makes EF-emptiness decidable.
Definition 3.1**.**
An R-U2P-PTA is a U2P-PTA where for any edge ⟨ℓ,g,a,u,ℓ′⟩∈ζ,
u is a total function whenever:
(1)
g is a parametric guard, or
2. (2)
u(x)∈P for some x∈X.
Both conditions of Definition 3.1 are necessary. If we allow parametric guards to be passed without a full update of clocks, then we obtain a larger class of PTAs for which the EF-emptiness problem is undecidable as it is for regular PTAs [AHV93]. If we allow partial parametric updates of clocks, then we obtain a larger class of Reset-to-Parameter Timed Automaton defined in [ALR18] for which we proved the EF-emptiness problem is undecidable.
In the following we only consider either non-parametric, or (necessarily total) fully parametric update functions.
A total update function which is not fully parametric (i. e., an update of some clocks to parameters and all others to constants)
can be encoded as a total fully parametric update immediately followed by a (partial) non-parametric update function.
The main idea for proving decidability is the following: given an R-U2P-PTA A we will construct a finite region automaton that bisimulates A, as in TA [AD94].
Our regions will contain both clocks and parameters and will be a finite number, due to the finite number of parameter and their construction similar to clock regions [AD94].
Since parameters are allowed in guards,
we need to construct parameter regions and more restricted clock regions.
We will define a form of Parametric Difference Bound Matrices (viz., p–PDBMs for precise PDBMs, inspired by [HRSV02]) in which, once valuated by a parameter valuation,
two clock valuations have the same discrete behavior and satisfy the same non-parametric guards. A p–PDBM will define the set of clocks and parameter valuations that satisfies it, while once valuated by a parameter valuation, a valuated p–PDBM will define the set of clock valuations that satisfies it.
A key point is that in our p–PDBMs the parametric constraints used in the matrix will be defined from a finite set of predefined expressions involving parameters and constants, and we will prove that this defines a finite number of p–PDBMs. Decidability will come from this fact: the region automaton will evolve in this finite and stable set of p–PDBMs under time elapsing and update operators.
We define this set of parametric constraints (PLT for parametric linear term) as follows:
PLT={frac(pi),1−frac(pi),frac(pi)−frac(pj),frac(pj)+1−frac(pi),1,0,frac(pi)−1−frac(pj),−frac(pi),frac(pi)−1},
for all 1≤i,j≤M.
Given a parameter valuation v and d∈PLT, we denote by v(d) the term obtained by replacing in d each parameter p by v(p).
Let us now define an equivalence relation between parameter valuations v and v′.
Definition 3.2** (regions of parameters).**
We write that v⌢v′ if
(1)
for all parameters p, ⌊v(p)⌋=⌊v′(p)⌋;
2. (2)
for all d1,d2,d3∈PLT, v(d1)≤v(d2)+v(d3)
iff v′(d1)≤v′(d2)+v′(d3).
Parameter regions are defined as the equivalence classes of ⌢, and we will use the notation Rp for parameter regions.
The set of all parameter regions is denoted by Rp.
The definition is in a way similar to Definition 2.3 but also involves comparisons of sums of elements of PLT. In fact, we will need this kind of comparisons to define our p–PDBMs. Nonetheless we do not need more complicated comparisons as in R-U2P-PTA whenever a parametric guard or updated is met the update is a total function: this preserves us from the parameter accumulation, e.g. obtaining expressions of the form 5frac(pi)−1−3frac(pj) (that may occur in usual PTAs).
In the following, our p–PDBMs will be matrices of
projections on parameters of parametric clock constraints,
written as matrices of pairs of the form D=(d,◃) where d∈PLT.
We therefore need to define comparisons on these pairs.
We define an associative and commutative operator ⊕ as ◃1⊕◃2=< if ◃1=◃2, or ◃1 if ◃1=◃2.
We define D1+D2=(d1+d2,◃1⊕◃2).
Following the idea of parameter regions, we define the validity of a comparison
between pairs of the form (di,◃i) within a given parameter region,
i. e., whether the comparison is true for all parameter valuations v in the parameter region Rp.
Definition 3.3** (validity of comparison).**
Let Rp be a parameter region.
Given any two linear terms d1,d2 over P (i. e., of the form ∑iαipi+d with αi,d∈Z),
the comparison (d1,◃1)◃(d2,◃2) is valid for Rp if:
(1)
◃=<, and either
(a)
for all v∈Rp, v(d1)<v(d2) evaluates to true regardless of ◃1,◃2,
or
2. (b)
for all v∈Rp, v(d1)≤v(d2) evaluates to true,
◃1=< and ◃2=≤;
2. (2)
◃=≤, and either
(a)
for all v∈Rp, v(d1)<v(d2) evaluates to true regardless of ◃1,◃2, or
2. (b)
for all v∈Rp, v(d1)≤v(d2) evaluates to true, and
◃1=◃2, or ◃1=<.
Transitivity is immediate from the definition: if D1◃1D2 and D2◃2D3 are valid for Rp, D1(◃1⊕◃2)D3 is valid for Rp.
Let d1,d2,d3,d4∈PLT. Let Rp be a parameter region.
If (d1,◃1)≤(d2,◃2) and (d3,◃3)≤(d4,◃4) are valid for Rp
then (d1,◃1)+(d3,◃3)≤(d2,◃2)+(d4,◃4) is valid for Rp.
We can now define our data structure, namely p–PDBMs (for precise Parametric Difference Bound Matrices),
inspired by the PDBMs of [HRSV02]; PDBMs were themselves inspired by the DBMs of [Dil89]. However, our p–PDBM compare differences of fractional parts of clocks, instead of clocks as in classical DBMs; therefore, our p–PDBMs are closer to
clock regions than to DBMs and fully contained into clock regions of [AD94].
A p–PDBM is a pair made of an integer vector (encoding the clocks integer part), and a matrix (encoding the parametric differences between any two clock fractional parts).
Their interpretation also follows that of PDBMs and DBMs:
for i=0, the matrix cell Di,0=(di,0,◃i0) is interpreted as the constraint frac(xi)◃i0di,0,
and D0,i=(d0,i,◃0i) as the constraint −frac(xi)◃0id0,i.
For i=0 and j=0,
the matrix cell Di,j=(di,j,◃ij) is interpreted as frac(xi)−frac(xj)◃ijdi,j.
Finally for all i, Di,i=(0,≤).
Our p–PDBMs are partitioned into two types: open–p–PDBMs and point–p–PDBMs.
A point–p–PDBM is a clock region defined by only parameters which contains only one clock valuation;
that is, it corresponds to a set of inequalities of the form xi≤pj∧pj≤xi.
In contrast, an open–p–PDBM is a clock region which can contain several clock valuations satisfying some possibly parametric constraints,
or contain at least one clock valuation satisfying non-parametric constraints (as the corner-point of [AD94]).
In particular, the initial clock region {0H} and any clock region {EiH} where Ei is an integer for all clock xi, is an open–p–PDBM.
Basically, only the first p–PDBM after a (necessarily total) parametric clock update will be a point–p–PDBM; any following p–PDBM will be an open–p–PDBM until the next (total) parametric update.
The following two definitions impose several conditions to p–PDBMs that ensure we build satisfiable ones.
Definition 3.5** (open–p–PDBM).**
Let Rp be a parameter region.
An open–p–PDBM for Rp is a pair (E,D) with E=(E1,…,EH) a vector of H integers (or ∞) which is the integer part of each clock,
and D is an (H+1)2 matrix where each element Di,j is a pair (di,j,◃ij) for all 0≤i,j≤H,
where di,j∈PLT. Moreover, for all 0≤i≤H, Di,i=(0,≤).
In addition:
(1)
For all i, (−1,<)≤D0,i≤(0,≤) and (0,≤)≤Di,0≤(1,<) are valid for Rp,
2. (2)
For all i=0,j=0, either (0,≤)≤Di,j≤(1,<) is valid for Rp and (−1,<)≤Dj,i≤(0,≤) is valid for Rp or (0,≤)≤Dj,i≤(1,<) is valid for Rp and (−1,<)≤Di,j≤(0,≤) is valid for Rp.
3. (3)
For all i,j, if di,j=−dj,i and is different from 1 then ◃ij=◃ji=≤, else ◃ij=◃ji=<,
4. (4)
For all i,j,k, Di,j≤Di,k+Dk,j is valid for Rp (canonical form), and
5. (5)
(a)
There is at least one i s.t. Di,0=D0,i=(0,≤), or
2. (b)
there is at least one i s.t. Di,0=(1,<) and for all j s.t. D0,j=(0,◃0j), then we have ◃0j=<.
Condition 1 ensures fractional parts of clocks valuations have only non negative values. Condition 2 ensures the consistency of differences of clocks i. e.,frac(x)−frac(y)≤0 iff 0≤frac(y)−frac(x). Condition 3 ensures the only possible closed sets of clock valuations are parametric singleton of clock valuations. Condition 4 is the canonical form which ensures, as described in [HRSV02, BY03], that the open–p–PDBM has the tightest possible bounds i. e., no constraint frac(x)−frac(y)◃xydx,y can be strengthened without losing solutions.
An open–p–PDBM satisfying condition 5a can be seen as a subregion of an open line segment or a corner point region of [AD94, fig. 9 example 4.4] (it can be seen as a border region)
and one satisfying condition 5b can be seen as a subregion of an open region of [AD94, fig. 9 example 4.4] (it can be seen as a center region).
Remark that sets of the form {frac(w(x))∣0≤frac(w(x))≤1} are forbidden by Definition 3.5 (3), as in the regions of [AD94].
Let Rp be a parameter region.
In the following, p–PDBM■(Rp) is the set of all possible open–p–PDBMs (E,D) for Rp.
This definition is similar to that of [HRSV02, def. 3.1].
The second type is the point–p–PDBM. It represents the unique clock valuation (for a given parameter valuation) obtained after a total parametric update in an U2P-PTA.
Definition 3.6** (point–p–PDBM).**
Let Rp be a parameter region.
A point–p–PDBM for Rp is a pair (E,D) where D is an (H+1)2 matrix
where each element Di,j is a pair (di,j,≤) and for all 0≤i,j≤H,
di,0=frac(p1)=−d0,i,
and di,j=frac(p1)−frac(p2)=−dj,i,
for any p1,p2∈P. and for all 1≤i≤H, Ei=⌊pk⌋ if di,0=frac(pk), for 1≤k≤M.
In addition:
(1)
For all i, (−1,<)≤D0,i≤(0,≤) and (0,≤)≤Di,0≤(1,<) are valid for Rp,
2. (2)
For all i,j,k, Di,j≤Di,k+Dk,j is valid for Rp (canonical form).
The fact that D is antisymmetric i. e., for all i,j, Di,j=−Dj,i,
means that each clock is valuated to a parameter and each difference of clocks is valuated to a difference of parameters. Conditions 1 and 2 are the same as for open–p–PDBMs.
The set of all point–p–PDBM for Rp is denoted by p–PDBM⊙(Rp), and the set of all p–PDBMs for Rp is denoted by p–PDBM(Rp) (hence p–PDBM(Rp)=p–PDBM■(Rp)∪p–PDBM⊙(Rp)).
The use of validity ensures the consistency of the p–PDBM. We denote the set of all p–PDBMs that are valid forRp by p–PDBM(Rp).
Given a p–PDBM (E,D), it defines the subset of RH∪QM
satisfying the constraints ⋀i,j∈[0,H]frac(xi)−frac(xj)◃i,jdi,j∧⋀i∈[1,H]⌊xi⌋=Ei.
Given a p–PDBM (E,D) and a parameter valuation v, we denote by (E,v(D)) the valuated p–PDBM, i. e., the set of clock valuations defined by the inequalities:
[TABLE]
For a clock valuation w, we write w∈(E,v(D)) if it satisfies all constraints of (E,v(D))111If v is a valuation assigning an integer to each parameter, then (E,v(D)) is DBM as defined in [BY03].
.
The following two lemmas derive from the above definitions of point–p–PDBM and p–PDBMs:
Lemma 3.7** (positivity of reflexivity).**
Let Rp be a parameter region and (E,D) be a p–PDBM for Rp.
For all clocks i,j, (0,≤)≤Di,j+Dj,i is valid for Rp.
But let us first clarify our needs graphically.
Intuitively, our p–PDBMs are partitioned into three types.
(1) The point–p–PDBM is a clock region defined by only parameters which contains only one clock valuation;
it represents the unique clock valuation (for a given parameter valuation) obtained after a total parametric update in an U2P-PTA.
Each clock is valuated to a parameter and each difference of clocks is valuated to a difference of parameters (it corresponds to constraints of the form x=p and x−y=pi−pj).
Let v be a parameter valuation. We assume ⌊v(p2)⌋=⌊v(p1)⌋=k∈N and frac(v(p1))>frac(v(p2)).
The p–PDBM obtained after an update u(x)=v(p2)
and u(y)=v(p1) is represented using the following pair (where the indices 0,x,y are shown for the sake of comprehension)
[TABLE]
Once valuated with v, it contains a unique clock valuation. We represent it as the black dot in Figure 2.
(2) In contrast, an open–p–PDBM satisfying condition (5a) is a clock region which can contain several clock valuations satisfying some possibly parametric constraints,
or contain at least one clock valuation satisfying non-parametric constraints (as the corner-point region of [AD94]).
In particular, the initial clock region {0H} and any clock region
that is a single integer clock valuation
is a p–PDBM.
An open–p–PDBM satisfying condition 5a is characterized by at least one clock x s.t. Dx,0=D0,x=(0,≤) and can be seen as a subregion of an open line segment or a corner point region of [AD94, fig. 9 example 4.4].
After an immediate update of x to k, the above p–PDBM (E,D) becomes
[TABLE]
We represent it once valuated with v as the blue dot in Figure 2. The open line segment of [AD94, fig. 9 example 4.4] can be represented as
[TABLE]
and is depicted as the vertical left black line in Figure 2.
(3) An open–p–PDBM satisfying condition (5b) is a clock region which can contain several clock valuations satisfying some possibly parametric constraints
(as the open region of [AD94]).
An open–p–PDBM satisfying condition (5b) is characterized by at least one clock y s.t. Dy,0=(1,<) and for all x s.t. D0,x=(0,◃ox), then we have ◃ox=< and can be seen as a subregion of an open region of [AD94, fig. 9 example 4.4].
After some time elapsing, and before any clock valuation reaches the next integer k+1—therefore the next open–p–PDBM satisfying condition 5a—, the above p–PDBM (E,D) becomes
[TABLE]
We represent it once valuated with v as the red line in Figure 2. The open region of [AD94, fig. 9 example 4.4] can be represented as
[TABLE]
and is depicted as the top left black triangle in Figure 2.
Remark that sets of the form {frac(w(x))∣0≤frac(w(x))≤1} are in contradiction with Definition 3.5 (3) and therefore cannot be part of a p–PDBM, as in the regions of [AD94].
Basically, only the first p–PDBM after a (necessarily total) parametric clock update will be a point–p–PDBM; any following p–PDBM will be a open–p–PDBM satisfying condition 5a or 5b until the next (total) parametric update.
The differentiation made in the previous paragraph between open–p–PDBMs satisfying condition 5a and 5b is intended to give an intuition to the reader about the inclusion of p–PDBMs into [AD94] clock regions.
Technical details are given in the following Section 4.
In the following subsections Sections 4.1, 4.2, 4.3, 4.4 and 4.5, we are going to define operations on p–PDBMs (i. e., update of clocks, time elapsing and guards satisfaction), and will show that the set of p–PDBMs is stable under these operations.
4. Operations on p–PDBMs
4.1. Non-parametric update
To apply a non-parametric update on a p–PDBM, following classical algorithms for DBMs [BY03], we define an update operator, given in Algorithm 1.
Given a p–PDBM (E,D) and unp a non-parametric update function that updates a clock x to k∈N,
update((E,D),unp) defines a new p–PDBM by
(1)
updating Ex to k;
2. (2)
setting the fractional part of x to [math]: Dx,0:=D0,x:=(0,≤);
3. (3)
updating the new difference between fractional parts with all other clocks i, which is the range of values i can currently take: Dx,i:=D0,i and Di,x:=Di,0.
Example 4.1**.**
Here is an open–p–PDBM satisfying condition 5b on the left of the figure below. Formally, it is written:
[TABLE]
After an update of y to k prior to reaching k+1, here is the open–p–PDBM satisfying condition 5a obtained, on the right of the figure below. Formally, it is written:
[TABLE]
Definition 4.2** (update of a p–PDBM).**
Let unp be a non-parametric update function.
Given (E,D)∈p–PDBM(Rp),
we define the update of (E,D),
denoted by (E′,D′)=update((E,D),unp) as: D′ is the result of Algorithm 1 and for each clock x if unp(x) is defined
Ex′:=unp(x), Ex′:=Ex otherwise.
Lemma 4.3** (stability under update).**
Let Rp be a parameter region and
[TABLE]
Let unp be a non-parametric update.
Then update((E,D),unp)∈p–PDBM■(Rp).
Proof.
Intuitively, we update in (E,D) the lower and upper bounds of some clocks to (0,≤) and the difference between two clocks Di,j to D0,j if xi is updated: that is, the new difference between two clocks if one has been updated is just the lower/upper bound of the one that is not updated. This allows us to conserve the canonical form as we only “moved” some cells in D that already verified the canonical form. Therefore update((E,D),unp) is a p–PDBM. See Appendix D for details.
∎
Applying a non-parametric update on any point–p–PDBM transforms it into an open–p–PDBM, and open–p–PDBMs are stable under update.
It can seem a paradox that the (non-parametric) update of a point–p–PDBM becomes an open–p–PDBM;
in fact, it remains geometrically speaking a point, i. e., a singleton containing one clock valuation.
Recall that our open–p–PDBMs include p–PDBMs geometrically corresponding to a point for each valuation.
In contrast, point–p–PDBMs are also punctual (for each valuation), but are fully parametric.
The following lemma states that the update operator behaves as expected.
Lemma 4.4** (semantics of update on p–PDBM(Rp)).**
Let Rp be a parameter region and (E,D)∈p–PDBM(Rp). Let v∈Rp.
Let unp be a non-parametric update.
For all w, [w]unp∈update((E,v(D)),unp) iff w∈(E,v(D)).
Proof.
The technical part is (⇒). The idea is to prove that, given w′∈update((E,v(D)),unp) there is a non-empty set of clock valuations w s.t. w′=[w]unp that is precisely defined by the constraints in (E,v(D)).
See Appendix E for details.
∎
4.2. Parametric update
Given (E,D)∈p–PDBM(Rp) we write update((E,D),u) to denote the update of (E,D) by u, when u is a total parametric update function, i. e., updating the set of clocks exclusively to parameters.
We therefore obtain a point–p–PDBM, containing the parametric constraints defining a unique clock valuation. The semantics is straightforward.
Recall that a total update function which is not fully parametric (i. e., an update of some clocks to parameters and some others to constants) can be encoded as a total parametric update immediately followed by a partial non-parametric update function.
4.3. Time elapsing
Given a parameter region Rp, recall that constraints satisfied by parameters are known, and we can order elements of PLT.
Thanks to this order, within a p–PDBM (E,D)
the clocks with the (possibly parametric) largest fractional part
i. e., the clocks that have a larger fractional part than any other clock,
can always be identified by their bounds in D.
For a p–PDBM (E,D), we define the set of clocks with the largest fractional part (LFP) as LFPRp(D)={x∈[1,H]∣(0,≤)≤Dx,i is valid for Rp, for all 0≤i≤H}.
Clocks belonging to LFP are the first to reach the upper bound 1 by letting time elapse.
Definition 4.5** (clocks with the largest fractional part in a p–PDBM).**
Let Rp be a parameter region and (E,D)∈p–PDBM(Rp).
A clock with the (possibly parametric) largest fractional part is a clock x
s.t. for all 0≤i≤H, (0,≤)≤Dx,i is valid for Rp.
There is at least one clock with the (possibly parametric) largest fractional part:
Lemma 4.6** (existence of a clock with the largest fractional part).**
Let Rp be a parameter region and (E,D)∈p–PDBM(Rp).
There is at least one clock x s.t. for all 0≤i≤H, (0,≤)≤Dx,i is valid for Rp.
Note that several clocks may have the largest fractional parts (up to some syntactic replacements
222Let v∈Rp and suppose, we have two different syntactic expressions, such as p,1−p that are equal once valuated i. e.,v(p)=1−v(p). From Definition 3.2 remark that if it is for v, it is for any v′∈Rp. We choose one e.g.1−v(p) and replace the second, v(p), everywhere it appears.
, in that case they satisfy the same constraints in (E,D)).
Suppose, given a parameter valuation v∈Rp, we have two different syntactic expressions that are equal once valuated
(such as, given p, v(p)=1−v(p) and by Definition 3.2 if it is for v, it is for any v′∈Rp). Then we choose one and replace the second in every constraint where it appears (e.g. replace 1−v(p) by v(p) everywhere).
For a p–PDBM (E,D), we define the set of clocks with the largest fractional part (LFP) as LFPRp(D)={x∈X∣0≤Dx,i is valid for Rp, for all 0≤i≤H}.
As we are able, thanks to the parameter regions, to order our parameter valuations (i. e., whether one is greater or less than another one),
we can define LFP from the constraints defined in the point–p–PDBM.
We will define and apply successively two time-elapsing algorithms:
the first one starts from a point–p–PDBM or an open–p–PDBM respecting condition Definition 3.5 (5a).
We will prove that we obtain an open–p–PDBM respecting condition Definition 3.5 (5b).
The second one starts from an open–p–PDBM respecting condition Definition 3.5 (5b) and will define constraints
defining the possible clocks valuations exactly when any clock of LFP has reached its upper bound 1.
We will prove that we obtain an open–p–PDBM respecting condition Definition 3.5 (5a).
As we will obtain at each iteration of the algorithm an open–p–PDBM respecting either condition Definition 3.5 (5a) or (5b),
this will prove that we have a stable set of open–p–PDBMs. Now we explain our algorithms more precisely.
Clocks belonging to LFP are the first to reach the upper bound 1 by letting time elapse.
Since LFP can contain multiple clocks and they have the same fractional part, we can consider any x∈LFP.
Let (E,D)∈p–PDBM(Rp) and x∈LFPRp(D). To formalize time elapsing until the largest fractional part frac(x) reaches 1,
we define a time elapsing operator that will have two variants depending on the input:
open–p–PDBM (Definition 3.5) satisfying condition (5a) and point–p–PDBM (Definition 3.6)
or open–p–PDBM (Definition 3.5 satisfying condition (5b)).
Given an open–p–PDBM satisfying condition 5a or a point–p–PDBM (E,D) with Ex=k,
TE((E,D)) described in Algorithm 2
and named TE<, defines a new open–p–PDBM satisfying condition 5b by
(1)
setting Dx,0:=(1,<) as x is the first one that will reach k+1;
2. (2)
updating the upper bound of all other clocks i, which has increased: Di,0:=Di,x+(1,<);
3. (3)
updating all lower bounds as they have to leave the border: D0,i:=D0,i+(0,<) (x included).
This gives the range of possible clock valuations beforefrac(x) reaches 1.
Intuitively it represents the transformation from an open line segment or the corner-point region of [AD94] into an open region of [AD94].
Example 4.7**.**
Here is an open–p–PDBM satisfying condition 5a, on the left of the figure below. Formally, it is written:
[TABLE]
Time elapsing before x∈LFP reaches the next integer gives the following open–p–PDBM satisfying condition 5b, on the right of the figure below. Formally, it is written:
[TABLE]
The result of Algorithm 2 is denoted by TE<((E,D)) and leaves E unchanged.
The time elapsing operator also operates the transformation from an open region of [AD94] to the upper open line segment or the corner-point region of [AD94], given in Algorithm 3
as TE=.
Given an open–p–PDBM (E,D) satisfying condition 5b where Ex=k,
TE((E,D)) defines a new open–p–PDBM satisfying condition 5a by
(1)
setting Dx,0:=D0,x:=(0,≤) (intuitively both became (1,≤)) and Ex=k+1 (if Ex≤K+1), as x is now in the upper border;
2. (2)
updating the upper/lower bounds of all other clocks i: Di,0:=Di,x+(1,≤) and D0,i:=Dx,i+(−1,≤);
3. (3)
updating the new difference between fractional parts with all other clocks i, which is the range of values i can currently take (as in the update operator): Dx,i:=D0,i and Di,x:=Di,0.
Example 4.8**.**
Here is an open–p–PDBM satisfying condition 5b, on the left of the figure below. Formally, it is written:
[TABLE]
When x∈LFP reaches k+1, the open–p–PDBM satisfying condition 5a obtained is given on the right of the figure below. Formally, it is written:
[TABLE]
The result of Algorithm 3 is denoted by TE=((E,D)).
Definition 4.9** (time elapsing in a p–PDBM).**
Let Rp be a parameter region and (E,D)∈p–PDBM⊙(Rp)∪p–PDBM■(Rp).
We define (E′,D′)=TE((E,D)) as applying
either TE< if (E,D) respects condition 5a
or (E,D)∈p–PDBM⊙(Rp),
or TE= if (E,D) respects condition 5b.
Lemma 4.10** (stability under time elapsing).**
Let Rp be a parameter region.
Let (E,D)∈p–PDBM(Rp).
Then TE((E,D))∈p–PDBM(Rp).
Proof.
Although we perform some additions such as Dj,i+(1,<), we do not create new expressions that are not in PLT.
In fact, this addition is performed on a negative term (e.g.frac(p)−1), as xi is a clock with the largest fractional part and adding 1 transforms it into another term of PLT. The intuition is similar when performing additions such as Di,j+(−1,≤): as xi is a clock with the largest fractional part, di,j is a positive term. The canonical form is also preserved by the last setting operations of the algorithm, as in the update operator. Therefore TE((E,D)) is a p–PDBM.
See Appendix G for details.
∎
Note that, by Lemma 4.10(E′,D′) is a p–PDBM.
open–p–PDBMs are stable under TE< and TE=, switching the condition they respect (5a, 5b).
Applying TE< on a point–p–PDBM transforms it into an open–p–PDBM.
The following proposition proves that time elapsing behaves as we expect.
Proposition 4.11** (semantics of p–PDBM under TE).**
Let Rp be a parameter region and (E,D)∈p–PDBM(Rp). Let v∈Rp.
There exists w′∈TE((E,v(D))) iff
there exist w∈(E,v(D)) and a delay δ s.t. w′=w+δ.
Proof.
This proof is quite technical. Intuitively, we bound the difference of each upper bound v(di,0) and w(xi) and each lower bound v(d0,i) and w(xi). This allows us to take a delay δ inside these bounds that allows us to reach the next p–PDBM.
See Appendix H for details.
∎
Running example:Figure 3 represents graphically different p–PDBMs obtained after an update u(x)=v(p2)
and u(y)=v(p1) (figure 1). Time elapsing before y∈LFP reaches the next integer gives the open–p–PDBM satisfying condition 5b (figure 2)
[TABLE]
After an update of y to k prior to reaching k+1, the open–p–PDBM satisfying condition 5a obtained is (figure 3)
[TABLE]
Time elapsing before x∈LFP reaches the next integer gives the open–p–PDBM satisfying condition 5b (figure 4)
[TABLE]
When x∈LFP reaches k+1, the open–p–PDBM satisfying condition 5a obtained is (figure 5)
[TABLE]
4.4. Non-parametric guard
From [AD94, Section 4.2] we have that either every clock valuation of a clock region satisfies a guard, or none of them does.
Note that a p–PDBM for Rp is contained into a clock region of Definition 2.3 (see I.1 for more details), therefore
we have that if w∈(E,v(D)) satisfies a non-parametric guard g,
then for all w′∈(E,v(D)) we also have w′ satisfies g.
Let v∈Rp. We define v∈guard∀(g,E,D) iff for all w∈(E,v(D)), w⊨g.
As any two v,v′∈Rp satisfy the same constraints,
the following lemma is straightforward
Lemma 4.12**.**
Let (E,D) be a p–PDBM for Rp and v∈Rp.
Let g be a non-parametric guard.
If v∈guard∀(g,E,D), then for all v′∈Rp, v′∈guard∀(g,E,D).
As for the previous result, using a projection on parameters i. e., eliminating clocks, does not create new constraints on parameters
that are not already in a parameter region Rp.
Indeed, a parametric guard g only adds new constraints of the form x⋈p which gives,
when eliminating clocks in both a p–PDBM (E,D) and a parametric guard,
again a comparison between elements of PLT. Therefore, these new constraints already belong to PLT and we can decide whether the set of clock valuations satisfying
these constraints is non-empty i. e., given v∈Rp, v(g) is satisfied by some clock valuation w∈(E,v(D)).
This is a key point in the overall process of proving the decidability of our R-U2P-PTAs.
Note that there will also be additional constraints involving clocks (with other clocks, constants or parameters), but they will not be relevant as we immediately update all clocks, therefore replacing these constraints with new constraints encoding the clock updates.
Let v∈Rp. We define v∈p\mbox−guard∃(g,E,D) iff there is a w\leavevmode∈(E,v(D)) s.t. w⊨v(g).333Remark that here is why our construction works for EF-emptiness, but cannot be used for, e.g., AF-emptiness (“is there a parameter valuation such that all runs reach a goal location ℓ”): unlike guard∀(g,E,D), not all clock valuations in a p–PDBM (E,v(D)) can satisfy a parametric guard if v∈p\mbox−guard∃(g,E,D).
Again, as any two v,v′∈Rp satisfy the same constraints,
the following lemma is straightforward
Lemma 4.13**.**
Let (E,D) be a p–PDBM for Rp and v∈Rp.
Let g be a parametric guard.
If v∈p\mbox−guard∃(g,E,D), then for all v′∈Rp, v′∈p\mbox−guard∃(g,E,D).
Now that we have defined useful operations on p–PDBMs, we are going, given a parameter region Rp, to construct a finite region automaton in which for any run, there is an equivalent concrete run in the R-U2P-PTA.
5. Parametric region automaton
Let (E,D)∈p–PDBM(Rp), we say (E′,D′)∈Succ((E,D))⇔∃\leavevmodei≥0
s.t. (E′,v(D′))=TEi((E,D)).
In other words, (E′,D′) is obtained after applying TE((E,D)) a finite number of times.
Succ((E,D)) is also called the time successors of (E,D).
In order to finitely simulate an R-U2P-PTA, we create a parametric region automaton.
Definition 5.1** (Parametric region automaton).**
Let Rp be a parameter region.
For an R-U2P-PTA A=(Σ,L,ℓ0,X,P,ζ),
given (E0,D0) the initial p–PDBM where all clocks are [math], the parametric region automatonR(A) over Rp
is the tuple (L′,Σ,L0′,ζ′) where:
(1)
L′=L×p–PDBM(Rp)
2. (2)
L0′=(ℓ0,(E0,D0))
3. (3)
\zeta^{\prime}=\{\big{(}(\ell,(E,D)),a,(\ell^{\prime},(E^{\prime},D^{\prime}))\big{)}\in L^{\prime}\times\Sigma\times L^{\prime}\mid\text{either }\exists e=\langle\ell,g,a,u_{np},\ell^{\prime}\rangle\in\zeta,
g is a non-parametric guard,
∃(E′′,D′′)∈Succ((E,D)), Rp⊆guard∀(g,(E′′,D′′))
and (E′,D′)=update(E′′,D′′,unp) is an open–p–PDBM,
or ∃e=⟨ℓ,g,a,u,ℓ′⟩∈ζ, g is a parametric guard,
∃(E′′,D′′)∈Succ((E,D)), Rp⊆p\mbox−guard∃(g,(E′′,D′′))
and (E′,D′)=update(E′′,D′′,u) is a point–p–PDBM.}
Let Rp be a parameter region, A be an R-U2P-PTA and R(A)=(L′,Σ,L0′,ζ′) its parametric region automaton over Rp.
A run in R(A) is an untimed sequence
σ:(ℓ0,(E0,D0))e0(ℓ1,(E1,D1))e1⋯(ℓi,(Ei,Di))ei(ℓi+1,(Ei+1,Di+1))ei+1⋯
such that for all i we have \big{(}(\ell_{i},(E_{i},D_{i})),a_{i},(\ell_{i+1},(E_{i+1},D_{i+1}))\big{)}\in\zeta^{\prime},
which we also write (ℓi,(Ei,Di))⟶ei(ℓi+1,(Ei+1,Di+1)).
Note that we label our transitions with the edges of the R-U2P-PTA.
6. Decidability of EF-emptiness and synthesis
Using our construction of the parametric region automaton R(A) for a given R-U2P-PTA A, we state the next proposition.
Proposition 6.1**.**
Let Rp be a parameter region. Let A be an R-U2P-PTA and R(A) its parametric region automaton over Rp.
There is a run σ:(ℓ0,(E0,D0))⟶e0(ℓ1,(E1,D1))⟶e1⋯(ℓf−1,(Ef−1,Df−1))⟶ef−1(ℓf,(Ef,Df))
in R(A) iff for all v∈Rp there is a run ρ:(ℓ0,w0)⟶e0(ℓ1,w1)⟶e1⋯(ℓf−1,wf−1)⟶ef−1(ℓf,wf)
in v(A)
s.t. for all 0≤i≤f, wi∈(Ei,v(Di)).
Proof.
We prove this result by induction on the length of the run. It is quite direct as we construct runs without parametric guards.
See Appendix K for details.
∎
Example 6.2**.**
Consider Figure 4.
Let A be an R-U2P-PTA, Rp a parameter region and v∈Rp.
Suppose there is a run in A, starting from the initial location (ℓ0,0) reaching a goal location (ℓf,wf).
Along this run, all edges are non-parametric transitions but \hbox{\pagecolor{yellow}e_{i}}=\langle\ell_{i},g,a_{i},u,\ell_{i+1}\rangle.
That is, u is a total parametric update,
and g is a possibly parametric guard.
The first part of this run, from (ℓ0,0) to (ℓi,wi) starts from (l0,(E0,D0)) where (E0,D0) is the p–PDBM of the initial clock region {0},
and ends in (ℓi,(Ei,Di)). The second part of this run, from (ℓi+1,wi+1) to (ℓf,wf)
starts from (li+1,(Ei+1,Di+1)) where (Ei+1,Di+1) is a point–p–PDBM,
and can reach (ℓf,(Ef,Df)) and further ends in (ℓs,(Es,Ds)).
These runs contain only non-parametric transitions, and as there is an edge in A from (ℓi,wi) to (ℓi+1,wi+1),
we have to bisimulate this run in R(A)
containing the parametric transition ei, where update((Ei,Di),u) gives (Ei+1,Di+1).
From Proposition 6.1, we deduce that if there is a run reaching a goal location in an instantiated R-U2P-PTA,
then for another parameter valuation in the same parameter region there is a run in the instantiated R-U2P-PTA with the same locations and transitions (but possibly different delays), reaching the same location.
Theorem 6.3**.**
Let A be an R-U2P-PTA.
Let Rp be a parameter region and v∈Rp.
If there is a run ρ=(ℓ0,w0)⟶e0⋯⟶ei−1(ℓi,wi) in v(A),
then for all v′∈Rp
there is a run ρ′=(ℓ0,w0′)⟶e0⋯⟶ei−1(ℓi,wi′) in v′(A)
with for all 0≤j≤i, there is (Ej,Dj)∈p–PDBM(Rp) s.t. wj∈(Ej,v(Dj)) and wj′∈(Ej,v′(Dj)).
Proof.
Let v∈Rp and ρ a run of v(A) reaching (ℓi,wi).
From Proposition 6.1, there is a run σ in R(A)
s.t. each clock valuation at a location j in ρ is in the p–PDBM (Ej,Dj) at the same location in σ.
Still from Proposition 6.1, for all v′∈Rp there is a run ρ′ in v′(A) reaching (ℓi,wi′)
s.t. each clock valuation at a location j in ρ′ is in the p–PDBM (Ej,Dj) at the same location in σ (note that possibly v=v′).
Therefore, we have
for all 0≤j≤i, there is (Ej,Dj)∈p–PDBM(Rp) s.t. wj∈(Ej,v(Dj)) and wj′∈(Ej,v′(Dj))
and the expected result.
∎
Note that there is a finite number of p–PDBMs for each parameter region Rp.
Let (E,D)∈p–PDBM(Rp) and consider PLT: D is an (H+1)2 matrix made of pairs (d,◃)
where d∈PLT and ◃∈{≤,<}.
Therefore the number of possible D is bounded by
[TABLE]
Moreover the number of E is unbounded, but only a finite subset of all values needs to be explored, i. e., those smaller than K+1: indeed, following classical works on timed automata [AD94, BDFP04], (integer) values exceeding the largest constant used in the guards or the parameter bounds are equivalent.
To test EF-emptiness given an R-U2P-PTA A and a goal location ℓ, we first enumerate all parameter regions (which are a finite number),
and apply for each Rp the following process:
we pick v∈Rp (e.g. using a linear programming algorithm [Kar84]).
Then, we consider v(A) which is an updatable timed automaton and test the reachability of ℓ in v(A) [BDFP04].
Then EF-emptiness is false if and only if there is v and a run in v(A) reaching ℓ.
Theorem 6.4**.**
The EF-emptiness problem is PSPACE-complete for bounded R-U2P-PTAs.
Proof.
Since a TA is a special case of R-U2P-PTA we have the PSPACE-hardness [AD94].
Now, let G be a set of goal locations of A.
We build a non-deterministic Turing machine that:
(1)
takes A, G and K as input;
2. (2)
non-deterministically “guesses” a parameter region Rp;
3. (3)
takes v∈Rp and writes it to the tape;
4. (4)
overwrites on the tape each parameter p by v(p)
giving the updatable TA v(A);
5. (5)
solves reachability in v(A) for G;
6. (6)
accepts iff the result of the previous step is “yes”.
The machine accepts iff there is an integer valuation v bounded by K
and a run in v(A) reaching a location ℓ∈G.
The size of the input is ∣A∣+∣G∣+∣K∣, using ∣.∣ to denote the size in bits
of the different objects.
Moreover, the number of parameter regions is bounded (M is the number of parameters in A)
by \big{(}M!\times 2^{M}\times\prod_{p\in\mathbb{P}}(2M+2)\big{)}\times\big{(}2\times{(2+M(3\frac{M-1}{2}+4))}^{3}\big{)}
since they are constructed as the clock regions of [AD94], the second part being the maximal number of constraints in a parameter region.
Picking v at step (3) uses a PSPACE linear programming algorithm (e.g. [Kar84]).
Storing the valuation at step (4) uses at most M×∣K∣
additional bits, which is polynomial w.r.t. the size of the input.
Step (5) also needs polynomial space from [BDFP04].
So globally this non-deterministic machine runs in polynomial space.
Finally, by Savitch’s theorem we have PSPACE=NPSPACE [Sav70], and the expected result.
∎
Given a goal location ℓ and a bounded R-U2P-PTA A, we can exactly synthesize the parameter valuations v s.t. there is a run in v(A) reaching ℓ by enumerating each parameter region (of which there is a finite number) and test if ℓ is reachable for one of its parameter valuations.
The result of the synthesis is the union of the parameter regions for which one valuation (and, from our results, all valuations in that region) indeed reaches the goal location in the instantiated TA.
Corollary 6.5**.**
Given a bounded R-U2P-PTA A and a goal location ℓ we can effectively compute the set of parameter valuations v s.t. there is a run in v(A) reaching ℓ.
Proof.
The procedure to obtain synthesis is as follows.
We assume an R-U2P-PTA A and a goal location ℓ.
(1)
enumerate all parameter regions (of which there is a finite number);
2. (2)
for each Rp, pick a parameter valuation we pick v∈Rp (e.g. using a linear programming algorithm [Kar84]);
3. (3)
test the reachability of ℓ in the updatable timed automaton v(A), which is decidable [BDFP04];
4. (4)
if ℓ is reachable in v(A), add Rp to the list of synthesized regions.
We finally return the union of all regions Rp that reach ℓ.
The correctness immediately comes from Theorems 6.3 and 6.4.
∎
Remark 6**.**
By bounding parameter valuations in guards but not those used in updates, we still have a finite number of parameter regions.
Indeed, an integer vector E with components Ex greater than ⌊K⌋+1 is equivalent to an
integer vector E′ with Ex′=Ex if Ex<⌊K⌋+1 and Ex′=⌊K⌋+1
if Ex≥⌊K⌋+1.
Moreover for all p, we have to replace each parameter valuation v
used in an update by v(p)=v′(p) if v(p)≤K
and v′(p)=K+1 if v(p)>K.
7. Parametric updates and stopwatches
In this section, we consider clocks in R-U2P-PTAs as stopwatches [CL00]: stopwatches can be stopped and started again on transitions. In the general case, stopwatches bring back undecidability in timed automata [BBR06]. Similarly to the “initialization” constraint of [HKPV98] we allow stopwatches to be stopped and started again only on specific transitions.
We define A an R-U2P-PTA with stopwatches instead of clocks. We will prove by using our p–PDBMs structure that the EF-emptiness problem is decidable under the condition that stopwatches can be stopped at each full update function, and started again at the next full update function.
Such a condition, as in Definition 3.1 is critical: allowing a partial (or empty) update of clocks ruins the efforts made to keep the set of p–PDBMs stable and allows accumulation of parameters, leading to the undecidability of the EF-emptiness problem.
Definition 1**.**
A stopwatch reset update-to-parameter PTA (S-R-U2P-PTAs)
A is a tuple A=(Σ,L,ℓ0,X,P,ζ,stop), where:
(1)
Σ is a finite set of actions,
2. (2)
L is a finite set of locations,
3. (3)
ℓ0∈L is the initial location,
4. (4)
X is a finite set of stopwatches,
5. (5)
P is a finite set of parameters,
6. (6)
ζ is a finite set of edges e=⟨ℓ,g,a,u,ℓ′⟩
where
ℓ,ℓ′∈L are the source and target locations, g is a parametric guard, a∈Σ and
u:X⇀N∪P is a parametric update function.
7. (7)
stop:L→2X assigns to each location a set of stopwatches that are stopped at this location.
Moreover, u is a total function whenever:
(1)
g is a parametric guard,
2. (2)
u(x)∈P for some x∈X, or
3. (3)
stop(ℓ)=stop(ℓ′) for e=⟨ℓ,g,a,u,ℓ′⟩.
The semantics is defined in a straightforward manner.
The update and time elapsing operators are defined in a similar manner as for R-U2P-PTA.
Theorem 2**.**
The EF-emptiness problem is PSPACE-complete for bounded S-R-U2P-PTAs.
Proof 7.1**.**
To prove this result, we first remove stopped stopwatches from p–PDBMs, and show that we can still reason as in Theorem 6.4.
Note that after a full update, stopped stopwatches satisfy constraints defined by a p–PDBM⊙(Rp).
These constraints, defined in Definition 3.6, are
For all i, (−1,<)≤D0,i≤(0,≤) and (0,≤)≤Di,0≤(1,<) are valid for Rp,
2. (2)
For all i,j,k, Di,j≤Di,k+Dk,j is valid for Rp (canonical form).
Let x be a stopped stopwatch, we remove the column and the row corresponding to x in the point–p–PDBM, and we put these constraints aside.
(1) is still satisfied for stopwatches different from x as nothing changed.
As both the column and the row are removed for x, constraints of the form Dx,j≤Dx,k+Dk,j and Di,x≤Di,k+Dk,x are removed as well. With the same argument, constraints of the form Di,j≤Di,x+Dx,j are also removed. Only constraints of the form Di,j≤Di,k+Dk,j where i,j,k are different from x remain, and therefore (2) is still satisfied.
We apply the same reasoning for all stopped stopwatches.
After this modification, we still have a point–p–PDBM.
Lemmas Lemmas 4.3, 4.4 and 4.10 and Proposition 4.11 are still applicable in this context.
Remains the comparison with non parametric guards Lemma 4.12 and parametric guards Lemma 4.13.
As stated, constraints on stopped stopwatches are put aside, call these constraints Cstop; as these constraints are the result of a full update it means there is one clock valuation that satisfies these constraints (it is not an interval, or a set of clock valuations). This argument is crucial in the following: we do not need to be able to bound difference of a stopped stopwatch and a running stopwatch (i. e., Dx,y in the p–PDBM for some stopped x and running y, or conversely) to compare separately the p–PDBM with a guard, parametric or not.
First, we compare the p–PDBM with a possibly parametric guard. Let Rp a parameter region and v∈Rp.
Separately we compare the guard g with the constraints on stopped stopwatch Cstop:
•
If g is a non parametric guard, let x be a stopped stopwatch appearing in g.
–
If x has been updated to a constant, we can test whether g is satisfied by testing the conjunction of the constraints v(Cstop) projected on x and g projected on x.
–
If x has been updated to a parameter, we can test the same conjunction as the order between parameters is defined in Rp.
•
If g is a parametric guard, let x be a stopped stopwatch appearing in g.
In both cases (x* updated to a parameter or a constant) we can test whether v(g) is satisfied by testing the conjunction of the constraints v(Cstop) projected on x and v(g) projected on x as the order between parameters and constants is defined in Rp.*
Therefore, Lemma 4.12 and parametric guards Lemma 4.13 are still applicable in this context.
With our modified structure of p–PDBM with stopwatches, the core operators for clock updates, time elapsing and comparison with guards are still applicable. We obtain our result by a similar reasoning as Theorem 6.4.
Similarly to Corollary 6.5, we obtain the following result:
Corollary 3**.**
Given a bounded S-R-U2P-PTA A and a goal location ℓ we can effectively compute the set of parameter valuations v s.t. there is a run in v(A) reaching ℓ.
8. Case study
We implemented EFsynth for R-U2P-PTAs in IMITATOR, a parametric model checker for (extensions of) PTAs [AFKS12].
Our class is the first for which synthesis is possible over bounded rational parameters.
We believe our formalism is useful to model several categories of case studies, notably distributed systems with a periodic (global) behavior for which the period is unknown: this can be encoded using a parametric guard while resetting all clocks—possibly to other parameters.
Consider the R-U2P-PTA in Figure 1 with six locations, three clocks compared to parameters ({\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x}, {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}y}, {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}t}), one constant (max) and six parameters ({\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p}, {\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}v}, {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}pv_{1}}, {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}pv_{2}}).
We consider the case of a network of peers exchanging transactions grouped by blocks, e.g. a blockchain, using the Proof-of-Work as a mean to validate new blocks to add.
In this simplified example, we consider a set of two peers (represented by {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x}, {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}y}) which have different computation power (represented by {\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}}).
Peers write new transactions on the current block ({\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{newTx}}). If it is full ({\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}t}={\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p}), both peers try to add a new block ({\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{newBlock}}) to write the transaction on it. We update {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x} to {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{1}}, {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}y} to {\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}t} to [math] as the peers have a different computation power, and they start “mining” the block (find a solution to a computation problem).
Either {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x} or {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}y} will eventually offer a solution to the problem ({\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{blockSolution_{x}}} if {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x}=max or {\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{blockSolution_{y}}} if {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}y}=max). If {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}y} offers a solution, {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x} will check whether the solution is correct: {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x} is updated to {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}pv_{1}} to represent its speed to verify an offer. {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x} can refuse the offer if the verification is too long ({\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{fakeBlock}} if {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x}>{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}v}) therefore the mining step restarts. {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x} can approve the offer ({\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{okBlock}} if {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x}\leq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}v}), {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}y} is rewarded and the block is added to the blockchain ({\color[rgb]{0.50,0.70,0.30}\definecolor[named]{pgfstrokecolor}{rgb}{0.50,0.70,0.30}\mathrm{addBlock}}).
We are interested in a malicious peer {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x} that wants to avoid {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}y} being rewarded for every new block. Therefore {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x} asks: “what are the possible computation power configurations and verification speed so that {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}y} can be rewarded” (EF(rewardy)-synthesis), considered as a bug state in the automaton.
We run this R-U2P-PTA using IMITATOR [AFKS12]444Experiments were conducted with IMITATOR 2.10.4 “Butter Jellyfish” on a 2.4 GHz Intel Core i5 processor with 2 GiB memory. Computation time is less than 1 second.
Sources, binaries, models and results are available at imitator.fr/static/FORTE19/.
We set max=30 units of time and also the upper bound of {\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p} and 1\geq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}v}>0 unit of time. IMITATOR computes a disjunction of constraints so that rewardy is unreachable: we keep two relevant ones;
(1)
{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{1}}\geq{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}}:
{\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x} has strictly more computation power than {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}y} in which case {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x} always offers a block solution, or has the same computation power than {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}y} in which case the systems blocks. {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x} should invest heavily into hardware to keep its computation power high;
2. (2)
{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}pv_{1}}>{\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}v}:
the malicious peer {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x} is always faster to verify the solution offered by {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}y} and refuses it. The blockchain is probably compromised.
Using a parameter valuation respecting one of the previous constraints guarantees that {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}y} is never rewarded.
Remark 1**.**
Even if we have to update all clocks whenever a parameter is met in a guard or in an update, the possibility to update clocks to unknown parameter offers an appreciable freedom in the range of system that can be modeled with R-U2P-PTA. Especially as our parameters can take unbounded rational values in updates and bounded rational values in guards.
However, such a restriction restricts the behavior that can be modeled. Consider the PTA of Figure 5 for which the set of possible parameter valuations s.t. ℓ3 is reachable is
\{v\mid v({\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{3}})=nv({\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{1}})+v({\color[rgb]{1,0.6,0.0}\definecolor[named]{pgfstrokecolor}{rgb}{1,0.6,0.0}p_{2}}) for some n∈N}.
This set cannot be computed from a R-U2P-PTA as in the loop transition over ℓ2 both clocks {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}x} and {\color[rgb]{0.4,0.4,1}\definecolor[named]{pgfstrokecolor}{rgb}{0.4,0.4,1}y} must be updated.
9. Conclusion and perspectives
Our class of R-U2P-PTAs is one of the few subclasses of PTAs (actually even extended with parametric updates) to enjoy decidability of EF-emptiness.
In addition, R-U2P-PTAs are the first “subclass” of PTAs to allow exact synthesis of bounded rational-valued parameters.
In terms of future work, beyond reachability emptiness, we aim at studying unavoidability-emptiness and language preservation emptiness (“given a reference parameter valuation, does there exist another parameter valuation with the same untimed language” [ALM20]), as well as their synthesis.
We would also study the possibility to stop and start stopwatches without full updates; it would change the p–PDBM structure by creating new clock constraints, but seems promising and the reachability emptiness problem might be decidable as well.
Time bounded reachability is also interesting to study:
given an R-U2P-PTA A, a parameter max and a goal location ℓ, is there a parameter valuation v and a run in v(A) reaching ℓ in less than v(max) time?
Finally, we would like to investigate whether our parametric updates can be applied to decidable hybrid extensions of TAs [HKPV98, BDG*+*13]. For example, we shall find a subclass of hybrid automata that can be reduced to R-U2P-PTA as done with initialized rectangular hybrid automata and TAs in [HKPV98].
Lemma 3.4** (recalled).**
*Let d1,d2,d3,d4∈PLT. Let Rp be a parameter region.
If (d1,◃1)≤(d2,◃2) and (d3,◃3)≤(d4,◃4) are valid for Rp
then (d1,◃1)+(d3,◃3)≤(d2,◃2)+(d4,◃4) is valid for Rp.
*
Proof A.1**.**
Four cases show up: for all v∈Rp,
•
v(d1)<v(d2)* and v(d3)<v(d4), then clearly v(d1)+v(d3)<v(d2)+v(d4) and we have our result from Definition 3.3 (2a).*
•
v(d1)<v(d2)* and v(d3)≤v(d4), then v(d1)+v(d3)<v(d2)+v(d4) and we have our result from Definition 3.3 (2a).*
•
v(d1)≤v(d2)* and v(d3)<v(d4), then v(d1)+v(d3)<v(d2)+v(d4) and we have our result from Definition 3.3 (2a).*
•
v(d1)≤v(d2)* and v(d3)≤v(d4), then v(d1)+v(d3)≤v(d2)+v(d4) and*
(1)
if ◃1=◃2 and ◃3=◃4 then ◃1⊕◃3=◃2⊕◃4 and we have our result from Definition 3.3 (2b).
2. (2)
if ◃1=◃2 and ◃3=<, ◃4=≤ then ◃1⊕◃3=< and ◃2⊕◃4 is either < or ≤ and we have our result from Definition 3.3 (2b).
3. (3)
if ◃1=<, ◃2=≤ and ◃3=◃4 then ◃1⊕◃3=< and ◃2⊕◃4 is either < or ≤ and we have our result from Definition 3.3 (2b).
4. (4)
if ◃1=◃3=< and ◃2=◃4=≤ then ◃1⊕◃3=< and ◃2⊕◃4=≤ and we have our result from Definition 3.3 (2b).
From Definition 3.3 (2a, 2b) we have that (d1,◃1)+(d3,◃3)≤(d2,◃2)+(d4,◃4) is valid for Rp.
Lemma 3.8** (recalled).**
*
Let Rp be a parameter region and (E,D) be a p–PDBM for Rp.
For all clocks i,j, Di,j≤Di,j+Dj,j and Di,j≤Di,i+Di,j are valid for Rp.
*
Proof C.1**.**
Let Rp be a parameter region and (E,D) be a p–PDBM for Rp.
Let Di,j=(di,j,◃ij) with di,j∈PLT.
By Definition 3.5 and Definition 3.6 for all clock i, Di,i=(0,≤).
We have Dj,i+Di,i=(dj,i+0,◃ij⊕≤)=Dj,i.
Moreover from Definition 3.3 (2b) Di,j≤Di,j is valid for Rp.
Hence Di,j≤Di,i+Di,j is valid for Rp.
The same way we prove Di,j≤Di,j+Dj,j is valid for Rp.
Lemma 4.3** (recalled).**
*
Let Rp be a parameter region and*
(E,D)∈p–PDBM(Rp).
*Let unp be a non-parametric update.
Then update((E,D),unp)∈p–PDBM■(Rp).
*
Proof D.1**.**
The case of a trivial non-parametric update i. e., that updates no clock, is straightforward.
We split this proof in two parts: the first one treats the case of point–p–PDBMs and the second one of open–p–PDBMs.
First we show that applying an update on any point–p–PDBM transforms it into an open–p–PDBM.
Claim 1** (p–PDBM⊙(Rp) becomes p–PDBM■(Rp) after update).**
Let Rp
be a parameter region and (E,D)∈p–PDBM⊙(Rp).
Let unp be a non-parametric update.
Then update((E,D),unp)∈p–PDBM■(Rp).
Proof D.2**.**
Let Rp be a parameter region and (E,D)∈p–PDBM⊙(Rp). Consider (E′,D′)=update((E,D),unp).
After applying Algorithm 1, for all clock xi of (E,D) where unp is defined,
Ei′=unp(xi); moreover for all clock j, Di,j′=D0,j and Dj,i′=Dj,0.
First note that if xi,xj have been updated, Di,j′=Dj,i′=D0,j′=Dj,0′=D0,i′=Di,0′=(0,≤)=D0,0.
For all clocks i,j,k, the following inequalities are valid for Rp:
(1)
(a)
if xi is updated: Di,0′=(0,≤)=D0,i′ and therefore trivially it holds that −1≤D0,i′≤0 and 0≤Di,0′≤1 are valid for Rp;
2. (b)
if xi is not updated: Di,0′=Di,0 and therefore −1≤D0,i′≤0 and 0≤Di,0′≤1 are valid for Rp because these constraints were already satisfied in (E,D).
2. (2)
For all xi,xj, if neither xi nor xj is updated, Di,j and Dj,i are not modified so condition Definition 3.5 (2) still holds.
If either xi is updated, as Di,j′=D0,j and Dj,i′=Dj,0 condition Definition 3.5 (2) still holds as it holds for D0,j and Dj,0 and we apply the same reasoning if xj is updated.
If both xi,xj are updated, condition Definition 3.5 (2) trivially holds.
3. (3)
For all xi, if it is updated then D0,i′=Di,0′=(0,≤), hence d0,i=−di,0=0 and ◃0i=◃i0=≤; condition Definition 3.5 (3) holds.
For all xi,xj, if neither xi nor xj is updated, Di,j′=Di,j and Dj,i′=Dj,i so condition Definition 3.5 (3) holds as it holds for Di,j and Dj,i.
If either xi is updated, as Di,j′=D0,j and Dj,i′=Dj,0, condition Definition 3.5 (3) holds as it holds for D0,j and Dj,0.
We treat the case where xj is updated similarly.
If both xi,xj are updated, condition Definition 3.5 (3) trivially holds.
4. (4)
Canonical form is preserved:
(a)
if xi,xj,xk are not updated:
since no clock is updated we have Di,j′=Di,j, Dj,k′=Dj,k and Di,k′=Di,k
since (E,D)∈p–PDBM⊙(Rp) from Definition 3.6 (2), we know that Di,k≤Di,j+Dj,k is valid for Rp;
therefore it remains valid.
2. (b)
if xk is updated and xi,xj are not updated: Di,j′=Di,j
and Dj,k′=Dj,0, Di,k′=Di,0 because xk is updated.
Since (E,D)∈p–PDBM⊙(Rp) from Definition 3.6 (2), we know that Di,0≤Di,j+Dj,0 is valid for Rp;
therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
3. (c)
if xj is updated and xi,xk are not updated:
then Di,k′=Di,k because neither xi nor xk are updated;
since xk is updated we have Dj,k′=D0,k and Di,j′=Di,0;
since (E,D)∈p–PDBM⊙(Rp) from Definition 3.6 (2), we know that Di,k≤Di,0+D0,k is valid for Rp;
therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
4. (d)
if xj,xk are updated and xi is not updated:
then Di,k′=Di,0 because xk is updated;
since xj is updated we have Di,j′=Di,0 and Dj,k′=D0,0;
since (E,D)∈p–PDBM⊙(Rp) from Definition 3.6 (2) and Lemma 3.8, we know that Di,0≤Di,0+D0,0 is valid for Rp;
therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
5. (e)
if xi is updated and xj,xk are not updated:
then Di,k′=D0,k, Di,j′=D0,j because xi is updated;
since xj,xk are not updated, we have Dj,k′=Dj,k;
since (E,D)∈p–PDBM⊙(Rp) from Definition 3.6 (2), we know that D0,k≤D0,j+Dj,k is valid for Rp;
therefore Di,k′≤Di,j′+Dj,k′ is valid for Rp.
6. (f)
if xi,xk are updated and xj is not updated: we have Di,k′=(0,≤)=D0,0, Di,j′=D0,j and Dj,k′=Dj,0 because xi,xk are updated.
Since (E,D)∈p–PDBM⊙(Rp) from Definition 3.6 (2), we know that D0,0≤D0,j+Dj,0 is valid for Rp;
therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
7. (g)
if xi,xj are updated and xk is not updated: we have Di,k′=D0,k, Di,j′=(0<≤)=D0,0 and Dj,k′=D0,k because xi,xj are updated.
Since (E,D)∈p–PDBM⊙(Rp) from Definition 3.6 (2) and Lemma 3.8, we know that D0,k≤D0,0+D0,k is valid for Rp;
therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
8. (h)
if xi,xj,xk are updated: we have Di,k′=D0,0, Di,j′=D0,0 and Dj,k′=D0,0 because xi,xj,xk are updated.
Since (E,D)∈p–PDBM⊙(Rp) from Definition 3.6 (2) and Lemma 3.8, we know that D0,0≤D0,0+D0,0 is valid for Rp;
therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
5. (5)
there is at least one clock xs.t.Dx,0′=D0,x′=(0,≤).
Therefore, (E′,D′)∈p–PDBM■(Rp).
Now we show that applying an update on any open–p–PDBM transforms it into an open–p–PDBM respecting Definition 3.5 (2).
Claim 2** (stability of p–PDBM■(Rp) under update).**
Let Rp be a parameter region and (E,D)∈p–PDBM■(Rp).
Let unp be a non-parametric update.
Then update((E,D),unp)∈p–PDBM■(Rp).
The remaining cases to treat are the cases of Definition 3.5 (2).
If i,j are different from [math], and
(1)
if i,j are not updated then Di,j′=Di,j and since it is the case in (E,D), condition Definition 3.5 (2) holds.
2. (2)
if j is updated and i is not updated then Di,j′=Di,0 and Dj,i′=D0,i
and as condition Definition 3.6 (1) holds for Di,0 and D0,i in (E,D),
condition Definition 3.5 (2) holds in (E′,D′).
3. (3)
if i is updated and j is not updated then Di,j′=D0,j and Dj,i′=Dj,0
and as condition Definition 3.6 (1) holds for Dj,0 and D0,j in (E,D),
condition Definition 3.5 (2) holds in (E′,D′).
4. (4)
if i,j are updated then trivially Di,j′=Dj,i′=(0,≤) and condition Definition 3.5 (2) holds.
Lemma 4.4** (recalled).**
*Let Rp be a parameter region and (E,D)∈p–PDBM(Rp). Let v∈Rp.
Let unp be a non-parametric update.
For all w, [w]unp∈update((E,v(D)),unp) iff w∈(E,v(D)).
*
Proof E.1**.**
We first treat the case of open–p–PDBMs, the case of point–p–PDBMs will be handled similarly at the end.
We also prove this lemma for a singleton update (only one clock, say xi) since updating several clocks can be done by applying several singleton updates in a [math] delay.
⟹** for open–p–PDBMs****
Let Rp be a parameter region and (E,D)∈p–PDBM■(Rp).
Let v∈Rp.
Let unp be a non-parametric update which updates xi to an integer n and lets the value of other clocks unchanged.
Consider (E′,D′)=update((E,v(D)),unp)
and suppose w′∈(E′,D′).
We want to construct a valuation
w∈(E,v(D)) s.t. w′=unp(w).
Let w be a clock valuation s.t.
for all clock xj where i=j, w(xj)=w′(xj).
That means that for all j=i,
[TABLE]
hold from Definition 4.2 since it is the case in (E′,D′) and these values are left untouched by the update.
Moreover for all j=i, k=i,
[TABLE]
again hold from Definition 4.2 since it is the case in (E′,D′) and these values are left untouched by the update.
We want a valuation for w(xi) s.t.
[TABLE]
hold, and for all j=i, k=i,
[TABLE]
hold.
Let us prove that such a valuation w exists.
We set ⌊w(xi)⌋=Ei.
The following lemma proves transitivity of constraints on clocks with respect to constraints in a p–PDBM.
Lemma 1**.**
Let Rp be a parameter region and (E,D)∈p–PDBM(Rp). Let v∈Rp.
Let w∈(E,v(D)).
For all clocks i,j,k,
frac(w(xj))−frac(w(xk))(◃ji⊕◃ik)v(dj,i)+v(di,k).
Proof E.2**.**
Let Rp be a parameter region and (E,D)∈p–PDBM(Rp). Let v∈Rp.
Let w∈(E,v(D)).
Since (E,D)∈p–PDBM(Rp), for all i,j,k we have from Definition 3.5 (4),
[TABLE]
is valid for Rp hence since v∈Rp, we have v(Dj,k)≤v(Dj,i)+v(Di,k).
Precisely
that is (v(dj,k),◃jk)≤(v(dj,i),◃ji)+(v(di,k),◃ik) i. e.,
[TABLE]
For all clocks j,k satisfying constraints of (E,D),
[TABLE]
Then for all i,j,k, either:
•
from Definition 3.3 (2a):
v(dj,k)<v(dj,i)+v(di,k) and then, regardless of ◃jk and ◃ji⊕◃ik
we have frac(w(xj))−frac(w(xk))(◃ji⊕◃ik)v(dj,i)+v(di,k),
or
•
from Definition 3.3 (2b):
–
v(dj,k)≤v(dj,i)+v(di,k)* and ◃jk=<, ◃ji⊕◃ik=≤ and then
we have*
[TABLE]
or
–
v(dj,k)≤v(dj,i)+v(di,k)* and ◃jk=◃ji⊕◃ik and then
we have*
holds. Note that ◃ji⊕◃ik is either ≤ or <.
Note the following trick is inspired by [HRSV02, Proof of Lemma 3.5] and [HRSV02, Proof of Lemma 3.13].
Hence
[TABLE]
is a non empty set.
That means that choosing a frac(w(xi)) with respect to constraints (1), recall that they are
[TABLE]
is equivalent to choose a frac(w(xi)) s.t.
[TABLE]
which is a nonempty set from formula (2).
Finally we choose a frac(w(xi))∈I, then w∈(E,v(D))
and it completes the proof.
⟸** for open–p–PDBMs****
Let Rp be a parameter region and (E,D)∈p–PDBM■(Rp).
Let v∈Rp.
Let unp be a non-parametric update which updates xi to an integer n and lets the value of other clocks unchanged.
Consider (E′,D′)=update((E,v(D)),unp).
Now suppose w∈(E,v(D)) and let w′=[w]unp.
•
for xi, since unp is defined,
w′(xi)=unp(xi)=Exi′ (i. e.,frac(w′(xi))=0) by applying update as defined in Definition 4.2.
By applying update as defined in Definition 4.2, Di,0′=D0,i′=(0,≤), hence
[TABLE]
hold from Definition 4.2 and Claim 1.
Moreover we know that for all j=i
[TABLE]
holds from Definition 4.2, and we also know that
[TABLE]
since frac(w′(xi))=0.
Hence, combining (3) and (4), clearly
since
[TABLE]
hold in (E′,D′),
[TABLE]
hold.
•
for any two clocks xj,xk where unp is not defined, w(xj)=w′(xj) and w(xk)=w′(xk). Hence
[TABLE]
and
[TABLE]
hold from Definition 4.2 and Claim 1 since bounds remain unchanged.
Then w′∈update((E,v(D)),unp).
This concludes the case (E,D)∈p–PDBM■(Rp).
Let us now treat the case (E,D)∈p–PDBM⊙(Rp).
⟹** for point–p–PDBMs****
Let Rp be a parameter region and (E,D)∈p–PDBM⊙(Rp).
Let v∈Rp.
Let unp be a non-parametric update which updates xi to an integer n and lets the value of other clocks unchanged.
Consider (E′,D′)=update((E,v(D)),unp)
and suppose w′∈(E′,D′).
We want to construct a valuation
[TABLE]
Let w be a clock valuation s.t.
for all clock xj where j=i, w(xj)=w′(xj).
That means for all j=i,
[TABLE]
hold from Definition 4.2 since it is the case in (E′,D′) and bounds remain unchanged i. e., D0,j=D0,j′ and Dj,0=Dj,0′.
Moreover for all k=i and k=j,
[TABLE]
also hold from Definition 4.2 since it is the case in (E′,D′) and bounds remain unchanged i. e., Dk,j=Dk,j′ and Dj,k=Dj,k′.
Recall that (E,D) contains only one clock valuation for each parameter valuation v∈Rp.
Let frac(w(xi))=v(di,0) (or equivalently frac(w(xi))=−v(d0,i)
since by Definition 3.6 we have (di,0,◃i0)=(−d0,i,◃0i)).
Then, as it is the case in (E,D),
[TABLE]
hold, and for all j=i, k=i,
[TABLE]
hold, which completes the proof, as w∈(E,v(D)) and w′=unp(w).
⟸** for point–p–PDBMs****
This case is straightforward and similar to the case (⇐) above of open–p–PDBMs.
Lemma 4.6** (recalled).**
*
Let Rp be a parameter region and (E,D)∈p–PDBM(Rp).
There is at least one clock x s.t. for all 0≤i≤H, (0,≤)≤Dx,i is valid for Rp.
*
Proof F.1**.**
Reductio ad absurdum: Let Rp be a parameter region and (E,D)∈p–PDBM■(Rp) with at least 2 clocks i,j.
Suppose for all clock xi there is another clock xj s.t. Di,j<0 is valid for Rp.
Let v∈Rp. Then v(Di,j)<0.
•
Suppose for xj, xi is the clock s.t.Dj,i<0 is valid for Rp.
Then v(Dj,i)<0.
We have v(Di,j)+v(Dj,i)<0 holds, therefore 0≤v(Di,j)+v(Dj,i) does not hold, and hence 0≤Di,j+Dj,i is not valid for Rp.
Then (E,D) does not respect Lemma 3.7 and violates condition (4) of Definition 3.5. So (E,D)∈p–PDBM■(Rp).
•
Suppose for xj, a third clock xk is the clock s.t.Dj,k<0 is valid for Rp. Then v(Dj,k)<0.
Suppose we have only three clocks. Then for xk, either xi or xj is the clock s.t.Dk,i<0 is valid for Rp.
–
Assume this is xi.
Then v(Dk,i)<0.
We have v(Dk,i)+v(Di,j)<0 and v(Dk,j)≤v(Dk,i)+v(Di,j) by Definition 3.5 (4).
Follows that v(Dk,j)+v(Dj,k)<0 and 0≤Dk,j+Dj,k is not valid for Rp.
Then (E,D) does not respect Lemma 3.7 and violates condition (4) of Definition 3.5. So (E,D)∈p–PDBM■(Rp).
–
Assume this is xj.
This case is similar (and simpler).
We apply the same reasoning for more than 3 clocks.
Now suppose (E,D)∈p–PDBM⊙(Rp). We apply the same reasoning, replacing the argument of condition (4) of Definition 3.5
by the fact from Definition 3.6 that D is antisymmetric.
Claim 1** (modification of an open–p–PDBM respecting condition (5a) under TE<).**
Let Rp be a parameter region and (E,D)∈p–PDBM■(Rp) respecting condition 5a,
then TE<((E,D))∈p–PDBM■(Rp) respecting condition 5b.
Proof G.2**.**
Suppose (E,D)∈p–PDBM■(Rp) respects condition (5a) of Definition 3.5,
i. e., we have at least an x s.t. Dx,0=D0,x=(0,≤).
Since, in Rp, we know which parameters have the largest fractional part,
we can determine LFPRp(D) from Lemma 4.6.
If more than one clock belong to LFPRp(D) then their valuations have the same fractional part.
Indeed, from Definition 4.5 if xi,xj∈LFPRp(D) then both (0,≤)≤Di,j
and (0,≤)≤Dj,i are valid for Rp, and from Definition 3.5 (2)
we must have Di,j=Dj,i=(0,≤)(⋆).
Let v∈Rp.
Assume xi∈LFPRp(D) and w∈(E,v(D)),
by letting time elapse, frac(w(xi)) is the first that might reach 1.
Moreover, for all xj∈X∖LFPRp(D), frac(w(xj)) cannot reach 1 before frac(w(xi)).
We are going to construct a new (E′,D′)=TE<((E,D)), which will be an open–p–PDBM respecting condition 5b of Definition 3.5.
While detailing the procedure of TE<, we are going to prove that Definition 3.5 (1) and (2) hold for (E′,D′).
Further we will prove that (4) and (5b) also hold.
According to the definition of TE< (Algorithm 2)
the first step is to set a new upper bound
[TABLE]
and obviously (0,≤)≤Di,0′≤(1,≤) is valid for Rp.
Then we set new upper bounds for all other clock xj∈X∖LFPRp(D) by setting
[TABLE]
Indeed, Dj,i is the constraint on the lower bound of frac(w(xj))−frac(w(xi))
and since the upper bound of xi has increased, this gives the new upper bound of xj.
Note that since xi∈LFPRp(D), from Definition 4.5 and Definition 3.5 (2)
we have that −1≤Dj,i≤0 is valid for Rp for all clock xj.
Precisely, dj,i∈{0,−p1,p2−p1,p1−1−p2,p1−1} for some p1,p2∈P
where p2≤p1 is valid for Rp.
Hence as dj,i+1∈{1,1−p1,p2+1−p1,p1−p2,p1},
we have that dj,0′∈PLT, ◃ji′=◃ji⊕<=< so (0,≤)≤Dj,0′≤(1,<) is valid for Rp.
Note that we cannot have (dj,i,◃ji)=(−1,<) because even if (di,j,◃ij)=(1,<), since (E,D)∈p–PDBM■(Rp) we do not have have 0≤Dj,i+Di,j is valid for Rp from Definition 3.5 (4) and Lemma 3.7.
Secondary we set for all clock x regardless of whether they are in LFPRp(D)
[TABLE]
Since some time elapsed, lower bounds of all clocks are increased.
Moreover, as (−1,<)≤D0,x≤(0,≤) is valid for Rp from Definition 3.5 (1),
(−1,≤)≤D0,x′≤(0,≤) is also valid for Rp.
Third we set for all clocks x,y regardless of whether they are in LFPRp(D)
[TABLE]
so as Definition 3.5 (2) holds in (E,D), it still does.
More intuitively since no fractional part has reached 1, constraints on differences of clocks and integer parts remain unchanged.
if xi∈LFPRp(D), Di,0′=(1,<), D0,i′=D0,i+(0,<) hence di,0′=d0,i′ and ◃i0′=◃0i′=<, condition Definition 3.5 (3) holds;
•
if xi∈X∖LFPRp(D), x∈LFPRp(D), Di,0′=Di,x+(1,<), D0,i′=D0,i+(0,<) hence as (0,≤)≤Di,0′ is valid for Rp and D0,i′≤(0,≤) is valid for Rp,
we have di,0′=d0,i′ and ◃i0′=◃0i′=< and condition Definition 3.5 (3) holds.
For all xi,xj:
•
if xi,xj∈X∖LFPRp(D), Di,j′=Di,j and Dj,i′=Dj,i, condition Definition 3.5 (3) holds as it holds for Di,j and Dj,i.
•
if xi∈X∖LFPRp(D), xj∈LFPRp(D), Di,0′=Di,j+(1,<), D0,i′=D0,i+(0,<) hence as (0,≤)≤Di,0′ is valid for Rp and D0,i′≤(0,≤) is valid for Rp,
we have di,0′=d0,i′ and ◃i0′=◃0i′=<, condition Definition 3.5 (3) holds. The case xj∈X∖LFPRp(D), xi∈LFPRp(D) is treated similarly.
•
if xi,xj∈LFPRp(D), Di,j′=Dj,i′=(0,≤), hence di,j′=−dj,i′=0 and ◃ij′=◃ji′=≤ and condition Definition 3.5 (3) holds.
Now we prove that Definition 3.5 (4) holds, i. e., for all clocks xi,xj,xk,
valid conditions such as Di,j′≤Di,k′+Dk,j′ remain valid in Rp.
Indeed, when time elapses, all clocks have the same behavior, hence the difference between two clocks does not change without an update.
Precisely, for all clocks xi,xj,xk, are valid for Rp:
(1)
if xi,xj,xk∈X∖LFPRp(D): let x∈LFPRp(D) and
•
if i,j,k are different from [math], we have Di,k′=Di,k, Di,j′=Di,j and Dj,k′=Dj,k;
since (E,D)∈p–PDBM■(Rp) from Definition 3.5 (4), we know that Di,k≤Di,j+Dj,k is valid for Rp;
therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
•
if i,j are different from [math], k=0, we have Di,0′=Di,x+(1,<), Di,j′=Di,j and Dj,0′=Dj,x+(1,<);
since (E,D)∈p–PDBM■(Rp) from Definition 3.5 (4), we know that Di,x≤Di,j+Dj,x is valid for Rp;
then Di,x+(1,<)≤Di,j+Dj,x+(1,<) is valid for Rp from Lemma 3.4 and therefore, Di,0′≤Di,j′+Dj,0′ is valid for Rp.
•
if i,k are different from [math], j=0, we have Di,k′=Di,k, Di,0′=Di,x+(1,<) and D0,k′=D0,k+(0,<);
we claim that
[TABLE]
is valid for Rp, which is equivalent to Di,k′≤Di,0′+D0,k′ is valid for Rp.
Since (E,D)∈p–PDBM■(Rp) from Definition 3.5 (1), we know that
[TABLE]
moreover we have
[TABLE]
Since (E,D)∈p–PDBM■(Rp) from Definition 3.5 (4), we know that Dx,k≤Dx,0+D0,k is valid for Rp;
combining with (6) and (7) we obtain
[TABLE]
Now, since (E,D)∈p–PDBM■(Rp) from Definition 3.5 (4), we know that Di,k≤Di,x+Dx,k is valid for Rp
and combining with (8) we obtain (5) and therefore our result.
•
if i is different from [math], j=k=0, we have Di,0′=Di,x+(1,<);
from Definition 3.3 (2b) we have that
[TABLE]
is valid for Rp.
Hence from Lemma 3.8
[TABLE]
is valid for Rp.
•
if j,k are different from [math], i=0, we have D0,k′=D0,k+(0,<), D0,j′=D0,j+(0,<) and Dj,k′=Dj,k;
since (E,D)∈p–PDBM■(Rp), from Definition 3.5 (4)
we know that D0,k≤D0,j+Dj,k is valid for Rp.
Moreover we have that
[TABLE]
so we have from Definition 3.3 (2b)
[TABLE]
is valid for Rp.
Hence D0,k′≤D0,j′+Dj,k′ is valid for Rp.
•
if j is different from [math], i=k=0, we have D0,0′=(0,≤), D0,j′=D0,j+(0,<) and Dj,0′=Dj,x+(1,<);
since (E,D)∈p–PDBM■(Rp), from Definition 3.5 (4)
we know that D0,x≤D0,j+Dj,x is valid for Rp;
moreover, from Definition 3.3 (2b) and Lemma 3.4,
[TABLE]
is valid for Rp.
Recall that from Lemma 3.7(0,≤)≤D0,x+Dx,0 is valid for Rp
and since Dx,0≤(1,<) from Definition 3.5 (1),
we have
[TABLE]
is valid for Rp.
As we have (1,<)+(0,<)=(1+0,<⊕<)=(1,<),
we obtain that
[TABLE]
is valid for Rp and therefore D0,0′≤D0,j′+Dj,0′ is valid for Rp.
•
if k is different from [math], i=j=0, we have D0,k′=D0,k+(0,<);
From Definition 3.3 (2b) and Lemma 3.4 we have that
[TABLE]
is valid for Rp.
Hence from Lemma 3.8
[TABLE]
is valid for Rp.
•
if i=j=k=0, from Definition 3.5 (4) and Lemma 3.8
we trivially have
[TABLE]
is valid for Rp.
2. (2)
if xk∈LFPRp(D) and xi,xj∈X∖LFPRp(D): k=0 and
•
if i,j are different from [math], we have Di,k′=Di,k, Di,j′=Di,j and Dj,k′=Dj,k;
since (E,D)∈p–PDBM■(Rp) from Definition 3.5 (4), we know that Di,k≤Di,j+Dj,k;
therefore, Di,k′≤Di,j′+Dj,k′.
•
if i=0, j=0, we have Di,k′=Di,k, Di,0′=Di,k+(1,<) and D0,k′=D0,k+(0,<);
we claim that Di,k≤Di,k+(1,<)+D0,k+(0,<) is valid for Rp, i. e.,
[TABLE]
is valid for Rp, which is equivalent to Di,k′≤Di,0′+D0,k′ is valid for Rp.
We have
[TABLE]
Since (E,D)∈p–PDBM■(Rp), from Definition 3.5 (4)
we know that (0,≤)≤D0,k+Dk,0 is valid for Rp
and from Definition 3.5 (1) that Dk,0≤(1,<) is valid for Rp;
combining with (9) and (10) we obtain our result.
•
if i=0, j=0, we have D0,k′=D0,k+(0,<), D0,j′=D0,j+(0,<) and Dj,k′=Dj,k;
since (E,D)∈p–PDBM■(Rp), from Definition 3.5 (4) we know that D0,k≤D0,j+Dj,k.
Moreover we have that
[TABLE]
so we have from Definition 3.3 (2b)
[TABLE]
is valid for Rp.
Hence D0,k′≤D0,j′+Dj,k′ is valid for Rp.
•
if i=j=0, from Definition 3.5 (4) and Lemma 3.8 we trivially have
[TABLE]
is valid for Rp.
3. (3)
if xj∈LFPRp(D) and xi,xk∈X∖LFPRp(D): j=0 and
•
if i,k are different from [math], we have Di,k′=Di,k, Di,j′=Di,j and Dj,k′=Dj,k;
since (E,D)∈p–PDBM■(Rp), from Definition 3.5 (4)
we know that Di,k≤Di,j+Dj,k is valid for Rp;
therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
•
if i=0, k=0, we have Di,0′=Di,j+(1,<), Di,j′=Di,j and Dj,0′=(1,<);
From Definition 3.3 (2b) we trivially have that
Di,j+(1,<)≤Di,j+(1,<) is valid for Rp and therefore, Di,0′≤Di,j′+Dj,0′ is valid for Rp.
•
if i=0, k=0, we have D0,k′=D0,k+(0,<), D0,j′=D0,j+(0,<) and Dj,k′=Dj,k;
since (E,D)∈p–PDBM■(Rp), from Definition 3.5 (4) we know that D0,k≤D0,j+Dj,k is valid for Rp.
Moreover we have that
[TABLE]
so we have from Definition 3.3 (2b) and Lemma 3.4
[TABLE]
is valid for Rp.
Hence D0,k′≤D0,j′+Dj,k′ is valid for Rp.
•
if i=k=0, we have D0,0′=(0,≤), D0,j′=D0,j+(0,<) and Dj,0′=(1,<);
since (E,D)∈p–PDBM■(Rp), from Lemma 3.7 we know that (0,≤)≤D0,j+Dj,0 is valid for Rp,
and since from Definition 3.5 (1) Dj,0≤(1,≤) is valid for Rp, that means (0,≤)≤D0,j+(1,<) is valid for Rp.
As we have
[TABLE]
we obtain that
[TABLE]
is valid for Rp and therefore D0,0′≤D0,j′+Dj,0′ is valid for Rp.
4. (4)
if xj,xk∈LFPRp(D) and xi∈X∖LFPRp(D): j=0,k=0 and
•
if i is different from [math], we have Di,k′=Di,k, Di,j′=Di,j and Dj,k′=Dj,k;
since (E,D)∈p–PDBM■(Rp), from Definition 3.5 (4) we know that Di,k≤Di,j+Dj,k;
therefore, Di,k′≤Di,j′+Dj,k′.
•
if i=0, we have D0,k′=D0,k+(0,<), D0,j′=D0,j+(0,<) and Dj,k′=Dj,k;
since (E,D)∈p–PDBM■(Rp), from Definition 3.5 (4) we know that D0,k≤D0,j+Dj,k.
Moreover we have that
[TABLE]
so we have from Definition 3.3 (2b) and Lemma 3.4
[TABLE]
is valid for Rp.
Hence D0,k′≤D0,j′+Dj,k′ is valid for Rp.
5. (5)
if xi∈LFPRp(D) and xj,xk∈X∖LFPRp(D): i=0 and
•
if j,k are different from [math], we have Di,k′=Di,k, Di,j′=Di,j and Dj,k′=Dj,k;
since (E,D)∈p–PDBM■(Rp), from Definition 3.5 (4) we know that Di,k≤Di,j+Dj,k;
therefore, Di,k′≤Di,j′+Dj,k′.
•
if j=0, k=0, we have Di,0′=(1,<), Di,j′=Di,j and Dj,0′=Dj,i+(1,<);
from Definition 3.5 (4) and Lemma 3.7 we know that (0,≤)≤Di,j+Dj,i is valid for Rp.
Since, from Definition 3.3 (2b) (1,<)≤(1,<) is valid for Rp,
then from Lemma 3.4
[TABLE]
is valid for Rp and therefore, Di,0′≤Di,j′+Dj,0′ is valid for Rp.
•
if j=0, k=0, we have Di,k′=Di,k, Di,0′=(1,<) and D0,k′=D0,k+(0,<);
we claim that
[TABLE]
is valid for Rp, which is equivalent to Di,k′≤Di,0′+D0,k′ is valid for Rp.
Since (E,D)∈p–PDBM■(Rp) from Definition 3.5 (4), we know that Di,k≤Di,0+D0,k is valid for Rp;
moreover, from Definition 3.5 (1), we know that Di,0≤(1,<) is valid for Rp.
We have
[TABLE]
so we obtain that
[TABLE]
is valid for Rp and therefore our result.
•
if i is different from [math], j=k=0, we have Di,0′=(1,<), D0,0′=(0,≤);
from Definition 3.3 (2b) we have that
[TABLE]
is valid for Rp.
Hence from Lemma 3.8
[TABLE]
is valid for Rp.
6. (6)
if xi,xk∈LFPRp(D) and xj∈X∖LFPRp(D): i=0,k=0 and
•
if j=0, we have Di,k′=Di,k, Di,j′=Di,j and Dj,k′=Dj,k;
since (E,D)∈p–PDBM■(Rp), from Definition 3.5 (4) we know that Di,k≤Di,j+Dj,k;
therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
•
if j=0, we have Di,k′=Di,k, Di,0′=(1,<) and D0,k′=D0,k+(0,<);
we claim that
[TABLE]
is valid for Rp, which is equivalent to Di,k′≤Di,0′+D0,k′ is valid for Rp.
Since (E,D)∈p–PDBM■(Rp) from Definition 3.5 (4), we know that Di,k≤Di,0+D0,k is valid for Rp;
moreover, from Definition 3.5 (1), we know that Di,0≤(1,<) is valid for Rp.
We have
[TABLE]
so we obtain that
[TABLE]
is valid for Rp and therefore our result.
7. (7)
if xi,xj∈LFPRp(D) and xk∈X∖LFPRp(D): i=0,j=0 and
•
if k=0, we have Di,k′=Di,k, Di,j′=Di,j and Dj,k′=Dj,k;
since (E,D)∈p–PDBM■(Rp), from Definition 3.5 (4) we know that Di,k≤Di,j+Dj,k is valid for Rp;
therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
•
if k=0, we have Di,0′=(1,<), Di,j′=Di,j=(0,≤) since both xi,xj∈LFPRp(D) (cf. (⋆)) and Dj,0′=(1,<);
then (1,<)≤(0,≤)+(1,<) is valid for Rp and therefore, Di,0′≤Di,j′+Dj,0′ is valid for Rp.
8. (8)
if xi,xj,xk∈LFPRp(D):
i,j,k are different from [math], we have Di,k′=Di,k, Di,j′=Di,j and Dj,k′=Dj,k;
since (E,D)∈p–PDBM■(Rp), from Definition 3.5 (4) we know that Di,k≤Di,j+Dj,k is valid for Rp;
therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
Finally, for xi∈LFPRp(D), Di,0′=(1,<) and for all clock j s.t. D0,j′=(0,◃0j′), then we have\leavevmode◃0j′=<.
Condition Definition 3.5 (5b) is satisfied.
We denote by (E,D′) the obtained p–PDBM and (E,D′)∈p–PDBM■(Rp).
Let (E,D)∈p–PDBM■(Rp); let xi∈LFPRp(D), xj∈X∖LFPRp(D).
If (di,j,◃ij)=(0,◃), then ◃=<
Proof G.3**.**
Let xi∈LFPRp(D), xj∈X∖LFPRp(D).
Suppose (di,j,◃ij)=(0,≤). From Definition 3.5 (2) we should have that (dj,i,◃ji)=(0,≤)
so Lemma 3.7 is satisfied, and then xj∈LFPRp(D).
Claim 3** (modification of an open–p–PDBM respecting condition 5b under TE=).**
Let Rp be a parameter region and (E,D)∈p–PDBM■(Rp) respecting condition 5b,
then TE=(E,D)∈p–PDBM■(Rp) respecting condition 5a.
Proof G.4**.**
Suppose (E,D)∈p–PDBM■(Rp) respects condition (5a) of Definition 3.5
i. e., we have at least an x s.t. Dx,0=(1,<) and for all other j s.t. D0,j=(0,◃0j), ◃0j=<.
First we can determine LFPRp(D). Let x∈LFPRp(D).
If more than one clock belong to LFPRp(D) then their valuations have the same fractional part.
Indeed, from Definition 4.5 if xi,xj∈LFPRp(D) then both (0,≤)≤Di,j
and (0,≤)≤Dj,i are valid for Rp, and from Definition 3.5 (2)
we must have Di,j=Dj,i=(0,≤).
Let v∈Rp. Let xi∈LFPRp(D) and w∈(E,v(D)).
By letting time elapse, frac(w(x)) is the first to actually reach 1.
Moreover, for all xj∈X∖LFPRp(D), frac(w(xj)) cannot reach 1 before frac(w(xi)).
We are going to construct a new (E′,D′)=TE=((E,D)) which is an open–p–PDBM respecting condition 5b.
While detailing the procedure of TE=, we are going to prove that Definition 3.5 (1) and (2) hold for (E′,D′). Further we will prove that (4) and (5a) also hold.
According to the definition of TE=Algorithm 3,
the first step is to fix the value of frac(xi) to [math] by setting
[TABLE]
Indeed, when frac(xi) reaches 1,
in the constraints expressed by (E,v(D)) we have to increase the integer part by 1 and set the new constraints on the fractional part to [math].
Secondary we set new upper and lower bound for all other clock xj∈X∖LFPRp(D)
[TABLE]
We have to force now upper and lower bounds for other clocks since we know the interval of time that elapsed when xi reached 1.
Note that since xi∈LFPRp(D), xj∈X∖LFPRp(D)
from Definition 4.5 we have that (0,≤)≤Di,j≤(1,<) is valid for Rp for all clock xj.
Nonetheless, since xj∈X∖LFPRp(D), we even have Di,j=(0,≤):
suppose (di,j,◃ij)=(0,≤):
from Definition 3.5 (2) we should have that (dj,i,◃ji)=(0,≤)
so Lemma 3.7 is satisfied, and then xj∈LFPRp(D).
The same reasoning leads to Dj,i=(0,≤).
Obviously, we have Di,j=(0,<): suppose Di,j=(0,<),
since xi∈LFPRp(D)
then from Definition 4.5(0,≤)≤Di,j should be valid for Rp,
which is not from Definition 3.3 (2b).
Precisely, di,j∈{1,1−p1,p2+1−p1,p1−p2,p1} for any two p1,p2∈P
where p2≤p1 is valid for Rp.
Hence as −1+di,j∈{0,−p1,p2−p1,p1−1−p2,p1−1},
we have that D0,j′∈PLT and (−1,<)≤D0,j′≤(0,≤) is valid for Rpfrom Lemma 2.
Also note that since xi∈LFPRp(D), from Definition 4.5 and Definition 3.5 (2)
we have that (−1,<)≤Dj,i≤(0,≤) is valid for Rp for all clock xj.
Precisely, dj,i∈{0,−p1,p2−p1,p1−1−p2,p1−1} for some p1,p2∈P
where p2≤p1 is valid for Rp.
Hence as dj,i+1∈{1,1−p1,p2+1−p1,p1−p2,p1},
we have that dj,0′∈PLT and (0,≤)≤Dj,0′≤(1,<) is valid for Rp.
if xi∈LFPRp(D), Di,0′=(0,≤), D0,i′=(0,≤) hence di,0′=−d0,i′ and ◃i0′◃0i′=≤, condition Definition 3.5 (3) holds;
•
if xi∈X∖LFPRp(D), x∈LFPRp(D), Di,0′=Di,x+(1,≤), D0,i′=Dx,i+(−1,≤) as condition Definition 3.5 (3) holds
for Di,x and Dx,i and ◃ij⊕≤=◃ij, ◃ji⊕≤=◃ji, condition Definition 3.5 (3) holds for Di,0′ and D0,i′.
For all xi,xj:
•
if xi,xj∈X∖LFPRp(D), Di,j′=Di,j and Dj,i′=Dj,i, condition Definition 3.5 (3) holds as it holds for Di,j and Dj,i.
•
if xi∈X∖LFPRp(D), xj∈LFPRp(D), Di,j′=Di,j+(1,≤), Dj,i′=Dj,i+(−1,≤) condition Definition 3.5 (3) holds
for Di,j and Dj,i and ◃ij⊕≤=◃ij, ◃ji⊕≤=◃ji, condition Definition 3.5 (3) holds for Di,j′ and Dj,i′.
The case xj∈X∖LFPRp(D), xi∈LFPRp(D) is treated similarly.
•
if xi,xj∈LFPRp(D), Di,j′=Dj,i′=(0,≤), hence di,j′=−dj,i′=0 and ◃ij′◃ji′=≤ and condition Definition 3.5 (3) holds.
Now we prove that Definition 3.5 (4) holds, i. e., for all clocks xi,xj,xk,
valid conditions such as Di,j′≤Di,k′+Dk,j′ remain valid in Rp.
This is not trivial since, in this construction some clocks have been updated.
Precisely, for all clocks xi,xj,xk, are valid for Rp:
(1)
if xi,xj,xk∈X∖LFPRp(D): let x∈LFPRp(D) and
•
if i,j,k are different from [math], we have Di,k′=Di,k, Di,j′=Di,j and Dj,k′=Dj,k;
since (E,D)∈p–PDBM■(Rp), from Definition 3.5 (4) we know that Di,k≤Di,j+Dj,k is valid for Rp;
therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
•
if i,j are different from [math], k=0, we have Di,0′=Di,x+(1,≤), Di,j′=Di,j and Dj,0′=Dj,x+(1,≤);
since (E,D)∈p–PDBM■(Rp), from Definition 3.5 (4) we know that Di,x≤Di,j+Dj,x is valid for Rp;
then from Lemma 3.4Di,x+(1,≤)≤Di,j+Dj,x+(1,≤) is valid for Rp and therefore, Di,0′≤Di,j′+Dj,0′ is valid for Rp.
•
if i,k are different from [math], j=0, we have Di,k′=Di,k, Di,0′=Di,x+(1,≤) and D0,k′=Dx,k+(−1,≤);
we claim that
[TABLE]
is valid for Rp, which is equivalent to Di,k′≤Di,0′+D0,k′ is valid for Rp.
We have
[TABLE]
Since (E,D)∈p–PDBM■(Rp) from Definition 3.5 (4), we know that Di,k≤Di,x+Dx,k is valid for Rp;
combining with (12) and since Dx,k+(0,≤)=Dx,k,
we obtain (11) and therefore our result.
•
if i is different from [math], j=k=0, we have Di,0′=Di,x+(1,≤), Dj,k′=D0,0′=(0,≤);
we have from Definition 3.3 (2b) that
[TABLE]
is valid for Rp.
Hence Lemma 3.8 gives that
[TABLE]
is valid for Rp.
•
if j,k are different from [math], i=0, we have D0,k′=Dx,k+(−1,≤), D0,j′=Dx,j+(−1,≤) and Dj,k′=Dj,k;
since (E,D)∈p–PDBM■(Rp), from Definition 3.5 (4) we know that Dx,k≤Dx,j+Dj,k is valid for Rp.
Moreover we have that
[TABLE]
is valid for Rp so we have from Definition 3.3 (2b) and Lemma 3.4
[TABLE]
is valid for Rp.
Hence D0,k′≤D0,j′+Dj,k′ is valid for Rp.
•
if j is different from [math], i=k=0, we have D0,j′=Dx,j+(−1,≤) and Dj,0′=Dj,x+(1,≤);
since (E,D)∈p–PDBM■(Rp), from Lemma 3.7 we know that (0,≤)≤Dx,j+Dj,x is valid for Rp;
moreover, we have that
[TABLE]
and Dj,x+(0,≤)=Dj,x.
Then we have from Lemma 3.4
[TABLE]
is valid for Rp and therefore D0,0′≤D0,j′+Dj,0′ is valid for Rp.
•
if k is different from [math], i=j=0, we have D0,k′=Dx,k+(−1,≤), Di,j′=D0,0′=(0,≤);
we have from Definition 3.3 (2b) that
[TABLE]
is valid for Rp.
Hence, as Dx,k+(−1,≤)+(0,≤)=Dx,k+(−1,≤) we have
[TABLE]
is valid for Rp.
•
if i=j=k=0, we trivially have from Definition 3.5 (4) and Lemma 3.8
[TABLE]
is valid for Rp.
2. (2)
if xk∈LFPRp(D) and xi,xj∈X∖LFPRp(D): k=0 and
•
if i,j are different from [math], we have Di,k′=Di,0′=Di,k+(1,≤), Di,j′=Di,j and Dj,k′=Dj,0′=Dj,k+(1,≤);
since (E,D)∈p–PDBM■(Rp), from Definition 3.5 (4) we know that Di,k≤Di,j+Dj,k is valid for Rp;
moreover, since we have (1,≤)≤(1,≤) is valid for Rp
then from Lemma 3.4
[TABLE]
is valid for Rp, therefore we have Di,k′≤Di,j′+Dj,k′ is valid for Rp.
•
if i=0, j=0, we have Di,k′=Di,0′=Di,k+(1,≤), Di,0′=Di,k+(1,≤) and D0,k′=(0,≤);
clearly
[TABLE]
and
[TABLE]
are valid for Rp, then from Lemma 3.4
we obtain Di,k′≤Di,0′+D0,k′ is valid for Rp.
•
if i=0, j=0, we have D0,k′=(0,≤), D0,j′=Dk,j+(−1,≤) and Dj,k′=Dj,0′=Dj,k+(1,≤);
since (E,D)∈p–PDBM■(Rp), from Lemma 3.7
we know that (0,≤)≤Dk,j+Dj,k is valid for Rp.
Moreover we have that
[TABLE]
so we have from Lemma 3.4
[TABLE]
is valid for Rp.
Hence D0,k′≤D0,j′+Dj,k′ is valid for Rp.
•
if i=j=0, we trivially have from Definition 3.5 (4) and Lemma 3.8
[TABLE]
is valid for Rp.
3. (3)
if xj∈LFPRp(D) and xi,xk∈X∖LFPRp(D): j=0 and
•
if i,k are different from [math], we have Di,k′=Di,k, Di,j′=Di,0′=Di,j+(1,≤) and Dj,k′=D0,k′=Dj,k+(−1,≤);
since (E,D)∈p–PDBM■(Rp), from Definition 3.5 (4) we know that Di,k≤Di,j+Dj,k is valid for Rp;
moreover, since we have
[TABLE]
then as Di,j+Dj,k+(0,≤)=Di,j+Dj,k,
clearly Di,k′≤Di,j′+Dj,k′ is valid for Rp.
•
if i=0, k=0, we have Di,0′=Di,j+(1,≤), Di,j′=Di,0′=Di,j+(1,≤) and Dj,0′=(0,≤);
From Definition 3.3 (2b) we trivially have that
Di,j+(1,≤)≤Di,j+(1,≤) is valid for Rp and therefore, Di,0′≤Di,j′+Dj,0′ is valid for Rp.
•
if i=0, k=0, we have D0,k′=Dj,k+(−1,≤), D0,j′=(0,≤) and Dj,k′=D0,k′=Dj,k+(−1,≤);
since (E,D)∈p–PDBM■(Rp), from Definition 3.5 (4) we know that D0,k≤D0,j+Dj,k is valid for Rp.
From Definition 3.3 (2b) we trivially have that
Dj,k+(−1,≤)≤Dj,k+(−1,≤) is valid for Rp.
As (−1,≤)+(0,≤)=(−1,≤), we have D0,k′≤D0,j′+Dj,k′ is valid for Rp.
•
if i=k=0, we have D0,j′=(0,≤) and Dj,0′=(0,≤);
As we have
[TABLE]
we clearly have that D0,0′≤D0,j′+Dj,0′ is valid for Rp.
4. (4)
if xj,xk∈LFPRp(D) and xi∈X∖LFPRp(D): j=0,k=0 and
•
if i is different from [math], we have Di,k′=Di,0′=Di,k+(−1,≤), Di,j′=Di,0′=Di,k+(−1,≤) and Dj,k′=(0,≤);
we have that (−1,≤)+(0,≤)=(−1,≤) and
[TABLE]
holds from Definition 3.3 (2b).
Therefore, Di,k′≤Di,j′+Dj,k′.
•
if i=0, we have D0,k′=(0,≤), D0,j′=(0,≤) and Dj,k′=(0,≤);
since (E,D)∈p–PDBM■(Rp) from Definition 3.5 (4), we know that D0,k≤D0,j+Dj,k.
As we have
[TABLE]
we clearly have that D0,k′≤D0,j′+Dj,k′ is valid for Rp.
5. (5)
if xi∈LFPRp(D) and xj,xk∈X∖LFPRp(D): i=0 and
•
if j,k are different from [math], we have Di,k′=D0,k′=Di,k+(−1,≤), Di,j′=D0,j′=Di,j+(−1,≤) and Dj,k′=Dj,k;
since (E,D)∈p–PDBM■(Rp), from Definition 3.5 (4) we know that Di,k≤Di,j+Dj,k is valid for Rp;
moreover, since we have
[TABLE]
is valid for Rp then from Lemma 3.4 we have Di,k′≤Di,j′+Dj,k′ is valid for Rp.
•
if j=0, k=0, we have Di,0′=(0,≤), Di,j′=D0,j′=Di,j+(−1,≤) and Dj,0′=Dj,i+(1,≤);
from Lemma 3.7 we know that (0,≤)≤Di,j+Dj,i is valid for Rp.
Moreover, we have
[TABLE]
then
[TABLE]
is valid for Rp and therefore, Di,0′≤Di,j′+Dj,0′ is valid for Rp.
•
if j=0, k=0, we have Di,k′=Di,k, Di,0′=(1,≤) and D0,k′=Di,k+(−1,≤);
we have that
[TABLE]
and from Definition 3.3 (2b) that
[TABLE]
is valid for Rp, which gives us our result.
•
if i is different from [math], j=k=0, we have Di,0′=(0,≤), Dj,k′=D0,0′=(0,≤);
we have from Definition 3.3 (2b) that
[TABLE]
is valid for Rp.
Hence
[TABLE]
is valid for Rp.
6. (6)
if xi,xk∈LFPRp(D) and xj∈X∖LFPRp(D): i=0,k=0 and
•
if j=0, we have Di,k′=(0,≤), Di,j′=D0,j′=Di,j+(−1,≤) and Dj,k′=Dj,0′=Dj,i+(1,≤);
since (E,D)∈p–PDBM■(Rp), from Lemma 3.7
we know that (0,≤)≤Di,j+Dj,i is valid for Rp;
we have
[TABLE]
and therefore from Lemma 3.4, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
•
if j=0, we have Di,k′=(0,≤), Di,0′=(0,≤) and D0,k′=(0,≤);
we have that (0,≤)+(0,≤)=(0,≤) and from Definition 3.3 (2b)
[TABLE]
is valid for Rp.
Therefore we obtain our result.
7. (7)
if xi,xj∈LFPRp(D) and xk∈X∖LFPRp(D): i=0,j=0 and
•
if k=0, we have Di,k′=D0,k′=Di,k+(−1,≤), Di,j′=(0,≤) and Dj,k′=D0,k′=Di,k+(−1,≤);
we have that
[TABLE]
is valid for Rp and from Lemma 3.4
[TABLE]
is valid for Rp. Therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
•
if k=0, we have Di,0′=(0,≤), Di,j′=(0,≤) and Dj,0′=(0,≤);
we have that (0,≤)+(0,≤)=(0,≤) and from Definition 3.3 (2b)
[TABLE]
is valid for Rp: therefore Di,0′≤Di,j′+Dj,0′ is valid for Rp.
8. (8)
if xi,xj,xk∈LFPRp(D):
i,j,k are different from [math], we have Di,k′=(0,≤), Di,j′=(0,≤) and Dj,k′=(0,≤);
we have that (0,≤)+(0,≤)=(0,≤) and from Definition 3.3 (2b)
[TABLE]
is valid for Rp: therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
Finally, there is at least one clock xi∈LFPRp(D) s.t. D0,i=Di,0=(0,≤).
Hence condition Definition 3.5 (5a) holds.
To conclude the proof, we set Ei′=Ei+1 if xi∈LFPRp(D) and Ej′=Ej if xj∈X∖LFPRp(D)
We denote by (E,D′) the obtained p–PDBM and (E′,D′)∈p–PDBM■(Rp).
Claim 4** (p–PDBM⊙(Rp) becomes p–PDBM■(Rp) after TE<).**
Let Rp be a parameter region and (E,D)∈p–PDBM⊙(Rp), then \mathit{TE}_{<}\big{(}(E,D)\big{)}\in p\textsf{--}\mathcal{PDBM}_{\blacksquare}(R_{p}) respecting condition 5b.
Proof G.5**.**
Suppose (E,D)∈p–PDBM⊙(Rp).
Since, in Rp, we know which parameters have the largest fractional part, we can determine LFPRp(D) from Lemma 4.6.
If more than one clock belong to LFPRp(D) then their valuations have the same fractional part.
Indeed, from Definition 4.5 if xi,xj∈LFPRp(D) then both (0,≤)≤Di,j and (0,≤)≤Dj,i are valid for Rp, and from Definition 3.5 (2)
we must have Di,j=Dj,i=(0,≤).
Let v∈Rp. Let xi∈LFPRp(D) and w∈(E,v(D)).
By letting time elapse, frac(w(xi)) is the first that might reach 1.
Moreover, for all xj∈X∖LFPRp(D), frac(w(xj)) cannot reach 1 before frac(w(xi)).
We are going to construct a new (E′,D′)=TE<((E,D)) which is an open–p–PDBM respecting condition 5b.
While detailing the procedure of TE<, we are going to prove that Definition 3.5 (1) and (2) hold for (E′,D′). Further we will prove that (4) and (5b) also hold.
According to the definition of TE< (Algorithm 2)
the first step is to set a new upper bound
[TABLE]
and obviously (0,≤)≤Di,0′≤(1,<) is valid for Rp.
Then we set new upper bounds for all other clock xj∈X∖LFPRp(D) by setting
[TABLE]
Indeed, Dj,i is the constraint on the lower bound of w(xj)−w(xi)
and since the upper bound of xi has increased, this gives the new upper bound of xj.
Note that since xi∈LFPRp(D), from Definition 4.5 we have for all clock xj that (−1,<)≤Dj,i≤(0,≤) is valid for Rp.
Precisely, dj,i∈{0,−p1,p2−p1,p1−1−p2,p1−1} for some p1,p2∈P
where p2≤p1 is valid for Rp.
Hence as dj,i+1∈{1,1−p1,p2+1−p1,p1−p2,p1},
we have that dj,0′∈PLT, ◃j0′=◃j0′⊕<=< and (0,≤)≤Dj,0′≤(1,<) is valid for Rp.
Note that we cannot have (dj,i,◃ji)=(−1,<) because even if (di,j,◃ij)=(1,<), since (E,D)∈p–PDBM■(Rp) we do not have have 0≤Dj,i+Di,j is valid for Rp from Definition 3.5 (4) and Lemma 3.7.
Secondary we set for all clock x regardless of whether they are in LFPRp(D)
[TABLE]
Since some time elapsed, lower bounds of all clocks are increased.
Moreover, from Definition 3.6 (1) as (−1,<)≤D0,x≤(0,≤) is valid for Rp,
(−1,<)≤D0,x′≤(0,≤) is also valid for Rp.
Third we set for all clocks x,y regardless of whether they are in LFPRp(D)
[TABLE]
since no fractional part has reached 1, constraints on differences of clocks and integer parts remain unchanged.
As it is the case in (E,D), Definition 3.5 (2) holds.
if xi∈LFPRp(D), Di,0′=(1,<), D0,i′=D0,i+(0,<) hence di,0′=d0,i′ and ◃i0′◃0i′=<, condition Definition 3.5 (3) holds;
•
if xi∈X∖LFPRp(D), x∈LFPRp(D), Di,0′=Di,x+(1,<), D0,i′=D0,i+(0,<) hence as (0,≤)≤Di,0′ is valid for Rp and D0,i′≤(0,≤) is valid for Rp,
we have di,0′=d0,i′ and ◃i0′◃0i′=< and condition Definition 3.5 (3) holds.
For all xi,xj:
•
if xi,xj∈X∖LFPRp(D), Di,j′=Di,j and Dj,i′=Dj,i, condition Definition 3.5 (3) holds as it holds for Di,j and Dj,i.
•
if xi∈X∖LFPRp(D), xj∈LFPRp(D), Di,0′=Di,j+(1,<), D0,i′=D0,i+(0,<) hence as (0,≤)≤Di,0′ is valid for Rp and D0,i′≤(0,≤) is valid for Rp,
we have di,0′=d0,i′ and ◃i0′◃0i′=<, condition Definition 3.5 (3) holds. The case xj∈X∖LFPRp(D), xi∈LFPRp(D) is treated similarly.
•
if xi,xj∈LFPRp(D), Di,j′=Dj,i′=(0,≤), hence di,j′=−dj,i′=0 and ◃ij′◃ji′=≤ and condition Definition 3.5 (3) holds.
Now we prove that Definition 3.5 (4) holds, i. e., for all clocks xi,xj,xk valid conditions such as Di,j′≤Di,k′+Dk,j′ remain valid in Rp.
Indeed, when time elapses, all clocks have the same behavior, hence the difference between two clocks does not change without an update.
Precisely, for all clocks xi,xj,xk, are valid for Rp:
(1)
if xi,xj,xk∈X∖LFPRp(D): let x∈LFPRp(D) and
•
if i,j,k are different from [math], we have Di,k′=Di,k, Di,j′=Di,j and Dj,k′=Dj,k;
since (E,D)∈p–PDBM⊙(Rp) from Definition 3.6 (2), we know that Di,k≤Di,j+Dj,k is valid for Rp;
therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
•
if i,j are different from [math], k=0, we have Di,0′=Di,x+(1,<), Di,j′=Di,j and Dj,0′=Dj,x+(1,<);
since (E,D)∈p–PDBM⊙(Rp), from Definition 3.6 (2) we know that Di,x≤Di,j+Dj,x is valid for Rp;
then from Lemma 3.4Di,x+(1,<)≤Di,j+Dj,x+(1,<) is valid for Rp and therefore, Di,0′≤Di,j′+Dj,0′ is valid for Rp.
•
if i,k are different from [math], j=0, we have Di,k′=Di,k, Di,0′=Di,x+(1,<) and D0,k′=D0,k+(0,<);
we claim that
[TABLE]
is valid for Rp, which is equivalent to Di,k′≤Di,0′+D0,k′ is valid for Rp.
Since (E,D)∈p–PDBM⊙(Rp), from Definition 3.6 (1) we know that
[TABLE]
is valid for Rp; moreover we have
[TABLE]
Since (E,D)∈p–PDBM⊙(Rp), from Definition 3.6 (2) we know that Dx,k≤Dx,0+D0,k is valid for Rp;
combining with (14) and (15) we obtain Dx,k≤(1,<)+D0,k+(0,<) is valid for Rp.
As Di,x≤Di,x is valid for Rp, using Lemma 3.4
we obtain
[TABLE]
is valid for Rp.
Now, since (E,D)∈p–PDBM⊙(Rp), from Definition 3.6 (2)
we know that Di,k≤Di,x+Dx,k is valid for Rp
and combining with (16) we obtain (13) and therefore our result.
•
if i is different from [math], j=k=0, we have Di,0′=Di,x+(1,<), Dj,k′=D0,0′=(0,≤);
we have from Definition 3.3 (2b) that
[TABLE]
is valid for Rp.
Hence
[TABLE]
is valid for Rp.
•
if j,k are different from [math], i=0, we have D0,k′=D0,k+(0,<), D0,j′=D0,j+(0,<) and Dj,k′=Dj,k;
since (E,D)∈p–PDBM⊙(Rp), from Definition 3.6 (2) we know that D0,k≤D0,j+Dj,k is valid for Rp.
Moreover we have that
[TABLE]
so we have from Lemma 3.4
[TABLE]
is valid for Rp.
Hence D0,k′≤D0,j′+Dj,k′ is valid for Rp.
•
if j is different from [math], i=k=0, we have Di,k′=D0,0′=(0,≤), D0,j′=D0,j+(0,<) and Dj,0′=Dj,x+(1,<);
since (E,D)∈p–PDBM⊙(Rp), from Definition 3.6 (2)
we know that D0,x≤D0,j+Dj,x is valid for Rp;
moreover from Lemma 3.4,
[TABLE]
is valid for Rp.
As we have
[TABLE]
we obtain from Lemma 3.4 that
[TABLE]
is valid for Rp.
Recall that from Lemma 3.7(0,≤)≤D0,x+Dx,0 is valid for Rp.
Since from Definition 3.6 (1) Dx,0≤(1,<) is valid for Rp,
we have (0,≤)≤D0,x+(1,<) is valid for Rp.
Therefore D0,0′≤D0,j′+Dj,0′ is valid for Rp.
•
if k is different from [math], i=j=0, we have Di,k′=Dj,k′=D0,k′=D0,k+(0,<), Di,j′=D0,0′=(0,≤);
we have from Definition 3.3 (2b) that
[TABLE]
is valid for Rp.
Hence from Lemma 3.8
[TABLE]
is valid for Rp.
•
if i=j=k=0, we trivially have
[TABLE]
is valid for Rp.
2. (2)
if xk∈LFPRp(D) and xi,xj∈X∖LFPRp(D): k=0 and
•
if i,j are different from [math], we have Di,k′=Di,k, Di,j′=Di,j and Dj,k′=Dj,k;
since (E,D)∈p–PDBM⊙(Rp), from Definition 3.6 (2)
we know that Di,k≤Di,j+Dj,k is valid for Rp;
therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
•
if i=0, j=0, we have Di,k′=Di,k, Di,0′=Di,k+(1,<) and D0,k′=D0,k+(0,<);
we claim that Di,k≤Di,k+(1,<)+D0,k+(0,<), i. e.,
[TABLE]
is valid for Rp, which is from Lemma 3.4 equivalent to Di,k′≤Di,0′+D0,k′ is valid for Rp.
We have
[TABLE]
Since (E,D)∈p–PDBM⊙(Rp), from Definition 3.6 (2)
we know that 0≤D0,k+Dk,0 is valid for Rp
and from Definition 3.6 (1)
that Dk,0≤(1,<) is valid for Rp;
combining with (18) we obtain (17) and therefore our result.
•
if i=0, j=0, we have D0,k′=D0,k+(0,<), D0,j′=D0,j+(0,<) and Dj,k′=Dj,k;
since (E,D)∈p–PDBM⊙(Rp), from Definition 3.6 (2)
we know that D0,k≤D0,j+Dj,k is valid for Rp.
Moreover we have that (0,<)≤(0,<) is valid for Rp
so we have from Lemma 3.4
[TABLE]
is valid for Rp.
Hence D0,k′≤D0,j′+Dj,k′ is valid for Rp.
•
if i=j=0, from Definition 3.6 (2) we trivially have
[TABLE]
is valid for Rp.
3. (3)
if xj∈LFPRp(D) and xi,xk∈X∖LFPRp(D): j=0 and
•
if i,k are different from [math], we have Di,k′=Di,k, Di,j′=Di,j and Dj,k′=Dj,k;
since (E,D)∈p–PDBM⊙(Rp), from Definition 3.6 (2)
we know that Di,k≤Di,j+Dj,k is valid for Rp;
therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
•
if i=0, k=0, we have Di,0′=Di,j+(1,<), Di,j′=Di,j and Dj,0′=(1,<);
from Definition 3.3 (2b) we trivially have that
Di,j+(1,<)≤Di,j+(1,<) is valid for Rp and therefore, Di,0′≤Di,j′+Dj,0′ is valid for Rp.
•
if i=0, k=0, we have D0,k′=D0,k+(0,<), D0,j′=D0,j+(0,<) and Dj,k′=Dj,k;
since (E,D)∈p–PDBM⊙(Rp), from Definition 3.6 (2)
we know that D0,k≤D0,j+Dj,k is valid for Rp.
Moreover we have that (0,<)≤(0,<) is valid for Rp
so we have
[TABLE]
holds from Definition 3.3 (2b).
Hence D0,k′≤D0,j′+Dj,k′ is valid for Rp.
•
if i=k=0, we have D0,j′=D0,j+(0,<) and Dj,0′=(1,<);
since (E,D)∈p–PDBM⊙(Rp), from Lemma 3.7 we know that 0≤D0,j+Dj,0 is valid for Rp,
from Definition 3.6 (1) we know that Dj,0≤1 is valid for Rp
which means 0≤D0,j+(1,<) is valid for Rp.
As we have
[TABLE]
we obtain that
[TABLE]
is valid for Rp and therefore D0,0′≤D0,j′+Dj,0′ is valid for Rp.
4. (4)
if xj,xk∈LFPRp(D) and xi∈X∖LFPRp(D): j=0,k=0 and
•
if i is different from [math], we have Di,k′=Di,k, Di,j′=Di,j and Dj,k′=Dj,k;
since (E,D)∈p–PDBM⊙(Rp), from Definition 3.6 (2)
we know that Di,k≤Di,j+Dj,k is valid for Rp;
therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
•
if i=0, we have D0,k′=D0,k+(0,<), D0,j′=D0,j+(0,<) and Dj,k′=Dj,k;
since (E,D)∈p–PDBM⊙(Rp), from Definition 3.6 (2)
we know that D0,k≤D0,j+Dj,k is valid for Rp.
Moreover we have that (0,<)≤(0,<) is valid for Rp
so we have from Lemma 3.4
[TABLE]
is valid for Rp.
Hence D0,k′≤D0,j′+Dj,k′ is valid for Rp.
5. (5)
if xi∈LFPRp(D) and xj,xk∈X∖LFPRp(D): i=0 and
•
if j,k are different from [math], we have Di,k′=Di,k, Di,j′=Di,j and Dj,k′=Dj,k;
since (E,D)∈p–PDBM⊙(Rp), from Definition 3.6 (2)
we know that Di,k≤Di,j+Dj,k is valid for Rp;
therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
•
if j=0, k=0, we have Di,0′=(1,<), Di,j′=Di,j and Dj,0′=Dj,i+(1,<);
since (E,D)∈p–PDBM⊙(Rp), from Lemma 3.7 we know that 0≤Di,j+Dj,i.
Then from Lemma 3.4
[TABLE]
is valid for Rp and therefore, Di,0′≤Di,j′+Dj,0′ is valid for Rp.
•
if j=0, k=0, we have Di,k′=Di,k, Di,0′=(1,<) and D0,k′=D0,k+(0,<);
we claim that
[TABLE]
is valid for Rp, which is equivalent to Di,k′≤Di,0′+D0,k′ is valid for Rp.
Since (E,D)∈p–PDBM⊙(Rp) from Definition 3.6 (2),
we know that Di,k≤Di,0+D0,k is valid for Rp;
moreover, from Definition 3.6 (1),
we know that Di,0≤(1,<) is valid for Rp.
We have
[TABLE]
We obtain that
[TABLE]
is valid for Rp and therefore our result.
•
if i is different from [math], j=k=0, we have Di,0′=(1,<), Dj,k′=D0,0′=(0,≤);
from Definition 3.3 (2b) we have that
[TABLE]
is valid for Rp.
Hence
[TABLE]
is valid for Rp.
6. (6)
if xi,xk∈LFPRp(D) and xj∈X∖LFPRp(D): i=0,k=0 and
•
if j=0, we have Di,k′=Di,k, Di,j′=Di,j and Dj,k′=Dj,k;
since (E,D)∈p–PDBM⊙(Rp), from Definition 3.6 (2)
we know that Di,k≤Di,j+Dj,k is valid for Rp;
therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
•
if j=0, we have Di,k′=Di,k, Di,0′=(1,<) and D0,k′=D0,k+(0,<);
we claim that
[TABLE]
is valid for Rp, which is equivalent to Di,k′≤Di,0′+D0,k′ is valid for Rp.
Since (E,D)∈p–PDBM⊙(Rp) from Definition 3.6 (2),
we know that Di,k≤Di,0+D0,k is valid for Rp;
moreover, from Definition 3.6 (1),
we know that Di,0≤(1,<) is valid for Rp.
We have
[TABLE]
We obtain that
[TABLE]
is valid for Rp and therefore our result.
7. (7)
if xi,xj∈LFPRp(D) and xk∈X∖LFPRp(D): i=0,j=0 and
•
if k=0, we have Di,k′=Di,k, Di,j′=Di,j and Dj,k′=Dj,k;
since (E,D)∈p–PDBM⊙(Rp), from Definition 3.6 (2),
we know that Di,k≤Di,j+Dj,k is valid for Rp;
therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
•
if k=0, since both xi,xj∈LFPRp(D) we have Di,j′=Di,j=(0,≤), Di,0′=(1,<) and Dj,0′=(1,<);
trivially (1,<)≤(0,≤)+(1,<) is valid for Rp and therefore, Di,0′≤Di,j′+Dj,0′ is valid for Rp.
8. (8)
if xi,xj,xk∈LFPRp(D):
i,j,k are different from [math], we have Di,k′=Di,k, Di,j′=Di,j and Dj,k′=Dj,k;
since (E,D)∈p–PDBM⊙(Rp), from Definition 3.6 (2) we know that Di,k≤Di,j+Dj,k is valid for Rp;
therefore, Di,k′≤Di,j′+Dj,k′ is valid for Rp.
Proposition 4.11** (recalled).**
*Let Rp be a parameter region and (E,D)∈p–PDBM(Rp). Let v∈Rp.
There exists w′∈TE((E,v(D))) iff
there exist w∈(E,v(D)) and a delay δ s.t. w′=w+δ.
*
Proof H.1**.**
Note that this proof is inspired by [HRSV02, Proof of Lemma 3.13]. We treat first open–p–PDBMs and then point–p–PDBMs.
Claim 1**.**
Let (E,D)∈p–PDBM■(Rp). If (E,D) satisfies condition Definition 3.5 (5b)
it has been obtained after applying Algorithm 2
on another open–p–PDBM satisfying condition Definition 3.5 (5a) or a point–p–PDBM.
Let (E,D)∈p–PDBM■(Rp). If (E,D) satisfies condition Definition 3.5 (5a)
it has been obtained after applying Algorithm 3
on another open–p–PDBM satisfying condition Definition 3.5 (5b) or
after a non-parametric update applied on another open–p–PDBM or a point–p–PDBM.
Proof H.2**.**
Let (E,D)∈p–PDBM■(Rp) and suppose (E,D) satisfies condition Definition 3.5 (5b).
Since for all y, if d0,y=0 we have ◃0y=<, from Claim 1 and Claim 2
it cannot be the result of a non-parametric update where there is at least a clock x update and Dx,0=D0,x=(0,≤).
From Claim 3 it cannot be the result of Algorithm 3,
as there must be at least a clock x s.t. Dx,0=D0,x=(0,≤).
Then it is the result either from Claim 1 of Algorithm 2
applied on an open–p–PDBM satisfying condition Definition 3.5 (5a),
or from Claim 4 of Algorithm 2
applied on a point–p–PDBM.
Let (E,D)∈p–PDBM■(Rp) and suppose (E,D) satisfies condition Definition 3.5 (5a).
Since there is at least a clock y s.t. Dy,0=D0,y=(0,≤), from Claims 1 and 4 it cannot be the result of Algorithm 2,
as for all x, if d0,x=0 we must have ◃ox=<.
Then it is the result of either from Claim 3 of Algorithm 3
applied on an open–p–PDBM satisfying condition Definition 3.5 (5b)
or from Claims 1 and 2 of Algorithm 1
applied on an open–p–PDBM or a point–p–PDBM.
Let Rp be a parameter region and (E,D)∈p–PDBM(Rp).
We have to consider two different cases: (E,D)∈p–PDBM■(Rp) and (E,D)∈p–PDBM⊙(Rp).
Claim 2**.**
Let Rp be a parameter region and (E,D)∈p–PDBM■(Rp). Let v∈Rp.
There is w′∈TE((E,v(D))) iff
there is w∈(E,v(D)) and a delay δ s.t. w′=w+δ.
Proof H.3**.**
Let Rp a parameter region and (E,D)∈p–PDBM■(Rp). Let v∈Rp.
Let v∈Rp. Consider (E′,D′)=TE((E,D)) respecting condition Definition 3.5 (5a), i. e.,
suppose there is xis.t.Di,0′=−D0,i′=(0,≤).
Let w′∈(E′,v(D′)), for this xi we have w′(xi)=0.
We need to find a value δs.t.w′−δ∈(E,v(D))
which is equivalent to prove for all xi,xj
[TABLE]
and
[TABLE]
and
[TABLE]
In this proof we are going to define a δ which is different from [math],
and give it an upper bound in order to show that constraints in (E,D)
are satisfied while going backward of\leavevmodeδ* units of time from w′.*
First we will prove that for all clock j, its constraints of lower bound D0,j and upper bound Dj,0 are satisfied.
Second we will prove that for all i, bounds on their difference Di,j and Dj,i are also satisfied.
We want to show that we have to go a little backward in time from w′
to ensure the upper bounds Dj,0 of (E,D) hold.
For this purpose, we are going to prove that for all xj
[TABLE]
is valid for Rp. Intuitively this means upper bounds of clocks in (E′,D′) are greater than in (E,D),
which is consistent as time is elapsing.
As (E′,D′) respects Definition 3.5 (5a) and precisely (E′,D′)=TE=((E,D)),
we know (E,D) is respecting condition Definition 3.5 (5b) from Claim 1.
As frac(w′(xi))=0 it was in (E,D) a clock with the largest fractional part,
i. e.,xi∈LFPRp(D) and Di,0=(1,<).
By definition of TE< (cf. Algorithm 2), in (E,D) which is the open–p–PDBM obtained after the application of TE< on another p–PDBM (see Claim 1),
for each xj∈X∖LFPRp(D), Dj,0=Dj,i+(1,<)
and for all xj∈X, we have Dj,0 is of the form (dj,0,<) for some dj,0.
By definition of TE= applied to (E,D) (cf. Algorithm 3), in (E′,D′), for each xj∈X∖LFPRp(D),
Dj,0′=Dj,i+(1,≤), i. e.,dj,0=dj,0′.
Hence by Definition 3.3 (2b) and as ◃j0′ is either ≤ or <, we have
[TABLE]
is valid for Rp.
Next we define the largest amount of time so that all upper bounds of (E,D) are satisfied.
*We claim that for all xj, frac(w′(xj))−v(dj,0)≤0.
Indeed, remark that by applying Algorithm 2 then 3,
constraints on upper bounds of clocks
in (E,D) and (E′,D′) differ only by their ◃. As for i∈LFPRp(D)
and j∈X∖LFPRp(D) it we have Dj,0=Dj,i+(1,<) in (E,D)
and Dj,0′=Dj,i+(1,≤) in (E′,D′), so dj,0=dj,0′.
Since for any x, its fractional part is less or equal to its upper bound in D and therefore in D′,
any difference between a fractional part and its upper bound is either negative or null.
For all x, since frac(w′(x))◃x0′v(dx,0′)
we have frac(w′(x))−v(dx,0′)◃x0′0.
Since v(dx,0′)=v(dx,0), frac(w′(x))−v(dx,0)◃x0′0,
therefore we have our result.*
Now we claim that we have to go at least an ϵ>0 backward in time to ensure all bounds of (E,D) are met.
Let xj∈X∖LFPRp(D). As
[TABLE]
we have
–
either ◃j0′=< and we already have
frac(w′(xj))<v(dj,0),
–
or ◃j0′=≤ and for any ϵ>0
we have frac(w′(xj))−ϵ<v(dj,0).
It is also true for each xi∈LFPRp(D): after applying TE< recall that we have Di,0=(1,<).
We can take ϵ>0 and define frac(w(xi))=1−ϵ,
so we have frac(w(xi))<v(di,0).
Now that we know we have to go a little backward in time (at least an ϵ>0)
so upper bounds of (E,D) are satisfied, we are going to give an upper bound to ϵ
so that all lower bounds D0,j of (E,D) are also satisfied.
Let
[TABLE]
We want to prove that t1>0.
Let us prove that for all xj, D0,j′≤D0,j is valid for Rp.
Recall that for xi∈LFPRp(D), we have that Di,0=(1,<).
Moreover, from Definition 3.5 (4) Di,j≤Di,0+D0,j is valid for Rp, then we have
[TABLE]
is valid for Rp.
Recall that after applying Algorithm 3,
D0,j′=Di,j+(−1,≤).
By Definition 3.3 (2b) we have (−1,≤)≤(−1,≤).
We invoke Lemma 3.4 which gives
[TABLE]
As, from Definition 3.3 (2b) we have D0,j+(0,<)≤D0,j is valid for Rp,
we infer (19) and it gives
[TABLE]
Since w′∈(E′,v(D′)) we have −frac(w′(xj))◃0j′v(d0,j′),
[TABLE]
Then we have that
[TABLE]
where,
–
either from Definition 3.3 (2a) d0,j′<d0,j;
–
or from Definition 3.3 (2b), d0,j′≤d0,j
and then ◃0j′=◃0j=<.
Indeed as D0,j′≤D0,j is valid for Rp, and since (E,D) is the
open–p–PDBM obtained after the application of TE< (cf. Algorithm 2) on another p–PDBM (see Claim 1),
we have ◃0j=<.
To conclude we have that for all xj either
[TABLE]
or
[TABLE]
As t1 is by definition the minimum value of an expression frac(w′(xj))+v(d0,j) for a given xj,
which as we just proved are all strictly positive, we have that for all xj
[TABLE]
We proved that t1>0,
so we can set δ=2t1 (therefore δ>0).
More intuitively δ is the value right in the middle of the least and the largest amount of time
s.t. we can go backward in time from w′ and respect all constraints defined in (E,v(D)).
Now we are going to prove that for any clock xj, its constraints on lower and upper bounds are satisfied, i. e.,
[TABLE]
First as δ<t1, we have
[TABLE]
which is −v(d0,j)<frac(w′(xj))−δ.
Since (E,D) is the open–p–PDBM obtained after the application of TE< (cf. Algorithm 3) on another p–PDBM (see Claim 1),
we have ◃0j=< so −v(d0,j)◃0jfrac(w′(xj))−δ.
Secondary as 0<δ, we have
[TABLE]
which is frac(w′(xj))−δ<v(dj,0).
Since (E,D) is the open–p–PDBM obtained after the application of TE< (cf. Algorithm 3) on another p–PDBM (see Claim 1),
we have ◃j0=< so frac(w′(xj))−δ◃j0v(dj,0)
Now we prove that constraints defined in (E,D) on differences of clocks are also satisfied
by going back of δ units of time from w′.
Recall that in (E′,D′) we have for all clock xj,
[TABLE]
In addition by definition of TE=, for xi∈LFPRp(D), Exi=Exi′−1
and for xj∈X∖LFPRp(D), Exj=Exj′.
We already treated the case whether i or j are [math], now suppose i,j are both different from [math].
–
if xi,xj∈X∖LFPRp(D): let x∈LFPRp(D) and
recall that after applying Algorithm 3,
Di,j′=Di,j, Dj,i′=Dj,i;
we have that frac(w′(xj))−frac(w′(xi))◃ij′dj,i′=dj,i,
and therefore frac(w′(xj))−δ−frac(w′(xi))+δ◃jidj,i.
We also have that frac(w′(xi))−frac(w′(xj))◃ij′di,j′=di,j,
therefore frac(w′(xi))−δ−frac(w′(xj))+δ◃ijdi,j;
–
if xi∈LFPRp(D) and xj∈X∖LFPRp(D):
recall that after applying Algorithm 3,
Dj,0′=Dj,i+(1,≤), and D0,j′=Di,j+(−1,≤).
Observe that as we added ≤ which is the neutral element of the addition ⊕ between two operators ◃,
we have ◃j0′=◃ji and ◃0j′=◃ij.
Note that as xi∈LFPRp(D), in (E′,D′) we have D0,i′=(0,≤)=Di,0′
which means frac(w′(xi))=0.
Going backward in time of δ units of time from w′(xi)
means that frac(w(xi))=1−δ.
We have that
[TABLE]
hence frac(w′(xj))−1◃jiv(dj,i) which is equivalent to
[TABLE]
The same way we have
[TABLE]
hence 1−frac(w′(xj))◃ijv(di,j) which is equivalent to
[TABLE]
To conclude, we define for all xjs.t.D0,j′=(0,≤) and Dj,0′=(0,≤)
Let v∈Rp.
Consider (E′,D′)=TE((E,D)) respecting condition Definition 3.5 (5b), i. e.,
suppose there is at least an xis.t.Di,0′=(1,<)
and for all js.t.D0,j=(0,◃0j), then we have ◃0j=<.
Let w′∈(E′,v(D′)).
We need to find a value δs.t.w′−δ∈(E,v(D))
which is equivalent to prove for all xi,xj
[TABLE]
and
[TABLE]
and
[TABLE]
As done previously we are going to define a δ which is different from [math] so we satisfy condition Definition 3.5 (5a),
and show that constraints in (E,D)
are satisfied while going backward of δ units of time from w′.
We define the largest and the least amount of time so that all upper bounds of (E,D) are satisfied.
Let
[TABLE]
and
[TABLE]
We want to prove that t0=t1>0.
For this purpose, let us first show that for all i,j
we have frac(w′(xj))−v(dj,0′)≤frac(w′(xi))+v(d0,i′),
which is t0≤t1.
First note that for all i,j
[TABLE]
By applying TE< (Algorithm 2)
to (E,D), we have that Dj,i′=Dj,i, i. e.,(di,j,◃ij)=(di,j′,◃ij′),
and from Definition 3.5 (4) we have that Dj,i≤Dj,0+D0,i is valid for Rp.
Hence, we have from Definition 3.3 (2b) that either v(dj,i)<v(dj,0)+v(d0,i) or
v(dj,i)≤v(dj,0)+v(d0,i) and ◃ji=◃j0⊕◃0i or ◃ji=< and ◃j0⊕◃0i=≤.
We can then write that
[TABLE]
which is equivalent to
[TABLE]
so we obtain our result, as (◃j0⊕◃0i) is either ≤ or <.
Now, recall that (E,D) respects condition Definition 3.5 (5a)
so we have at least an xs.t.Dx,0=D0,x=(0,≤).
For this clock x we have that frac(w′(x))=frac(w′(x))−v(dx,0)≤t0
and that t1≤frac(w′(x))+v(d0,x)=frac(w′(x)).
Hence t0=t1=frac(w′(x)).
As ◃x0=≤,
we have (◃x0⊕◃0i)=◃0i
and (◃j0⊕◃0x)=◃j0, which gives
[TABLE]
and
[TABLE]
Moreover in (E′,D′) we have that frac(w′(x))◃0x′v(d0,x′).
Since (E′,D′) respects condition Definition 3.5 (5b), if D0,x′=(0,◃0x′) then
◃0x′=<.
Hence 0<frac(w′(x)) and
[TABLE]
Let δ=t0=t1.
More intuitively δ is the value right in the middle of the least and the largest amount of time
s.t. we can go backward in time from w′ and respect all constraints defined in (E,v(D)).
First we have
[TABLE]
which is −v(d0,j)◃j0frac(w′(xj))−δ.
Secondary we have
[TABLE]
which is frac(w′(xj))−δ◃0jv(dj,0).
Now we prove that constraints defined in (E,D) on differences of clocks are also satisfied
by going back of δ units of time from w′
Recall that in (E′,D′) from the definition of Algorithm 2
we have for all clocks xi,xj,
[TABLE]
Since we already treated the case whether i or j are [math], now suppose i,j are both different from [math].
We have that frac(w′(xj))−frac(w′(xi))◃ji′v(dj,i′)=v(dj,i),
and therefore as ◃ji′=◃ji,
[TABLE]
We also have that frac(w′(xi))−frac(w′(xj))◃ij′v(di,j′)=v(di,j),
therefore as ◃ij′=◃ij,
Suppose in (E,D) there is at least an xis.t.Di,0=(1,<)
and for all js.t.D0,j=(0,◃), we have ◃=<.
Let xi be such a clock and v∈Rp.
Now consider (E′,D′)=TE((E,D)).
We need to find a value δs.t.w+δ∈(E′,v(D′)).
which is equivalent to prove for all xi,xj
[TABLE]
and
[TABLE]
and
[TABLE]
As done previously we are going to define a δ which is different from [math],
and show that constraints in (E,D)
are satisfied while going forward of δ units of time from w.
Recall that xi∈LFPRp(D) and let δ=1−frac(w(xi))
which we will prove is the exact amount of time so that all upper bounds of (E′,D′) are satisfied.
Let
[TABLE]
and
[TABLE]
Recall that since (E,D) respects condition Definition 3.5 (5b),
for all js.t.D0,j=(0,◃0j), we have ◃0j=<.
Hence as −frac(w(xi))<v(d0,j), frac(w(xi))=0.
Using the same reasoning as before, we are going to prove that t0≤δ≤t1.
First we will prove that t0≤δ.
Consider xi∈LFPRp(D). For all clock xj, since w∈(E,v(D))
we have frac(w(xi))−frac(w(xj))◃ijfrac(v(di,j)).
From Algorithm 3
applied to (E,D) and since xi∈LFPRp(D) we obtain in (E′,D′) that D0,j′=Di,j+(−1,≤).
Clearly we have ◃0j′=◃ij⊕≤=◃ij.
It gives that
[TABLE]
which is equivalent to
frac(w(xi))−frac(w(xj))−1◃0j′frac(v(d0,j′))
which is equivalent to
[TABLE]
This gives us our first result.
Second we will prove that δ≤t1.
Consider xi∈LFPRp(D). For all clock xj, from Definition 3.5 (4)
we have frac(w(xj))−frac(w(xi))◃jifrac(v(dj,i)).
We have
[TABLE]
From Algorithm 3
applied to (E,D) and since xi∈LFPRp(D) we obtain in (E′,D′) that Dj,0′=Dj,i+(1,≤).
Clearly we have ◃j0′=◃ji⊕≤=◃ji.
Then we can write that
frac(w(xj))−frac(w(xi))+1◃j0′frac(v(dj,0′))
which is equivalent to
[TABLE]
This gives us our second result.
Now for all clock xj, we obtain two results.
First we have
[TABLE]
which is −v(d0,j′)◃0j′frac(w(xj))+δ.
Secondary we have
[TABLE]
which is frac(w(xj))+δ◃j0′v(dj,0′).
Since we already treated the case whether i or j are [math], now suppose i,j are both different from [math].
Note that if both xi,xj∈LFPRp(D), as frac(w(xi))=frac(w(xj)),
Di,j=Di,j′=(0,≤) and Dj,i=Dj,i′=(0,≤) from Definition 4.5.
Hence frac(w(xi))+δ−frac(w(xj))−δ◃ij′frac(v(di,j′))
and frac(w(xj))+δ−frac(w(xj))−δ◃ji′frac(v(dj,i′)).
The same way, if both xi,xj∈LFPRp(D) we have Di,j=Di,j′ and Dj,i=Dj,i′ and again our result.
If either xi or xj is in LFPRp(D), the case is similar to D0,j′ or Di,0′.
Suppose in (E,D) there is at least an xjs.t.Dj,0=D0,j=(0,≤)
Let v∈Rp, and xi∈LFPRp(D).
Now consider (E′,D′)=TE((E,D)).
We need to find a value δs.t.w+δ∈(E′,v(D′)).
which is equivalent to prove for all xi,xj
[TABLE]
and
[TABLE]
and
[TABLE]
As done previously we are going to define a δ which is different from [math],
and show that constraints in (E,D)
are satisfied while going forward of δ units of time from w.
Let
[TABLE]
and
[TABLE]
We want to prove that t0≤t1.
For this purpose, we are going to prove for all clocks i,j that
−frac(w(xj))−v(dj,0′)≤v(d0,i′)−frac(w(xi)).
First note that
[TABLE]
By definition of TE< applied to (E,D), we have that Dj,i′=Dj,i,
and from Definition 3.5 (4) we have that Dj,i′≤Dj,0′+D0,i′.
Hence, we have from Definition 3.3 (2b) that either dj,i′<dj,0′+d0,i′ or
dj,i′=dj,0′+d0,i′ and ◃ji′=◃j0′⊕◃0i′ or ◃ji′=< and ◃j0′⊕◃0i′=≤.
We can then write that
[TABLE]
which is equivalent to
[TABLE]
Now we prove that t0=0.
Clearly from Definition 3.5 for any clock i we have that
−frac(w(xi))◃0iv(d0,i) which is equivalent to
−frac(w(xi))−v(d0,i)◃0i0.
Hence if as (E,D) there is at least an xjs.t.Dj,0=D0,j=(0,≤), for this clock j
we have −frac(w(xj))−v(d0,j)=0.
By definition of TE< applied to (E,D), we have that D0,i′=D0,i+(0,<).
In order to respect the constraint −frac(w(xi))−δ◃0i′v(d0,i′)
which is, as ◃0i′=<, −frac(w(xi))−δ<v(d0,i′)
and especially for j where v(d0,j′)=0 we have to find a δ>0.
In order to find an upper bound for δ, we are going to prove that t1>0.
From Definition 3.5 (4) we have in (E,D) that for any clocks i,jDj,0≤Dj,i+Di,0. Let xi∈LFPRp(D).
From Definition 3.5 (1), we have that Di,0≤(1,<).
This gives that Dj,i+Di,0≤Dj,i+(1,<).
By definition of TE< applied to (E,D), we have that Dj,0′=Dj,i+(1,<).
Hence we have Dj,0≤Dj,0′.
Now as frac(w(xi))◃i0v(di,0)
we can write frac(w(xi))◃i0′v(di,0′)
and then 0◃i0′v(di,0′)−frac(w(xi))
where ◃i0′=<, which prove our result.
We define δ=2t1, therefore t0<δ<t1.
Now for all clock xj, we obtain two results.
First we have
[TABLE]
which is −v(d0,j′)◃0jfrac(w(xj))+δ as ◃0j′=<.
Secondary we have
[TABLE]
which is frac(w(xj))+δ◃j0v(dj,0′) as ◃0j′=<.
Now we prove that constraints defined in (E′,D′) on differences of clocks are also satisfied
by going forward of δ units of time from w
Recall that in (E′,D′) from the definition of Algorithm 2
we have for all clock xj,
[TABLE]
Since we already treated the case whether i or j are [math], now suppose i,j are both different from [math].
We have that frac(w(xj))−frac(w(xi))◃jiv(dj,i)=v(dj,i′),
and therefore as ◃ji′=◃ji,
[TABLE]
We also have that frac(w(xi))−frac(w(xj))◃ijv(di,j)=v(di,j′),
therefore as ◃ij′=◃ij,
[TABLE]
Finally, we define w′=w+δ and w′∈(E′,v(D′)).
Claim 3**.**
Let Rp be a parameter region and (E,D)∈p–PDBM⊙(Rp). Let v∈Rp.
There is w′∈TE((E,v(D)))
iff there is w∈(E,v(D)) and a delay δ s.t. w′=w+δ.
Proof H.4**.**
(⟸) for point–p–PDBMs
Let v∈Rp.
Consider (E′,D′)=TE((E,D)) respecting condition Definition 3.5 (5b), i. e.,
suppose there is at least an xi s.t. Di,0′=(1,<)
and for all j s.t. D0,j=(0,◃0j), then we have ◃0j=<.
Let w′∈(E′,v(D′)).
We need to find a value δ s.t. w′−δ∈(E,v(D))
which is equivalent to prove for all xi,xj
[TABLE]
and
[TABLE]
and
[TABLE]
As done previously we are going to define a δ which is different from [math],
and show that constraints in (E,D)
are satisfied while going backward of δ units of time from w′.
We define the largest and the least amount of time so that all upper bounds of (E,D) are satisfied.
Let
[TABLE]
and
[TABLE]
We want to prove that t0=t1>0.
For this purpose, let us first show that for all i,j
we have frac(w′(xj))−v(dj,0′)≤frac(w′(xi))+v(d0,i′),
which is t0≤t1.
First note that for all i,j
[TABLE]
By applying TE< (Algorithm 2)
to (E,D), we have that Dj,i′=Dj,i, i. e., (di,j,◃ij)=(di,j′,◃ij′),
and from Definition 3.6 (2) we have that Dj,i≤Dj,0+D0,i is valid for Rp.
Hence, we have from Definition 3.3 (2b) that either v(dj,i)<v(dj,0)+v(d0,i) or
v(dj,i)≤v(dj,0)+v(d0,i) and ◃ji=◃j0⊕◃0i or ◃ji=< and ◃j0⊕◃0i=≤.
We can then write that
[TABLE]
which is equivalent to
[TABLE]
so we obtain our result, as (◃j0⊕◃0i) is either ≤ or <.
Now, recall that in (E,D) for all x we have d0,x=−dx,0 and ◃0x=◃x0.
For any clock x we have that frac(w′(x))−v(dx,0)≤t0
and that t1≤frac(w′(x))+v(d0,x)=frac(w′(x))−v(dx,0).
Hence t0=t1.
As for all x, ◃x0=≤,
we have for all i,j that (◃x0⊕◃0i)=◃0i
and (◃j0⊕◃0x)=◃j0, which gives
[TABLE]
and
[TABLE]
Moreover in (E′,D′) we have that frac(w′(x))◃0x′v(d0,x′).
From Claim 1, (E′,D′) is obtained after applying Algorithm 2
and therefore ◃0x′=<.
Hence 0<frac(w′(x)) and
[TABLE]
Let δ=t0=t1.
More intuitively δ is the value right in the middle of the least and the largest amount of time
s.t. we can go backward in time from w′ and respect all constraints defined in (E,v(D)).
First we have
[TABLE]
which is −v(d0,j)◃j0frac(w′(xj))−δ.
Secondary we have
[TABLE]
which is frac(w′(xj))−δ◃0jv(dj,0).
Now we prove that constraints defined in (E,D) on differences of clocks are also satisfied
by going back of δ units of time from w′
Recall that in (E′,D′) from the definition of Algorithm 2
we have for all clocks xi,xj,
[TABLE]
Since we already treated the case whether i or j are [math], now suppose i,j are both different from [math].
We have that frac(w′(xj))−frac(w′(xi))◃ji′v(dj,i′)=v(dj,i),
and therefore as ◃ji′=◃ji,
[TABLE]
We also have that frac(w′(xi))−frac(w′(xj))◃ij′v(di,j′)=v(di,j),
therefore as ◃ij′=◃ij,
[TABLE]
To conclude, we define for all xj
[TABLE]
and clearly, w∈(E,v(D)).
(⟹) for point–p–PDBMs
Assume in (E,D)∈p–PDBM⊙(Rp).
Let v∈Rp, and xi∈LFPRp(D).
Now consider (E′,D′)=TE((E,D)).
We need to find a value δ s.t. w+δ∈(E′,v(D′)).
which is equivalent to prove for all xi,xj
[TABLE]
and
[TABLE]
and
[TABLE]
As done previously we are going to define a δ which is different from [math],
and show that constraints in (E,D)
are satisfied while going forward of δ units of time from w.
Let
[TABLE]
and
[TABLE]
We prove that t1≤t0.
for any clock i we have that Di,0=(frac(p),≤) and Di,0=(−frac(p),≤) i. e., d0,i=−di,0
for some p, hence −frac(w(xi))−v(d0,i)=−frac(w(xi))+v(di,0).
By definition of TE< applied to (E,D), we have that D0,i′=D0,i+(0,<).
In order to respect the constraint −frac(w(xi))−δ◃0i′v(d0,i′)
which is, as ◃0i′=<, −frac(w(xi))−δ<v(d0,i′),
we have to find a δ>0.
In order to find an upper bound for δ, we are going to prove that t1>0.
From Definition 3.6 (2) we have in (E,D) that for any clocks i,jDj,0≤Dj,i+Di,0. Let xi∈LFPRp(D).
From Definition 3.6 (1), we have that Di,0≤(1,<).
This gives that Dj,i+Di,0≤Dj,i+(1,<).
By definition of TE< applied to (E,D), we have that Dj,0′=Dj,i+(1,<).
Hence we have Dj,0≤Dj,0′.
Now as frac(w(xi))◃i0v(di,0)
we can write frac(w(xi))◃i0′v(di,0′)
and then 0◃i0′v(di,0′)−frac(w(xi))
where ◃i0′=<, which prove our result.
We define δ=2t1, therefore t0<δ<t1.
Now for all clock xj, we obtain two results.
First we have
[TABLE]
which is −v(d0,j′)◃0jfrac(w(xj))+δ as ◃0j′=<.
Secondary we have
[TABLE]
which is frac(w(xj))+δ◃j0v(dj,0′) as ◃0j′=<.
Now we prove that constraints defined in (E′,D′) on differences of clocks are also satisfied
by going forward of δ units of time from w
Recall that in (E′,D′) from the definition of Algorithm 2 we have for all clock xj,
[TABLE]
Since we already treated the case whether i or j are [math], now suppose i,j are both different from [math].
We have that frac(w(xj))−frac(w(xi))◃jiv(dj,i)=v(dj,i′),
and therefore as ◃ji′=◃ji,
[TABLE]
We also have that frac(w(xi))−frac(w(xj))◃ijv(di,j)=v(di,j′),
therefore as ◃ij′=◃ij,
Lemma 4.12** (recalled).**
*
Let (E,D) be a p–PDBM for Rp and v∈Rp.
Let g be a non-parametric guard.
If v∈guard∀(g,E,D), then for all v′∈Rp, v′∈guard∀(g,E,D).
*
Proof I.1**.**
Our idea is to define a clock region “larger” than our p–PDBM (following Definition 2.3) and show that, even for this (larger) clock region, either all clock valuations satisfy the guard—or none does.
Definition 1**.**
Let Rp be a parameter region, v∈Rp. Let (E,D) be a p–PDBM for Rp.
We define the clock region containing (E,v(D)), denoted by [(E,v(D))]Rc, as follows:
for all w∈[(E,v(D))]Rc, for all clocks xi,xj,
•
if Exi<K, ⌊w(xi)⌋=Exi,
else if Exi=∞, w(xi)≥K;
•
if (0,≤)<Di,j is valid for Rp and Exi<K,
frac(w(xj))<frac(w(xi));
•
if (0,≤)=Di,j is valid for Rp and Exi<K,
frac(w(xj))=frac(w(xi));
•
if Di,0=D0,i=(0,≤) and Exi<K,
frac(w(xi))=0;
•
if Di,0=(0,≤),D0,i=(0,≤) and Exi<K,
frac(w(xi))=0.
Claim 2**.**
Let (E,D) be a p–PDBM for Rp and v∈Rp.
We have (E,v(D))⊆[(E,v(D))]Rc.
Proof I.2**.**
Clock regions of Definition 2.3 define constraints on clocks of the form 0=frac(x),
0<frac(x)<1, 0=frac(x)−frac(y) and 0<frac(x)−frac(y)<1 for some x,y,
and ⌊x⌋=k for some integer k.
Let (E,D) be a p–PDBM for Rp and v∈Rp. It defines constraints
[TABLE]
Clearly, if w∈(E,v(D)) satisfies ⌊xi⌋=Ei then it satisfies the same constraint defined in [(E,v(D))]Rc.
Consider the constraints frac(xi)−frac(xj)◃i,jv(di,j) and frac(xj)−frac(xi)◃j,iv(dj,i).
•
Suppose i,j are both different from [math]. From Definition 3.5 (3) and Definition 3.6,
either di,j=dj,i and then ◃i,j=≤=◃j,i, then if di,j=dj,i=0 it satisfies the same constraint defined in [(E,v(D))]Rc,
or di,j and dj,i are different from [math], as they are elements of PLT which are strictly smaller than 1, it satisfies either 0<frac(xi)−frac(xj)<1
or 0=frac(xi)−frac(xj) in [(E,v(D))]Rc.
Finally if di,j=dj,i, then ◃i,j=<=◃j,i and it satisfies 0<frac(xi)−frac(xj)<1 in [(E,v(D))]Rc.
•
Suppose i is different from [math] and j=0.
From Definition 3.5 (3) and Definition 3.6,
either di,0=d0,i and then ◃i,0=≤=◃0,i, then if di,0=d0,i=0 it satisfies the same constraint defined in [(E,v(D))]Rc,
or di,0 and d0,i are different from [math], as they are elements of PLT which are strictly smaller than 1, it satisfies either 0<frac(xi)<1
or 0=frac(xi) in [(E,v(D))]Rc.
Finally if di,0=d0,i, then ◃i,0=<=◃0,i and it satisfies 0<frac(xi)<1 in [(E,v(D))]Rc.
•
The case j is different from [math] and i=0 is similar.
•
Suppose both i,j are [math], the constraint is not taken into account as we have no x0 in [(E,v(D))]Rc.
Finally, we have that if w∈(E,v(D)) then w∈[(E,v(D))]Rc.
Now we come back to the proof of the main lemma:
Let (E,D) be a p–PDBM for Rp and v∈Rp. It defines constraints
[TABLE]
Moreover, let g be a non-parametric guard. It defines constraints for a finite number of integer constants ki with i∈I⊆[1,H]
[TABLE]
The intersection between the two is given by the conjunction of those constraints.
We project this intersection on parameter variables (by elimination of clock variables) and we prove that the intersection does not create new constraints on parameters different from those we already have in (E,v(D)) (and therefore in Rp).
For some set of clocks I⊆[1,H] and i∈I,
suppose we have the constraints frac(xi)≤0 and −frac(xi)≤0 in g.
When eliminating xi in any constraint of the form frac(xi)−frac(xj)◃i,jv(di,j),
it is clear that we proceed on PLT to the operation (0,≤)+(di,j,◃i,j)=(0+di,j,≤⊕◃i,j)=(di,j,◃i,j).
The same way on any constraint of the form frac(xi)◃i,0v(di,0), eliminating xi
gives the constraint (0,≤)+(di,0,◃i,0)=(di,0,◃i,0).
Hence it does not create new inequalities not belonging to Rp.
Now suppose v∈guard∀(g,E,D). We have that all w∈(E,v(D)) satisfy g.
As no new constraints not in PLT have been created, all v′∈Rp respect the same constraints on their fractional part and integer part as v
and therefore, (E,v′(D)) is contained in the same clock region as (E,v(D)) is,
i. e.,[(E,v(D))]Rc=[(E,v′(D))]Rc.
Finally, v′∈guard∀(g,E,D).
Lemma 4.13** (recalled).**
*
Let (E,D) be a p–PDBM for Rp and v∈Rp.
Let g be a parametric guard.
If v∈p\mbox−guard∃(g,E,D), then for all v′∈Rp, v′∈p\mbox−guard∃(g,E,D).
*
Proof J.1**.**
Let (E,D) be a p–PDBM for Rp and v∈Rp.
Let g be a parametric guard and suppose v∈p\mbox−guard∃(g,E,D).
After applying a projection on parameters, we obtain constraints on elements of PLT.
By hypothesis, all these constraints are satisfied by v.
Suppose v′∈Rp.
By definition of our parameter regions, and since v and v′ both belong to Rp, v′ satisfies the same constraints on elements of PLT.
Therefore, the same constraints is satisfied by v′ and v′∈p\mbox−guard∃(g,E,D).
Proposition 6.1** (recalled).**
*
Let Rp be a parameter region. Let A be an R-U2P-PTA and R(A) its parametric region automaton over Rp.
There is a run σ:(ℓ0,(E0,D0))⟶e0(ℓ1,(E1,D1))⟶e1⋯(ℓf−1,(Ef−1,Df−1))⟶ef−1(ℓf,(Ef,Df))
in R(A) iff for all v∈Rp there is a run ρ:(ℓ0,w0)⟶e0(ℓ1,w1)⟶e1⋯(ℓf−1,wf−1)⟶ef−1(ℓf,wf)
in v(A)
s.t. for all 0≤i≤f, wi∈(Ei,v(Di)).
*
Proof K.1**.**
⇐
By induction on the length of the run.
Let v∈Rp.
As the basis for the induction, in the initial location (ℓ0,{0}H) the only valuation is reachable by an empty run of v(A).
Moreover {0}H∈(E0,v(D0)) the initial p–PDBM containing only [math].
Therefore the initial location
(ℓ0,(E0,v(D0))) is reachable by an empty run of R(A).
For the induction step, suppose for all v, there is run in v(A) of length f−1 we have our result.
Let v∈Rp and ρ=(ℓ0,w0)⟶e0⋯⟶ef−2(ℓf−1,wf−1)⟶ef−1(ℓf,wf) be a run of v(A) of length f.
By induction hypothesis, there is a run σ=(ℓ0,(E0,D0))⟶e0⋯⟶ef−2(ℓf−1,(Ef−1,Df−1)) in R(A) and for all 0≤i≤f−1, wi∈(Ei,v(Di)).
Consider ef−1. By Definition 5.1 of the parametric region automaton, it is also in its set of edges ζ′.
Three cases show up:
–
If ef−1=⟨ℓf−1,a,g,unp,ℓf⟩ contains no parametric guard nor parametric update.
Using Definition 2.2 there is a delay δ (possibly [math]) s.t.(ℓf−1,wf−1)↦δ(ℓf−1wf−1′)↦ef−1(ℓf,wf) where wf−1′⊨g and wf=[wf−1′]unp.
As wf−1∈(Ef−1,v(Df−1)) there is (Ef−1′,Df−1′)∈Succ((Ef−1,Df−1))s.t. from Proposition 4.11 we have wf−1′∈(Ef−1′,v(Df−1′)).
As wf−1′⊨g by construction of our p–PDBMs (see Section 4.4) any other clock valuation belonging to (Ef−1′,v(Df−1′)) satisfies g.
Therefore v∈guard∀(g,Ef−1′,Df−1′) and from Lemma 4.12, Rp⊆guard∀(g,Ef−1′,Df−1′).
Now, as wf=[wf−1′]unp consider the open–p–PDBM (Ef,Df)=update((Ef−1′,Df−1′),unp);
from Lemma 4.4 we have wf∈(Ef,v(Df)).
Finally there is an edge
[TABLE]
–
If ef−1=⟨ℓf−1,a,g,u,ℓf⟩ contains a parametric guard and a parametric update.
Using Definition 2.2 there is a delay δ (possibly [math]) s.t.(ℓf−1,wf−1)↦δ(ℓf−1,wf−1′)↦ef−1(ℓf,wf) where wf−1′⊨v(g) and wf=[wf−1′]v(u).
As wf−1∈(Ef−1,v(Df−1)) there is (Ef−1′,Df−1′)∈Succ((Ef−1,Df−1))s.t. from Proposition 4.11 we have wf−1′∈(Ef−1′,v(Df−1′)).
As wf−1′⊨v(g), v∈p\mbox−guard∃(g,Ef−1′,Df−1′) and from Lemma 4.13, Rp⊆p\mbox−guard∃(g,Ef−1′,Df−1′).
Now, as wf=[wf−1′]v(u) consider the point–p–PDBM (Ef,Df)=update((Ef−1′,Df−1′),u);
(Ef,v(Df)) contains only one clock valuation, precisely defined by the fully parametric update v(u) so we have wf∈(Ef,v(Df)).
Finally there is an edge (ℓf−1,(Ef−1,Df−1))⟶ef−1(ℓf,(Ef,Df)).
–
The case where ef−1 contains a non parametric guard and a parametric update is similar to the previous one.
Finally, there is a run σ′=σ⟶ef−1(ℓf,(Ef,Df)) of length f in R(A)s.t. for all 0≤i≤f, wi∈(Ei,v(Di)).
⇒
By induction on the length of the run.
Let v∈Rp.
As the basis for the induction, the initial location (ℓ0,(E0,v(D0))) is reachable by an empty run of R(A).
Moreover, as {0}H∈(E0,v(D0)), the initial location
(ℓ0,{0}H) is reachable by an empty run of v(A).
For the induction step, suppose it is true for all run in R(A) of length f−1.
Let v∈Rp and σ=(ℓ0,(E0,D0))⟶e0⋯⟶ef−2(ℓf−1,(Ef−1,Df−1))⟶ef−1(ℓf,(Ef,Df)) be a run of R(A) of length f.
Consider ef−1. By Definition 5.1 of the parametric region automaton, it is also in the set of edges ζ of A.
Two cases show up:
–
If ef−1=⟨ℓf−1,a,g,unp,ℓf⟩ contains no parametric guard nor parametric update.
By induction hypothesis, there is a run ρ=(ℓ0,w0)⟶e0⋯⟶ef−2(ℓf−1,wf−1) of v(A) of length f−1s.t. for all 0≤i≤f−1, wi∈(Ei,v(Di)).
Using Definition 5.1 there is (Ef−1′,Df−1′)∈Succ((Ef−1,Df−1)),
Rp⊆guard∀(g,Ef−1′,Df−1′) and
(Ef,Df)=update((Ef−1′,Df−1′),unp).
From Proposition 4.11 we have wf−1′∈(Ef−1′,v(Df−1′)) and a delay δs.t.wf−1′=wf−1+δ.
As Rp⊆guard∀(g,Ef−1′,Df−1′)
from Lemma 4.12 we have v∈guard∀(g,Ef−1′,Df−1′) and wf−1′⊨g.
Moreover, since (Ef,Df)=update((Ef−1′,Df−1′),unp), we define wf=[wf−1′]unp
and therefore from Lemma 4.4, wf∈(Ef,v(Df)).
Finally there is an edge (ℓf−1,wf−1)⟶ef−1(ℓf,wf) and a run ρ′=ρ⟶ef−1(ℓf,wf) in v(A) of length fs.t. for all 0≤i≤f, wi∈(Ei,v(Di)).
–
If ef−1=⟨ℓf−1,a,g,u,ℓf⟩ contains a parametric guard and a parametric update.
Using Definition 5.1 there is (Ef−1′,Df−1′)∈Succ((Ef−1,Df−1)),
Rp⊆p\mbox−guard∃(g,Ef−1′,Df−1′) and
(Ef,Df)=update((Ef−1′,Df−1′),u).
From Lemma 4.13 we can take wf−1′∈(Ef−1′,v(Df−1′))s.t.wf−1′⊨v(g).
Let wf=[wf−1′]v(u).
Clearly, (Ef,Df)=update((Ef−1′,Df−1′),u) is a point–p–PDBM;
as (Ef,v(Df)) contains only one clock valuation precisely defined by the fully parametric update v(u), we have wf∈(Ef,v(Df)).
From Proposition 4.11 as wf−1′∈(Ef−1′,v(Df−1′)) there is a delay δ and a wf−1∈(Ef−1,v(Df−1))s.t.wf−1′=wf−1+δ.
Using the induction hypothesis, there is a run
ρ=(ℓ0,w0)⟶e0⋯⟶ef−2(ℓf−1,wf−1) of v(A) of length f−1s.t. for all 0≤i≤f−1, wi∈(Ei,v(Di)).
Finally there is an edge (ℓf−1,wf−1)⟶ef−1(ℓf,wf)
and a run ρ′=ρ⟶ef−1(ℓf,wf) in v(A) of length fs.t. for all 0≤i≤f, wi∈(Ei,v(Di)).
–
The case where ef−1 contains a non parametric guard and a parametric update is similar to the previous one.
Bibliography30
The reference list from the paper itself. Each links out to its DOI / PubMed record.
1[AD 94] Rajeev Alur and David L. Dill. A theory of timed automata. Theoretical Computer Science , 126(2):183–235, April 1994.
2[AFKS 12] Étienne André, Laurent Fribourg, Ulrich Kühne, and Romain Soulat. IMITATOR 2.5: A tool for analyzing robustness in scheduling problems. In Dimitra Giannakopoulou and Dominique Méry, editors, FM , volume 7436 of Lecture Notes in Computer Science , pages 33–36. Springer, August 2012.
3[AHV 93] Rajeev Alur, Thomas A. Henzinger, and Moshe Y. Vardi. Parametric real-time reasoning. In S. Rao Kosaraju, David S. Johnson, and Alok Aggarwal, editors, STOC , pages 592–601, New York, NY, USA, 1993. ACM.
4[AL 17] Étienne André and Didier Lime. Liveness in L/U-parametric timed automata. In Alex Legay and Klaus Schneider, editors, ACSD , pages 9–18. IEEE, 2017.
5[ALM 20] Étienne André, Didier Lime, and Nicolas Markey. Language preservation problems in parametric timed automata. Logical Methods in Computer Science , 16, January 2020.
6[ALR 16] Étienne André, Didier Lime, and Olivier H. Roux. Decision problems for parametric timed automata. In Kazuhiro Ogata, Mark Lawford, and Shaoying Liu, editors, ICFEM , volume 10009 of Lecture Notes in Computer Science , pages 400–416. Springer, 2016.
7[ALR 18] Étienne André, Didier Lime, and Mathias Ramparison. Timed automata with parametric updates. In Gabriel Juhás, Thomas Chatain, and Radu Grosu, editors, ACSD , pages 21–29. IEEE, 2018.
8[ALR 19] Étienne André, Didier Lime, and Mathias Ramparison. Parametric updates in parametric timed automata. In Jorge A. Pérez and Nobuko Yoshida, editors, FORTE , volume 11535 of Lecture Notes in Computer Science , pages 39–56. Springer, 2019.
