1. β 0 is an arbitrary valuation.
2. If a i = g?x, then β i (y) = β i−1 (y) for every y = x. Intuitively, x is arbitrarily assigned by the read
action, and the rest of the variables are unchanged.
3. If a i is an assignment x := e, then β i (x) = e[¯ x ← β i−1 (¯ x)] and β i (y) = β i−1 (y) for every y = x.
4. If a i = (g?x, g!y) or a i = (g!y, g?x) then β i (x) = β i−1 (y) and β i (z) = β i−1 (z) for every z = x.
That is, the effect of a synchronous communication on a channel is that of an assignment.
5. If a i does not involve a read or an assignment, then β i = β i−1 .
6. Finally, if a i is a constraint in C, then β i (¯ x) a i (and since a i does not change the variable assignments, then β i−1 (¯ x) a i holds as well).
We say that t is feasible if there exists a run of t.
The symbolic language of M , denoted T (M ), is the set of all accepted traces induced by paths of M .
The concrete language of M is the set of all runs of accepted traces in T (M ). We will mostly be interested
in feasible traces, which represent (concrete) runs of the program. Intuitively, the symbolic language of a
program M corresponds to its syntactic behavior, while the concrete language corresponds to the semantics
of the program.
Example 1. – The trace (x := 2 · y, g?x, y := y +1, g!y) is feasible, as it has a run (x = 1, y = 3), (x =
6, y = 3), (x = 20, y = 3), (x = 20, y = 4), (x = 20, y = 4).
– The trace (g?x, x := x
2 , x < 0) is not feasible since no β can satisfy the constraint x < 0 if x := x
2
is executed beforehand.
2.1 Parallel Composition
We now describe and define the parallel run of two communicating programs, and the way in which they
communicate.
Let M 1 and M 2 be two programs, where M i = Q i , X i , α i , δ i , q 0
i , F i for i ∈ {1, 2}. Let G 1 , G 2 be
the sets of communication channels occurring in actions of M 1 , M 2 , respectively. We assume X 1 ∩ X 2 = ∅.
The interface alphabet αI of M 1 and M 2 consists of all communication actions on channels that are
common to both components. That is, αI = { g?x, g!x | g ∈ G 1 ∩ G 2 , x ∈ X 1 ∪ X 2 }.
In parallel composition, the two components synchronize on their communication interface only when
one component writes data through a channel, and the other reads it through the same channel. The two components cannot synchronize if both are trying to read or both are trying to write. We distinguish between
communication of the two components with each other (on their common channels), and their communication with their environment. In the former case, the components must “wait” for each other in order to
progress together. In the latter case, the communication actions of the two components interleave asynchronously.
Formally, the parallel composition of M 1 and M 2 , denoted M 1 ||M 2 , is the program M = Q, x, α, δ, q 0 , F
defined as follows.
1. Q = (Q 1 × Q 2 ) ∪ (Q
1 × Q
2 ), where Q
1 and Q
2 are new copies of Q 1 and Q 2 , respectively. The initial
state is q 0 = (q
1
0 , q
2
0 ).
2. X = X 1 ∪ X 2 .
3. α = { (g?x 1 , g!x 2 ), (g!x 1 , g?x 2 ) | g∗x 1 ∈ (α 1 ∩αI) and g∗x 2 ∈ (α 2 ∩αI)}∪((α 1 ∪α 2 )\αI). That is,
the alphabet includes pairs of read-write communication actions on channels common to M 1 and M 2 .
It also includes individual actions of M 1 and M 2 – assignment actions, constraints and communication
actions which are not communications on common channels.
216
H. Frenkel et al.
2. If a i = g?x, then β i (y) = β i−1 (y) for every y = x. Intuitively, x is arbitrarily assigned by the read
action, and the rest of the variables are unchanged.
3. If a i is an assignment x := e, then β i (x) = e[¯ x ← β i−1 (¯ x)] and β i (y) = β i−1 (y) for every y = x.
4. If a i = (g?x, g!y) or a i = (g!y, g?x) then β i (x) = β i−1 (y) and β i (z) = β i−1 (z) for every z = x.
That is, the effect of a synchronous communication on a channel is that of an assignment.
5. If a i does not involve a read or an assignment, then β i = β i−1 .
6. Finally, if a i is a constraint in C, then β i (¯ x) a i (and since a i does not change the variable assignments, then β i−1 (¯ x) a i holds as well).
We say that t is feasible if there exists a run of t.
The symbolic language of M , denoted T (M ), is the set of all accepted traces induced by paths of M .
The concrete language of M is the set of all runs of accepted traces in T (M ). We will mostly be interested
in feasible traces, which represent (concrete) runs of the program. Intuitively, the symbolic language of a
program M corresponds to its syntactic behavior, while the concrete language corresponds to the semantics
of the program.
Example 1. – The trace (x := 2 · y, g?x, y := y +1, g!y) is feasible, as it has a run (x = 1, y = 3), (x =
6, y = 3), (x = 20, y = 3), (x = 20, y = 4), (x = 20, y = 4).
– The trace (g?x, x := x
2 , x < 0) is not feasible since no β can satisfy the constraint x < 0 if x := x
2
is executed beforehand.
2.1 Parallel Composition
We now describe and define the parallel run of two communicating programs, and the way in which they
communicate.
Let M 1 and M 2 be two programs, where M i = Q i , X i , α i , δ i , q 0
i , F i for i ∈ {1, 2}. Let G 1 , G 2 be
the sets of communication channels occurring in actions of M 1 , M 2 , respectively. We assume X 1 ∩ X 2 = ∅.
The interface alphabet αI of M 1 and M 2 consists of all communication actions on channels that are
common to both components. That is, αI = { g?x, g!x | g ∈ G 1 ∩ G 2 , x ∈ X 1 ∪ X 2 }.
In parallel composition, the two components synchronize on their communication interface only when
one component writes data through a channel, and the other reads it through the same channel. The two components cannot synchronize if both are trying to read or both are trying to write. We distinguish between
communication of the two components with each other (on their common channels), and their communication with their environment. In the former case, the components must “wait” for each other in order to
progress together. In the latter case, the communication actions of the two components interleave asynchronously.
Formally, the parallel composition of M 1 and M 2 , denoted M 1 ||M 2 , is the program M = Q, x, α, δ, q 0 , F
defined as follows.
1. Q = (Q 1 × Q 2 ) ∪ (Q
1 × Q
2 ), where Q
1 and Q
2 are new copies of Q 1 and Q 2 , respectively. The initial
state is q 0 = (q
1
0 , q
2
0 ).
2. X = X 1 ∪ X 2 .
3. α = { (g?x 1 , g!x 2 ), (g!x 1 , g?x 2 ) | g∗x 1 ∈ (α 1 ∩αI) and g∗x 2 ∈ (α 2 ∩αI)}∪((α 1 ∪α 2 )\αI). That is,
the alphabet includes pairs of read-write communication actions on channels common to M 1 and M 2 .
It also includes individual actions of M 1 and M 2 – assignment actions, constraints and communication
actions which are not communications on common channels.
216
H. Frenkel et al.