160
A. Cimatti et al.
Verification and Synthesis Problems The core problem we address is to check if
a given specification S = {C 1 , . . . , C n } is compatible, i.e., if Comp S holds. The
consistency checking problem amounts to checking if there exists a time point in
which the final phase of all the local requirements is reached, that is it amounts
to checking if the following formula holds:
∃t 1 . . . ∃t n Reach((C 1 , |C 1 |, t 1 ), . . . , (C n , |C n |, t n ))
If this is the case, then we say that S is consistent. Finally, we can formalize the
synthesis problem as the problem of computing (a symbolic representation of)
the set: {S
| Comp S ∧ S
S}
2.1 NP-hardness
In this section, we show that the simplest of the problems defined above is
already NP-hard. In fact, we show a reduction from SAT to the consistency
checking problem.
Let ϕ(¯ x) be a Boolean formula over the variables ¯
x = x 1 . . . x n ; without loss of generality, we assume ϕ(¯ x) to be in negated normal form, i.e., with
all the negations only in front of literals. For all 1 ≤ i ≤ n, we define the
local requirement corresponding to variable x i as C i = P
i
1 , P
i
2 , such that
B P i
2
= [0, +∞) and φ P i
1
= ψ P i
1
= φ P i
2
= ψ P i
2
= ; the idea is to encode
the values ⊥ and of each x i with the two phases P
i
1 and P
i
2 , respectively.
Moreover, we define the local requirement G, which will be useful as a gadget
for the reduction, as follows: G = P
G
1 , P
G
2 , where P
G
2 = [0, +∞), ϕ[x i →
C i , P
i
2 , ¬x i → →C i , P
i
1 ], . The specification S
ϕ corresponding to the Boolean
formula ϕ(¯ x) is defined as S
ϕ = {G, C 1 , . . . , C n }. It holds that ϕ(¯ x) is satisfiable if and only if S
ϕ is consistent. In fact, if S
ϕ is consistent, then there
exists a time point in which the signal dependency of the second phase of G
has been satisfied, and thus ϕ(¯ x) is satisfiable. Viceversa, let’s suppose that
ϕ(¯ x) is satisfiable and let M be an arbitrary model of it, expressed as the
set of true atoms, in which we also substitute every x i in it with the pair
C i , P
i
2 . Since the local requirements C 1 . . . C n have no dependencies and, together with G, have only infinite bounds, there exists a time t such that predicate
Reach((G, P
G
1 , t), (C 1 , P
G
b1 , t 1 ), . . . , (C n , P
n
bn , t n )) is true, where for all 1 ≤ i ≤ n,
b i = 2 and t i = 0 iff x i ∈ M and t i = t otherwise. By definition of Reach (see Definition 3), this implies that Reach((G, P
G
2 , t), (C 1 , P
1
2 , t), . . . , (C n , P
n
2 , t)) holds,
i.e., S is consistent.
In Sec. 3.2, we will give an encoding of the consistency checking problem
based on SMT(DL) (i.e., Satisfiability Modulo Theory of Difference Logic). In
particular, we will show that the problem can be reduced to the satisfiability
of a formula in SMT(DL). Since the latter belongs to NP [15], the consistency
checking problem belongs to NP as well, having that consistency checking is
NP-complete.
A. Cimatti et al.
Verification and Synthesis Problems The core problem we address is to check if
a given specification S = {C 1 , . . . , C n } is compatible, i.e., if Comp S holds. The
consistency checking problem amounts to checking if there exists a time point in
which the final phase of all the local requirements is reached, that is it amounts
to checking if the following formula holds:
∃t 1 . . . ∃t n Reach((C 1 , |C 1 |, t 1 ), . . . , (C n , |C n |, t n ))
If this is the case, then we say that S is consistent. Finally, we can formalize the
synthesis problem as the problem of computing (a symbolic representation of)
the set: {S
| Comp S ∧ S
S}
2.1 NP-hardness
In this section, we show that the simplest of the problems defined above is
already NP-hard. In fact, we show a reduction from SAT to the consistency
checking problem.
Let ϕ(¯ x) be a Boolean formula over the variables ¯
x = x 1 . . . x n ; without loss of generality, we assume ϕ(¯ x) to be in negated normal form, i.e., with
all the negations only in front of literals. For all 1 ≤ i ≤ n, we define the
local requirement corresponding to variable x i as C i = P
i
1 , P
i
2 , such that
B P i
2
= [0, +∞) and φ P i
1
= ψ P i
1
= φ P i
2
= ψ P i
2
= ; the idea is to encode
the values ⊥ and of each x i with the two phases P
i
1 and P
i
2 , respectively.
Moreover, we define the local requirement G, which will be useful as a gadget
for the reduction, as follows: G = P
G
1 , P
G
2 , where P
G
2 = [0, +∞), ϕ[x i →
C i , P
i
2 , ¬x i → →C i , P
i
1 ], . The specification S
ϕ corresponding to the Boolean
formula ϕ(¯ x) is defined as S
ϕ = {G, C 1 , . . . , C n }. It holds that ϕ(¯ x) is satisfiable if and only if S
ϕ is consistent. In fact, if S
ϕ is consistent, then there
exists a time point in which the signal dependency of the second phase of G
has been satisfied, and thus ϕ(¯ x) is satisfiable. Viceversa, let’s suppose that
ϕ(¯ x) is satisfiable and let M be an arbitrary model of it, expressed as the
set of true atoms, in which we also substitute every x i in it with the pair
C i , P
i
2 . Since the local requirements C 1 . . . C n have no dependencies and, together with G, have only infinite bounds, there exists a time t such that predicate
Reach((G, P
G
1 , t), (C 1 , P
G
b1 , t 1 ), . . . , (C n , P
n
bn , t n )) is true, where for all 1 ≤ i ≤ n,
b i = 2 and t i = 0 iff x i ∈ M and t i = t otherwise. By definition of Reach (see Definition 3), this implies that Reach((G, P
G
2 , t), (C 1 , P
1
2 , t), . . . , (C n , P
n
2 , t)) holds,
i.e., S is consistent.
In Sec. 3.2, we will give an encoding of the consistency checking problem
based on SMT(DL) (i.e., Satisfiability Modulo Theory of Difference Logic). In
particular, we will show that the problem can be reduced to the satisfiability
of a formula in SMT(DL). Since the latter belongs to NP [15], the consistency
checking problem belongs to NP as well, having that consistency checking is
NP-complete.