representation is similar in nature to that of a control-flow graph. Its advantage, however, is in the ability to
exploit an automata-learning algorithm such as L
∗ for its verification.
We first formally define the alphabet over which communicating programs are defined. Let G be a
finite set of communication channels. Let X be a finite set of variables (whose ordered vector is ¯
x) and D
be a (possibly infinite) data domain. For simplicity, we assume that all variables are defined over D. The
elements of D are also used as constants in arithmetic expressions and constraints.
Definition 1. An action alphabet is α = G ∪ E ∪ C where:
1. G ⊆ { g?x 1 , g!x 1 , (g?x 1 , g!x 2 ), (g!x 1 , g?x 2 ) |g ∈ G, x 1 , x 2 ∈ X} is a finite set of communication
actions. g?x is a read action of a value to the variable x through channel g, and g!x is a write action of
the value of x on channel g. We use g ∗ x to indicate some action, either read or write, through g. The
pairs (g?x 1 , g!x 2 ) and (g!x 1 , g?x 2 ) represent a synchronization of two programs on read-write actions
over channel g (defined later).
2. E ⊆ { x := e | e ∈ E, x ∈ X} is a finite set of assignment statements, where E is a set of expressions
over X ∪ D.
3. C is a finite set of constraints over X ∪ D.
Definition 2. A communicating program (or, a program) is M = Q, X, α, δ, q 0 , F , where:
1. Q is a finite set of states and q 0 ∈ Q is the initial state.
2. X is a finite set of variables that range over D.
3. α = G ∪ E ∪ C is the action alphabet of M .
4. δ ⊆ Q × α × Q is the transition relation, where for each q ∈ Q, only one of the following holds:
– α ∈ C for all (q, α, q
) ∈ δ
– α ∈ G ∪ E for all (q, α, q
) ∈ δ
That is, for each state it holds that either all outgoing edges are labeled with constraints, or that all
outgoing edges are labeled with assignments or communication actions.
5. F ⊆ Q is the set of accepting states.
The words that are read along a communicating program are a symbolic representation of the program
behaviors. We refer to such a word as a trace. Each such trace induces concrete runs of the program, which
are formed by concrete assignments to the program variables in a way that conforms with the actions along
the word.
We now formally define these notions.
Definition 3. A path in a program M is a finite sequence of states and actions p = (q 0 , a 1 ,
q 1 , . . . , a n , q n ), starting with the initial state q 0 , such that ∀0 ≤ i < n we have (q i , a i+1 , q i+1 ) ∈ δ. The
induced trace of p is the sequence t = (a 1 , . . . , a n ) of the actions in p. If q n is accepting, then t is an
accepted trace of M .
From now on we assume that every trace we discuss is induced by some path. We turn to define the
concrete runs of the program.
Definition 4. Let t = (a 1 , . . . , a n ) be a trace and let (β 0 , . . . , β n ) be a sequence of valuations (i.e., assignments to the program variables)
4 . Then a sequence r = (β 0 , a 1 , β 1 , a 2 , . . . , a n , β n ) is a run of t if the
following holds.
4 Such valuations are usually referred to as states. We do not use this terminology here in order not to confuse them
with the states of the automaton.
Assume, Guarantee or Repair
215
exploit an automata-learning algorithm such as L
∗ for its verification.
We first formally define the alphabet over which communicating programs are defined. Let G be a
finite set of communication channels. Let X be a finite set of variables (whose ordered vector is ¯
x) and D
be a (possibly infinite) data domain. For simplicity, we assume that all variables are defined over D. The
elements of D are also used as constants in arithmetic expressions and constraints.
Definition 1. An action alphabet is α = G ∪ E ∪ C where:
1. G ⊆ { g?x 1 , g!x 1 , (g?x 1 , g!x 2 ), (g!x 1 , g?x 2 ) |g ∈ G, x 1 , x 2 ∈ X} is a finite set of communication
actions. g?x is a read action of a value to the variable x through channel g, and g!x is a write action of
the value of x on channel g. We use g ∗ x to indicate some action, either read or write, through g. The
pairs (g?x 1 , g!x 2 ) and (g!x 1 , g?x 2 ) represent a synchronization of two programs on read-write actions
over channel g (defined later).
2. E ⊆ { x := e | e ∈ E, x ∈ X} is a finite set of assignment statements, where E is a set of expressions
over X ∪ D.
3. C is a finite set of constraints over X ∪ D.
Definition 2. A communicating program (or, a program) is M = Q, X, α, δ, q 0 , F , where:
1. Q is a finite set of states and q 0 ∈ Q is the initial state.
2. X is a finite set of variables that range over D.
3. α = G ∪ E ∪ C is the action alphabet of M .
4. δ ⊆ Q × α × Q is the transition relation, where for each q ∈ Q, only one of the following holds:
– α ∈ C for all (q, α, q
) ∈ δ
– α ∈ G ∪ E for all (q, α, q
) ∈ δ
That is, for each state it holds that either all outgoing edges are labeled with constraints, or that all
outgoing edges are labeled with assignments or communication actions.
5. F ⊆ Q is the set of accepting states.
The words that are read along a communicating program are a symbolic representation of the program
behaviors. We refer to such a word as a trace. Each such trace induces concrete runs of the program, which
are formed by concrete assignments to the program variables in a way that conforms with the actions along
the word.
We now formally define these notions.
Definition 3. A path in a program M is a finite sequence of states and actions p = (q 0 , a 1 ,
q 1 , . . . , a n , q n ), starting with the initial state q 0 , such that ∀0 ≤ i < n we have (q i , a i+1 , q i+1 ) ∈ δ. The
induced trace of p is the sequence t = (a 1 , . . . , a n ) of the actions in p. If q n is accepting, then t is an
accepted trace of M .
From now on we assume that every trace we discuss is induced by some path. We turn to define the
concrete runs of the program.
Definition 4. Let t = (a 1 , . . . , a n ) be a trace and let (β 0 , . . . , β n ) be a sequence of valuations (i.e., assignments to the program variables)
4 . Then a sequence r = (β 0 , a 1 , β 1 , a 2 , . . . , a n , β n ) is a run of t if the
following holds.
4 Such valuations are usually referred to as states. We do not use this terminology here in order not to confuse them
with the states of the automaton.
Assume, Guarantee or Repair
215