2. If (q, c 1 , q
) and (q, c 2 , q
) are in δ for constraints c 1 , c 2 ∈ C and q
= q
, then c 1 ∧ c 2 ≡ false.
3. Let C q be the set of all constraints on transitions leaving q. Then (
c∈Cq c) ≡ true .
A property is a deterministic and complete program with no assignment actions.
A trace is accepted by a property P if it reaches a state in F , the set of accepting states of P . Otherwise,
it reaches a state in Q \ F , and is rejected by P .
Next, we define the satisfaction relation between a program and a property. Intuitively, a program M
satisfies a property P (denoted M P ) if all runs induced by accepted traces of M reach an accepting state
in P .
A property P specifies the behavior of a program M by referring to communication actions of M and
imposing constraints over the variables of M . Thus, the set of variables of P is identical to that of M . Let
G be the set of communication actions of M . Then, αP includes a subset of G as well as constraints over
the variables of M . The interface of M and P , which consists of the communication actions that occur in
P , is defined as αI = G ∩ αP .
In order to capture the satisfaction relation between M and P , we define a conjunctive composition
between M and P , denoted M × P . In conjunctive composition, the two components synchronize on their
common communication actions when both read or both write through the same communication channel.
They interleave on constraints and on actions of αM that are not in αP .
Definition 6. Let M = Q M , X M , αM, δ M , q
M
0 , F M be a program and P = Q P , X P , αP, δ P , q
P
0 , F P
be a property, where X M = X P . The conjunctive composition of M and P is M ×P = Q, X, α, δ, q 0 , F ,
where:
1. Q = Q M × Q P . The initial state is q 0 = (q
M
0 , q
P
0 ).
2. X = X M = X P .
3. α = { g!x, g?x, (g?x, g!y), (g!x, g?y) | g ∗ x, (g ∗ x, g ∗ y) ∈ αI} ∪ ((αM ∪ αP ) \ αI))
6 . That is, the
alphabet includes communication actions on channels common to M and P . It also includes individual
actions of M and P .
4. δ is defined as follows.
(a) For a = (g ∗ x, g ∗ y) ∈ αI, or a = g ∗ x ∈ αI: δ((q 1 , q 2 ), a) = (δ M (q 1 , a), δ P (q 2 , a)).
(b) For a ∈ αM \ αI: δ((q 1 , q 2 ), a) = (δ M (q 1 , a), q 2 ).
(c) For a ∈ αP \ αI: δ((q 1 , q 2 ), a) = (q 1 , δ P (q 2 , a)).
That is, on actions that are not common communication actions to M and P , the two components
interleave.
5. F = F M × B P , where B P = Q P \ F P .
Note that accepted traces in M ×P are those that are accepted in M and rejected in P . Such traces are called
error traces and their corresponding runs are called error runs. Intuitively, an error run is a run along M
which violates the properties modeled by P . Such a run either fails to synchronize on the communication
actions, or reaches a point in the computation in which its assignments, coming from M , violate some
constraint described by P . These runs are manifested in the traces that are accepted in M but are composed
with matching traces that are rejected in P . We can now formally define when a program satisfies a property.
Definition 7. For a program M and a property P , we define M P iff M × P contains no feasible
accepted traces.
6 Note that communication actions of the form (g ∗ x, g ∗ y) can only appear if M is a parallel composition of two
programs.
218
H. Frenkel et al.
) and (q, c 2 , q
) are in δ for constraints c 1 , c 2 ∈ C and q
= q
, then c 1 ∧ c 2 ≡ false.
3. Let C q be the set of all constraints on transitions leaving q. Then (
c∈Cq c) ≡ true .
A property is a deterministic and complete program with no assignment actions.
A trace is accepted by a property P if it reaches a state in F , the set of accepting states of P . Otherwise,
it reaches a state in Q \ F , and is rejected by P .
Next, we define the satisfaction relation between a program and a property. Intuitively, a program M
satisfies a property P (denoted M P ) if all runs induced by accepted traces of M reach an accepting state
in P .
A property P specifies the behavior of a program M by referring to communication actions of M and
imposing constraints over the variables of M . Thus, the set of variables of P is identical to that of M . Let
G be the set of communication actions of M . Then, αP includes a subset of G as well as constraints over
the variables of M . The interface of M and P , which consists of the communication actions that occur in
P , is defined as αI = G ∩ αP .
In order to capture the satisfaction relation between M and P , we define a conjunctive composition
between M and P , denoted M × P . In conjunctive composition, the two components synchronize on their
common communication actions when both read or both write through the same communication channel.
They interleave on constraints and on actions of αM that are not in αP .
Definition 6. Let M = Q M , X M , αM, δ M , q
M
0 , F M be a program and P = Q P , X P , αP, δ P , q
P
0 , F P
be a property, where X M = X P . The conjunctive composition of M and P is M ×P = Q, X, α, δ, q 0 , F ,
where:
1. Q = Q M × Q P . The initial state is q 0 = (q
M
0 , q
P
0 ).
2. X = X M = X P .
3. α = { g!x, g?x, (g?x, g!y), (g!x, g?y) | g ∗ x, (g ∗ x, g ∗ y) ∈ αI} ∪ ((αM ∪ αP ) \ αI))
6 . That is, the
alphabet includes communication actions on channels common to M and P . It also includes individual
actions of M and P .
4. δ is defined as follows.
(a) For a = (g ∗ x, g ∗ y) ∈ αI, or a = g ∗ x ∈ αI: δ((q 1 , q 2 ), a) = (δ M (q 1 , a), δ P (q 2 , a)).
(b) For a ∈ αM \ αI: δ((q 1 , q 2 ), a) = (δ M (q 1 , a), q 2 ).
(c) For a ∈ αP \ αI: δ((q 1 , q 2 ), a) = (q 1 , δ P (q 2 , a)).
That is, on actions that are not common communication actions to M and P , the two components
interleave.
5. F = F M × B P , where B P = Q P \ F P .
Note that accepted traces in M ×P are those that are accepted in M and rejected in P . Such traces are called
error traces and their corresponding runs are called error runs. Intuitively, an error run is a run along M
which violates the properties modeled by P . Such a run either fails to synchronize on the communication
actions, or reaches a point in the computation in which its assignments, coming from M , violate some
constraint described by P . These runs are manifested in the traces that are accepted in M but are composed
with matching traces that are rejected in P . We can now formally define when a program satisfies a property.
Definition 7. For a program M and a property P , we define M P iff M × P contains no feasible
accepted traces.
6 Note that communication actions of the form (g ∗ x, g ∗ y) can only appear if M is a parallel composition of two
programs.
218
H. Frenkel et al.