4. δ is defined as follows.
(a) For (g ∗ x 1 , g ∗ x 2 ) ∈ α:
i. δ((q 1 , q 2 ), (g ∗ x 1 , g ∗ x 2 )) = (q
1 , q
2 ).
ii. δ((q
1 , q
2 ), x 1 == x 2 ) = (δ 1 (q 1 , g ∗ x 1 ), δ 2 (q 2 , g ∗ x 2 )).
That is, when a communication is performed synchronously in both components, the data is transformed through the channel from the writing component to the reading component. As a result, the
values of x 1 and x 2 equalize. This is enforced in M by adding a transition labeled by the constraint
x 1 == x 2 that immediately follows the synchronous communication.
(b) For a ∈ α 1 \ αI we define δ((q 1 , q 2 ), a) = (δ 1 (q 1 , a), q 2 ).
(c) For a ∈ α 2 \ αI we define δ((q 1 , q 2 ), a) = (q 1 , δ 2 (q 2 , a)).
That is, on actions that are not in the interface alphabet, the two components interleave.
5. F = F 1 × F 2
Figure 3 demonstrates the parallel composition of components M 1 and M 2 of Figures 1 and 2. The
program M = M 1 ||M 2 reads a password from the environment through channel read . The two components
synchronize on channels enc and getEnc.
(q0,p0 )
(q1,p0 )
(q2,p0 )
(q3,p0 )
(q4,p1 )
(q4,p2 )
(q
3 ,p
0 )
(q
4 ,p
2 )
read ?xpw
xpw ≤999
read ?xpw
999
(enc!xpw ,
enc?ypw )
xpw ==ypw
(getEnc?xpw2,
getEnc!ypw )
xpw2==ypw
Fig. 3: Parallel composition M = M 1 ||M 2 of components M 1 and M 2 from Figures 1, 2
3 Regular Properties and Their Satisfaction
In this section we define the syntax and semantics of the properties that we consider. These are properties
that can be represented as finite automata, hence the name regular. However, the alphabet of such automata
includes communication actions and first-order constraints over program variables. Thus, such automata are
suitable for specifying the desired and undesired behaviors of communicating programs over time.
In order to define our properties, we first need the notion of a deterministic and complete program. The
definition is somewhat different from the standard definition for finite automata, since it takes the semantic
meaning of constraints into account.
Intuitively, in a deterministic and complete program, every concrete run has exactly one trace that induces it.
Definition 5. A program over alphabet α is deterministic and complete if for every state q and for every
action a ∈ α the following hold:
1. There is exactly one state q
such that (q, a, q
) is in δ.
5
5 in our examples we sometimes omit the actions that lead to a rejecting sink for the sake of clarity.
Assume, Guarantee or Repair
217
(a) For (g ∗ x 1 , g ∗ x 2 ) ∈ α:
i. δ((q 1 , q 2 ), (g ∗ x 1 , g ∗ x 2 )) = (q
1 , q
2 ).
ii. δ((q
1 , q
2 ), x 1 == x 2 ) = (δ 1 (q 1 , g ∗ x 1 ), δ 2 (q 2 , g ∗ x 2 )).
That is, when a communication is performed synchronously in both components, the data is transformed through the channel from the writing component to the reading component. As a result, the
values of x 1 and x 2 equalize. This is enforced in M by adding a transition labeled by the constraint
x 1 == x 2 that immediately follows the synchronous communication.
(b) For a ∈ α 1 \ αI we define δ((q 1 , q 2 ), a) = (δ 1 (q 1 , a), q 2 ).
(c) For a ∈ α 2 \ αI we define δ((q 1 , q 2 ), a) = (q 1 , δ 2 (q 2 , a)).
That is, on actions that are not in the interface alphabet, the two components interleave.
5. F = F 1 × F 2
Figure 3 demonstrates the parallel composition of components M 1 and M 2 of Figures 1 and 2. The
program M = M 1 ||M 2 reads a password from the environment through channel read . The two components
synchronize on channels enc and getEnc.
(q0,p0 )
(q1,p0 )
(q2,p0 )
(q3,p0 )
(q4,p1 )
(q4,p2 )
(q
3 ,p
0 )
(q
4 ,p
2 )
read ?xpw
xpw ≤999
read ?xpw
999
(enc!xpw ,
enc?ypw )
xpw ==ypw
(getEnc?xpw2,
getEnc!ypw )
xpw2==ypw
Fig. 3: Parallel composition M = M 1 ||M 2 of components M 1 and M 2 from Figures 1, 2
3 Regular Properties and Their Satisfaction
In this section we define the syntax and semantics of the properties that we consider. These are properties
that can be represented as finite automata, hence the name regular. However, the alphabet of such automata
includes communication actions and first-order constraints over program variables. Thus, such automata are
suitable for specifying the desired and undesired behaviors of communicating programs over time.
In order to define our properties, we first need the notion of a deterministic and complete program. The
definition is somewhat different from the standard definition for finite automata, since it takes the semantic
meaning of constraints into account.
Intuitively, in a deterministic and complete program, every concrete run has exactly one trace that induces it.
Definition 5. A program over alphabet α is deterministic and complete if for every state q and for every
action a ∈ α the following hold:
1. There is exactly one state q
such that (q, a, q
) is in δ.
5
5 in our examples we sometimes omit the actions that lead to a rejecting sink for the sake of clarity.
Assume, Guarantee or Repair
217