166
A. Cimatti et al.
where:
WEAKVIOL(t
c
i ) := ¬φ
c
i [(d, j) → (r
d
j ∧ t
d
j ≤ t
c
i < t
d
j+1 )] ∨
¬ψ
c
i [(d, j) → (r
d
j ∧ t
d
j ≤ t
c
i )] ∨
¬ψ
c
i−1 [(d, j) → (r
d
j ∧ t
c
i ≤ t
d
j+1 )])
(9)
We can prove that W
ill and
W ill
fin are equisatisfiable for every set of local requirements with only finite bounds and convex dependencies. Notably, there are
no quantifiers in W
ill
fin : as said before, this makes the encoding dramatically more
efficient with respect to W: in Sec. 5, we will consider only local requirements of
this type. The details of the proofs are reported in the extended version of the
paper in which, given that the proofs are a bit involved, we proceed incrementally, showing first how we can remove upfront the quantifiers in case of finite
bounds with strict semantics, then in the case with weak semantics and finally
in case of convex dependencies.
4 Synthesis
In this section, we tackle the synthesis problem, i.e., computing the set of all
stronger local requirements (as defined in Def. 2) of the initial local requirements
such that their composition is compatible. We solve this problem by reducing it
to a parameter synthesis problem (see [9] for a more detailed description); given
a local requirement C, its corresponding parametric local requirement C, π is
defined as C (see Sec. 2), except that the bounds l P and u P of each phase P are
now the parameters ¯ l P and ¯
u P , respectively, and π := { ¯ l P | P is a phase of C} ∪
{¯ u P | P is a phase of C}. Given a set of local requirements S = {C 1 , . . . , C n },
we write S, Π for its parametric version {{C 1 , π 1 , . . . , C n , π n }, where the set
of parameters is defined as Π :=
n
i=1 π i . A parameter valuation γ : Π → Q
assigns a rational value to each parameter; moreover, for each 1 ≤ i ≤ n, it
also induces a (concrete) local requirement C i , γ(π i ), obtained from C i , π i
by replacing every parameter p ∈ π i with the concrete value γ(p). In the same
way, we can define the concrete version S, γ(π) of S, π. γ is said to be feasible
for S if C i , γ(π i ) is a stronger local requirement of C i , for all 1 ≤ i ≤ n, and
S, γ(π) is compatible. A feasible region is a set R := {γ | γ is feasible for S}.
Also in this case, we can either use parameter synthesis algorithms over timed
automata [3] or reduce the problem to SMT(LRA); we focus on the latter and in
particular, we will synthesize a symbolic representation of the region R, namely
an SMT formula ϕ R with the following property: γ |= ϕ R iff γ ∈ R, for each
valuation γ.
Let W ill be the encoding equal to W
ill except that each number l
c
i (resp. u
c
i )
is replaced with the variable ¯ l
c
i (resp. ¯
u
c
i ) and each phase is required to have
finite bounds. We define the sets of variables R := {r
c
i | c ∈ S, i is a phase of c}
and S := {s
c
i | c ∈ S, i is a phase of c}: these are the variables we are going to
remove by means of quantifier elimination. Finally, we define:
A. Cimatti et al.
where:
WEAKVIOL(t
c
i ) := ¬φ
c
i [(d, j) → (r
d
j ∧ t
d
j ≤ t
c
i < t
d
j+1 )] ∨
¬ψ
c
i [(d, j) → (r
d
j ∧ t
d
j ≤ t
c
i )] ∨
¬ψ
c
i−1 [(d, j) → (r
d
j ∧ t
c
i ≤ t
d
j+1 )])
(9)
We can prove that W
ill and
W ill
fin are equisatisfiable for every set of local requirements with only finite bounds and convex dependencies. Notably, there are
no quantifiers in W
ill
fin : as said before, this makes the encoding dramatically more
efficient with respect to W: in Sec. 5, we will consider only local requirements of
this type. The details of the proofs are reported in the extended version of the
paper in which, given that the proofs are a bit involved, we proceed incrementally, showing first how we can remove upfront the quantifiers in case of finite
bounds with strict semantics, then in the case with weak semantics and finally
in case of convex dependencies.
4 Synthesis
In this section, we tackle the synthesis problem, i.e., computing the set of all
stronger local requirements (as defined in Def. 2) of the initial local requirements
such that their composition is compatible. We solve this problem by reducing it
to a parameter synthesis problem (see [9] for a more detailed description); given
a local requirement C, its corresponding parametric local requirement C, π is
defined as C (see Sec. 2), except that the bounds l P and u P of each phase P are
now the parameters ¯ l P and ¯
u P , respectively, and π := { ¯ l P | P is a phase of C} ∪
{¯ u P | P is a phase of C}. Given a set of local requirements S = {C 1 , . . . , C n },
we write S, Π for its parametric version {{C 1 , π 1 , . . . , C n , π n }, where the set
of parameters is defined as Π :=
n
i=1 π i . A parameter valuation γ : Π → Q
assigns a rational value to each parameter; moreover, for each 1 ≤ i ≤ n, it
also induces a (concrete) local requirement C i , γ(π i ), obtained from C i , π i
by replacing every parameter p ∈ π i with the concrete value γ(p). In the same
way, we can define the concrete version S, γ(π) of S, π. γ is said to be feasible
for S if C i , γ(π i ) is a stronger local requirement of C i , for all 1 ≤ i ≤ n, and
S, γ(π) is compatible. A feasible region is a set R := {γ | γ is feasible for S}.
Also in this case, we can either use parameter synthesis algorithms over timed
automata [3] or reduce the problem to SMT(LRA); we focus on the latter and in
particular, we will synthesize a symbolic representation of the region R, namely
an SMT formula ϕ R with the following property: γ |= ϕ R iff γ ∈ R, for each
valuation γ.
Let W ill be the encoding equal to W
ill except that each number l
c
i (resp. u
c
i )
is replaced with the variable ¯ l
c
i (resp. ¯
u
c
i ) and each phase is required to have
finite bounds. We define the sets of variables R := {r
c
i | c ∈ S, i is a phase of c}
and S := {s
c
i | c ∈ S, i is a phase of c}: these are the variables we are going to
remove by means of quantifier elimination. Finally, we define: