Safe Decomposition of Startup Requirements
161
3 Verification
3.1 Reduction to Model Checking
In order to formalize the two verification problems into ones of model checking
networks of timed automata, we use timed automata with shared variables. To
this end, besides the clock constraints Ξ(C), we define L = {l A , l B , . . . } as a
set of location variables (one for each automaton A in the network), and Θ(L)
as the set of all Boolean combinations of atoms of type l A = v A , where A is a
timed automata, l A ∈ L and v A is a state of A.
Definition 5 (Timed Automata with Shared Variables) A timed automaton with shared variables (TASV, for short) A = V A , v
0
A , l A , C A , inv
cl
A , inv
loc
A , T A
consists of:
– a finite set of locations V A ;
– an initial location v
0
A ∈ V A ;
– a location variable l A with range V A ;
– a finite set of clocks C A , where a clock is a real-valued variable;
– a clock invariant inv
cl
A : V A → Ξ(C A ) for each location;
– a location invariant inv
loc
A : V A → Θ(C A ) for each location;
– a transition relation T A ⊆ V A × 2
C A × Ξ(C A ) × Θ(L) × V A .
Given a set of clocks C, we denote with ν : C → R a clock valuation, that is
a function assigning a rational value to each clock; with V C , we denote the set of
all possible clock valuations over C. For t ∈ R, ν + t is the clock valuation which
maps every clock c ∈ C to the value ν(c) + t. For R ⊆ C, we define ν[R → 0]
to be the valuation that maps x to 0 if x ∈ R, and to ν(x) otherwise. When
defining the product of two TASVs, we will deal with tuples (l A1 , . . . , l An ) of
location variables; in this context, we usually denote with λ any function from
the set of n-tuples of location variables to the set V A1 × · · · × V An . Moreover,
we write that λ |= Φ (where Φ ∈ Θ(L)) iff Φ[l Ai → v Ai , for all 1 ≤ i ≤ n] is
true and λ((. . . , l Ai , . . . )) = (. . . , v Ai , . . . ). We give the semantics of a TASV in
terms of traces and we define their product as described below.
Definition 6 (Trace of a TASV) A trace τ of a TASV A = V A , v
0
A , l A , C A ,
inv
cl
A , inv
loc
A , T A is a (either finite or infinite) sequence of states of the form:
v 0 , ν 0 , λ 0
α1
−→ →v 1 , ν 1 , λ 1
α2
−→ →v 2 , ν 2 , λ 2
α3
−→ . . .
such that v i ∈ V A , α i ∈ R ∪ {τ }, ν i ∈ V C A and λ i ∈ V L for all i ≥ 0, and:
– (initiation) v 0 = v
0
A , ν 0 (x) = 0 for all x ∈ C A , ν 0 |= inv
cl
A (v
0
A ), λ 0 (l A ) = v 0
and λ 0 |= inv
loc
A (v
0
A );
– (consecution): for all i ≥ 0
• (timed transition) if α ∈ R, then v i+1 = v i and ν i+1 = ν i + α, ν i + δ |=
inv
cl
A (v i ), for all 0 ≤ δ ≤ α, and λ i+1 (l A ) = v i ;
161
3 Verification
3.1 Reduction to Model Checking
In order to formalize the two verification problems into ones of model checking
networks of timed automata, we use timed automata with shared variables. To
this end, besides the clock constraints Ξ(C), we define L = {l A , l B , . . . } as a
set of location variables (one for each automaton A in the network), and Θ(L)
as the set of all Boolean combinations of atoms of type l A = v A , where A is a
timed automata, l A ∈ L and v A is a state of A.
Definition 5 (Timed Automata with Shared Variables) A timed automaton with shared variables (TASV, for short) A = V A , v
0
A , l A , C A , inv
cl
A , inv
loc
A , T A
consists of:
– a finite set of locations V A ;
– an initial location v
0
A ∈ V A ;
– a location variable l A with range V A ;
– a finite set of clocks C A , where a clock is a real-valued variable;
– a clock invariant inv
cl
A : V A → Ξ(C A ) for each location;
– a location invariant inv
loc
A : V A → Θ(C A ) for each location;
– a transition relation T A ⊆ V A × 2
C A × Ξ(C A ) × Θ(L) × V A .
Given a set of clocks C, we denote with ν : C → R a clock valuation, that is
a function assigning a rational value to each clock; with V C , we denote the set of
all possible clock valuations over C. For t ∈ R, ν + t is the clock valuation which
maps every clock c ∈ C to the value ν(c) + t. For R ⊆ C, we define ν[R → 0]
to be the valuation that maps x to 0 if x ∈ R, and to ν(x) otherwise. When
defining the product of two TASVs, we will deal with tuples (l A1 , . . . , l An ) of
location variables; in this context, we usually denote with λ any function from
the set of n-tuples of location variables to the set V A1 × · · · × V An . Moreover,
we write that λ |= Φ (where Φ ∈ Θ(L)) iff Φ[l Ai → v Ai , for all 1 ≤ i ≤ n] is
true and λ((. . . , l Ai , . . . )) = (. . . , v Ai , . . . ). We give the semantics of a TASV in
terms of traces and we define their product as described below.
Definition 6 (Trace of a TASV) A trace τ of a TASV A = V A , v
0
A , l A , C A ,
inv
cl
A , inv
loc
A , T A is a (either finite or infinite) sequence of states of the form:
v 0 , ν 0 , λ 0
α1
−→ →v 1 , ν 1 , λ 1
α2
−→ →v 2 , ν 2 , λ 2
α3
−→ . . .
such that v i ∈ V A , α i ∈ R ∪ {τ }, ν i ∈ V C A and λ i ∈ V L for all i ≥ 0, and:
– (initiation) v 0 = v
0
A , ν 0 (x) = 0 for all x ∈ C A , ν 0 |= inv
cl
A (v
0
A ), λ 0 (l A ) = v 0
and λ 0 |= inv
loc
A (v
0
A );
– (consecution): for all i ≥ 0
• (timed transition) if α ∈ R, then v i+1 = v i and ν i+1 = ν i + α, ν i + δ |=
inv
cl
A (v i ), for all 0 ≤ δ ≤ α, and λ i+1 (l A ) = v i ;