Thus, a feasible error trace in M × P is an evidence to M P , since it indicates the existence of a run that
violates P .
Example 2. Consider the program M of Figure 3 and the property P of Figure 2. As we discussed in
Section 1, M P . The trace t = read ?x pw , 999 < x pw , (enc!x pw , enc?y pw ), x pw == y pw , y pw :=
2 · y pw , (getEnc?x pw2 , getEnc!y pw ), x pw2 == y pw , x pw ! = x pw2 , y pw ≥ 2
64 is a feasible error trace in
M × P proving that an overflow is possible.
4 The Assume-Guarantee-Repair (AGR) Framework
In this section we discuss our Assume-Guarantee-Repair (AGR) framework for communicating programs.
The framework consists of a learning-based Assume-Guarantee algorithm, called AG L ∗ , and a REPAIR
procedure, which are tightly joined.
Let M 1 and M 2 be two programs, and let P be a property. The classical Assume-Guarantee (AG)
proof rule [26] assures that if we find an assumption A (in our case, a communicating program) such
that M 1 ||A P and M 2 A both hold, then M 1 ||M 2 P holds as well. For LTSs [9], the AG-rule is
guaranteed to either prove correctness or return a real (non-spurious) counterexample. The work in [9] relies
on the L
∗ algorithm [5] for learning an assumption A for the AG-rule. In particular, L
∗ aims at learning
A w , the weakest assumption for which M 1 ||A w P holds. A crucial point of this method is the fact that
A w is regular [15], and thus can be learned by L
∗ .
Lemma 1. For infinite-state communicating programs, the weakest assumption A w is not always regular.
Example 3. Consider the programs M 1 , M 2 and the property P of Figure 4. The weakest assumption with
which M 1 satisfies P should contain exactly all traces (over the alphabet of M 2 ) that contain equally many
actions of the form x := x + 1 and y := y + 1. This set of traces is not regular, and therefore cannot be
learned by L
∗ .
q0
q1
sync
true
p0
p1
p2
p3
x:=0
y:=0
x:=x+1
y:=y+1
sync
true
r0
r1
r2
r3
sync x==y
true
x!=y
∗
M1
M2
P
Fig. 4: A system for which the weakest assumption is not regular
To cope with this difficulty, we change the target of learning. Instead of learning the (possibly) nonregular language of A w , we learn T (M 2 ), the set of accepted traces of M 2 . This language is guaranteed to
be regular, as it is represented by the automaton M 2 .
Note that in case that M 1 ||M 2 P , repair is never needed, and M 2 is a valid assumption. In the worst
case, the procedure halts once it has learned M 2 . In particular, in case there are no error traces, termination
of our algorithm is guaranteed. If M 1 ||M 2 P then there does not exist a matching assumption, and
attempting to learn M 2 will reveal this. Therefore, using T (M 2 ) as a learning goal matches the AG rule.
Assume, Guarantee or Repair
219
violates P .
Example 2. Consider the program M of Figure 3 and the property P of Figure 2. As we discussed in
Section 1, M P . The trace t = read ?x pw , 999 < x pw , (enc!x pw , enc?y pw ), x pw == y pw , y pw :=
2 · y pw , (getEnc?x pw2 , getEnc!y pw ), x pw2 == y pw , x pw ! = x pw2 , y pw ≥ 2
64 is a feasible error trace in
M × P proving that an overflow is possible.
4 The Assume-Guarantee-Repair (AGR) Framework
In this section we discuss our Assume-Guarantee-Repair (AGR) framework for communicating programs.
The framework consists of a learning-based Assume-Guarantee algorithm, called AG L ∗ , and a REPAIR
procedure, which are tightly joined.
Let M 1 and M 2 be two programs, and let P be a property. The classical Assume-Guarantee (AG)
proof rule [26] assures that if we find an assumption A (in our case, a communicating program) such
that M 1 ||A P and M 2 A both hold, then M 1 ||M 2 P holds as well. For LTSs [9], the AG-rule is
guaranteed to either prove correctness or return a real (non-spurious) counterexample. The work in [9] relies
on the L
∗ algorithm [5] for learning an assumption A for the AG-rule. In particular, L
∗ aims at learning
A w , the weakest assumption for which M 1 ||A w P holds. A crucial point of this method is the fact that
A w is regular [15], and thus can be learned by L
∗ .
Lemma 1. For infinite-state communicating programs, the weakest assumption A w is not always regular.
Example 3. Consider the programs M 1 , M 2 and the property P of Figure 4. The weakest assumption with
which M 1 satisfies P should contain exactly all traces (over the alphabet of M 2 ) that contain equally many
actions of the form x := x + 1 and y := y + 1. This set of traces is not regular, and therefore cannot be
learned by L
∗ .
q0
q1
sync
true
p0
p1
p2
p3
x:=0
y:=0
x:=x+1
y:=y+1
sync
true
r0
r1
r2
r3
sync x==y
true
x!=y
∗
M1
M2
P
Fig. 4: A system for which the weakest assumption is not regular
To cope with this difficulty, we change the target of learning. Instead of learning the (possibly) nonregular language of A w , we learn T (M 2 ), the set of accepted traces of M 2 . This language is guaranteed to
be regular, as it is represented by the automaton M 2 .
Note that in case that M 1 ||M 2 P , repair is never needed, and M 2 is a valid assumption. In the worst
case, the procedure halts once it has learned M 2 . In particular, in case there are no error traces, termination
of our algorithm is guaranteed. If M 1 ||M 2 P then there does not exist a matching assumption, and
attempting to learn M 2 will reveal this. Therefore, using T (M 2 ) as a learning goal matches the AG rule.
Assume, Guarantee or Repair
219