Learning to Prove Safety over Parameterised
Concurrent Systems
Yu-Fang Chen

Chih-Duo Hong

Anthony W. Lin

Philipp Rümmer

Academia Sinica

Oxford University

Oxford University

Uppsala University

Abstract—We revisit the classic problem of proving safety
over parameterised concurrent systems, i.e., an infinite familyof finite-state concurrent systems that are represented by somefinite (symbolic) means. An example of such an infinite family isa dining philosopher protocol with any number n of processes(n being the parameter that defines the infinite family). Regularmodel checking is a well-known generic framework for modellingparameterised concurrent systems, where an infinite set of
configurations (resp. transitions) is represented by a regular set(resp. regular transducer). Although verifying safety properties in
the regular model checking framework is undecidable in general,many sophisticated semi-algorithms have been developed in thepast fifteen years that can successfully prove safety in many
practical instances. In this paper, we propose a simple solution
to synthesise regular inductive invariants that makes use of
Angluin’s classic L∗ algorithm (and its variants). We provide atermination guarantee when the set of configurations reachable
from a given set of initial configurations is regular. We have tested
L∗ algorithm on standard (as well as new) examples in regularmodel checking including the dining philosopher protocol, thedining cryptographer protocol, and several mutual exclusion
protocols (e.g. Bakery, Burns, Szymanski, and German). Our
experiments show that, despite the simplicity of our solution, it
can perform at least as well as existing semi-algorithms.

I. I NTRODUCTION
Parameterised concurrent systems are infinite families offinite-state concurrent systems, parameterised by the number nof processes. There are numerous examples of parameterised
concurrent systems, including models of distributed algorithms
which are typically designed to handle an arbitrary number nof processes [32], [53]. Verification of such systems, then,amounts to proving that a desired property holds for all
permitted values of n. For example, proving that the safety
property holds for a dining philosopher protocol entails proving that the protocol with any given number n of philosophers(n ≥ 3) can never reach a state when two neighbouring
philosophers eat simultaneously. For each given value of n,verifying safety/liveness is decidable, albeit the exponential
state-space explosion in the parameter n. However, when theproperty has to hold for each value of n, the number ofsystem configurations a verification algorithm has to explore
is potentially infinite. Indeed, even safety checking is alreadyundecidable for parameterised concurrent systems [9], [12],[30]; see [13] for a comprehensive survey on the decidability
aspect of the parameterised verification problem.
Various sophisticated semi-algorithms for verifying parameterised concurrent systems are available. These semialgorithms typically rely on a symbolic framework for repre-

senting infinite sets of system configurations and transitions.
Regular model checking [42], [7], [14], [15], [6], [1], [22],[45], [65] is one well-known symbolic framework for modelling and verifying parameterised concurrent systems. In regular model checking, configurations are modelled using words
over a finite alphabet, sets of configurations are represented as
regular languages, and the transition relation is defined by aregular transducer. From the research programme of regularmodel checking, not only are regular languages/transducers
known to be highly expressive symbolic representations formodelling parameterised concurrent systems, they are alsoamenable to an automata-theoretic approach (due to many niceclosure properties of regular languages/transducers), whichhave often proven effective in verification.
In this paper, we revisit the classic problem of verifying safety in the regular model checking framework. Many
sophisticated semi-algorithms for dealing with this problem
have been developed in the literature using methods such as
abstraction [4], [5], [21], [20], widening [15], [23], acceleration [57], [42], [11], and learning [54], [55], [38], [63], [62].
One standard technique for proving safety for an infinite-statesystems is by exhibiting an inductive invariant Inv (i.e. a setof configurations that is closed under an application of thetransition relation) such that (i) Inv subsumes the set Init of
all initial configurations, but (ii) Inv does not intersect with theset Bad of unsafe configurations. In regular model checking,the sets Init and Bad are given as regular sets. For this reason,a natural method for proving safety in regular model checking
is to exhibit a regular inductive invariant satisfying (i) and(ii). The regular set Inv can be constructed as a “regular
proof” for safety since checking that a candidate regular set
Inv is a proof for safety is decidable. A few semi-algorithms
inspired by automata learning — some based on the passive
learning algorithms [38], [55], [2] and some others based on
active learning algorithms [55], [62]— have been proposed
to synthesise a regular inductive invariant in regular model
checking. Despite these semi-algorithms, not much attention
has been paid to applications of automata learning in regularmodel checking.
In this paper, we are interested in one basic researchquestion in regular model checking: can we effectively apply
the classic Angluin’s L∗ automata learning [8] (or variants[58], [44]) to learn a regular inductive invariant? Hitherto
this question, perhaps surprisingly, has no satisfactory answer
in the literature. A more careful consideration reveals at least

two problems. Firstly, membership queries (i.e. is a word w
reachable from Init?) may be asked by the L∗ algorithm,
which amounts to checking reachability in an infinite-statesystem, which is undecidable in general. This problem wasalready noted in [54], [55], [62], [63]. Secondly, a regularinductive invariant satisfying (i) and (ii) might not be unique,and so strictly speaking we are not dealing with a well-definedlearning problem. More precisely, consider the question ofwhat the teacher should answer when the learner asks whether
v is in the desired invariant, but v turns out not to be reachable
from Init? Discarding v might not be a good idea, since this
could force the learning algorithm to look for a minimal (inthe sense of set inclusion) inductive invariant, which might
not be regular. Similarly, let us consider what the teacher
should answer in the case when we found a pair (v, w) ofconfigurations such that (1) v is in the candidate Inv , (2)w∈/ Inv , and (3) there is a transition from v to w. In the ICElearning framework [35], [34], [54], the pair (v, w) is called an
implication counterexample. To satisfy the inductive invariant
constraint, the teacher may respond that w should be added toInv , or that v should be removed from Inv . Some works in theliterature have proposed using a three-valued logic/automaton(with “don’t know” as an answer) because of the teacher’s
incomplete information [37], [26].
a) Contribution: In this paper, we propose a simple andpractical solution to the problem of applying the classic L∗
automata learning algorithm and its variants to synthesise aregular inductive invariant in regular model checking. To deal
with the first problem mentioned in the previous paragraph,
we propose to restrict to length-preserving regular transducers.
In theory, length-preservation is not a restriction for safety
analysis, since it just implies that each instance of the considered parameterised system is operating on bounded memory ofsize n (but the parameter n is unbounded). Experience showsthat many practical examples in parameterised concurrent systems can be captured naturally in terms of length-preserving
systems, e.g., see [52], [7], [6], [42], [22], [57], [1]. The benefitof the restriction is that the problem of membership queries is
now decidable, since the set of configurations that may reach(be reachable from) any given configuration w is finite andcan be solved by a standard finite-state model checker. For
the second problem mentioned in the previous paragraph, we
propose that a strict teacher be employed in L∗ learning for
regular inductive invariants in regular model checking. A strict
teacher attempts to teach the learner the minimal inductive invariant (be it regular or not), but is satisfied when the candidate
answer posed by the learner is an inductive invariant satisfying(i) and (ii) without being minimal. [In this sense, perhaps amore appropriate term is a strict but generous teacher, whotries to let a student pass a final exam whenever possible.]
For this reason, when the learner asks whether w is in thedesired inductive invariant, the teacher will reply NO if w is
not reachable from Init. The same goes with an implication
counterexample (v, w) such that the teacher will say that an
unreachable v is not in the desired inductive invariant.
We have implemented the learning-based approach in a

prototype tool with an interface to the libalf library, which
includes the L∗ algorithm and its variants. Despite the simplicity of our solution, it (perhaps surprisingly) works extremely
well in practice, as our experiments suggest. We have taken
numerous standard examples from regular model checking,including cache coherence protocols (German’s Protocol), selfstabilising protocols (Israeli-Jalfon’s Protocol and Herman’s
Protocol), synchronisation protocols (Lehmann-Rabin’s Dining Philosopher Protocol), secure multi-party computation protocols (Dining Cryptographers Protocol [25]), and mutual exclusion protocols (Szymanski’s Protocol, Burn’s Protocol, Dijkstra’s Protocol, Lamport’s bakery algorithm, and ResourceAllocator Protocol). We show that L∗ algorithm can perform atleast as well as (and, in fact, often outperform) existing semialgorithms. We compared the performance of our algorithmwith well-known and established techniques such as SATbased learning [55], [54], [51], [52], abstract regular model
checking (ARMC), which is based on abstraction-refinement
using predicate abstractions and finite-length abstractions [20],[21], and T(O)RMC, which is based on extrapolation (awidening technique) [16]. Our experiments show that, despite
the simplicity of our solution, it can perform at least as well
as existing semi-algorithms.
b) Related Work: The work of Vardhan et al. [63], [62]applies L∗ learning to infinite-state systems and, amongst
other, regular model checking. The learning algorithm attempts
to learn an inductive invariant enriched with “distance” information, which is one way to make membership queries(i.e. reachability for general infinite-state systems) decidable.
This often makes the resulting set not regular, even if theset of reachable configurations is regular, in which case ouralgorithm is guaranteed to terminate (recall our algorithm isonly learning a regular invariant without distance information).
Conversely, when an inductive invariant enriched with distanceinformation is regular, so is the projection that omits the distance information. Unfortunately, neither their tool Lever [63],nor the models used in their experiments are available, sothat we cannot make a direct comparison to our approach.
A learning algorithm allowing incomplete information [37]has been applied in [55] for inferring inductive invariantsof regular model checking. Although the learning algorithmin [37] uses the same data structure as the standard L∗
algorithm, it is essentially a SAT-based learning algorithm (itstermination is not guaranteed by the Myhill-Nerode theorem).
Despite our results that SAT-based learning seems to be lessefficient than L∗ learning for synthesising regular inductive
invariants in regular model checking, SAT-based learning
is more general and more easily applicable when verifying
other properties, e.g., liveness [52], fair termination [48], andsafety games [56]. View abstraction [5] is a novel techniquefor parameterised verification. Comparing to parameterised
verification based on view abstraction, our framework (i.e.
general regular model checking framework with transducers)
provides a more expressive modelling language that is requiredin specifying protocols with near-neighbour communication(e.g. Dining Cryptographers and Dining Philosophers).

2

When preparing the final version, we found that a very
similar algorithm had already appeared in Vardhan’s thesis [61,Section 6] from 2006; in particular, including the trick tomake a membership query (i.e. point-to-point reachability)
decidable by bounding the space of the transducers. The
research presented here was conducted independently, andconsiders several aspects that were not yet present in [61],including experimental results on systems that are not countersystems (parameterised concurrent systems with topologies),and heuristics like the use of shortest counterexamples andcaching. We cannot compare our implementation in detail withthe one from [61], since the latter tool is not publicly available.
c) Organisation: The notations are defined in Section II.
A brief introduction to regular model checking and automata
learning is given in Section III and Section IV, respectively.
The learning-based algorithm is provided in Section V. The
result of the experiments is in Section VI.

III. R EGULAR MODEL CHECKING
Regular model checking (RMC) is a uniform framework formodelling and automatically analysing parameterised concurrent systems. In the paper, we focus on the regular model
checking framework for safety properties. Under the framework, each system configuration is represented as a word inΣ∗ . The sets of initial configurations and of bad configurations
are captured by regular languages over Σ. The transition
relation is captured by a regular and length-preserving relationon Σ∗ . We use a triple (I, T , B) to denote a regular model
checking problem, where I is an FA recognizing the setof initial configurations, T is a transducer representing thetransition relation, and B is an FA recognizing the set ofbad configurations. Then the regular model checking problem(I, T , B) asks if T ∗ (I) ∩ B = ∅. A standard way to proveT ∗ (I) ∩ B = ∅ is to find a proof based on a set V satisfying
the following three conditions: (1)I ⊆ V (i.e. all initialconfigurations are contained in V ), (2) V ∩ B = ∅ (i.e. V
does not contain bad configurations), (3) T (V ) ⊆ V (i.e.
V is inductive: applying T to any configuration in V does
not take it outside V ). We call the set V an inductive
invariant for the regular model checking problem (I, T , B). In
the framework of regular model checking, a standard method
for proving safety (e.g. see [55], [7]) is to find a regular
proof, i.e., an inductive invariant that can be captured by finite
automaton. Because regular languages are effectively closed
under Boolean operations and taking pre-/post-images w.r.t.
finite transducers, an algorithm for verifying whether a given
regular language is an inductive invariant can be obtained byusing language inclusion algorithms for FA [3], [19].

II. P RELIMINARIESa) General Notations: Let Σ be a finite set of symbols
called alphabet. A word over Σ is a finite sequence of symbols
of Σ. We use λ to represent an empty word. For a set I ⊆ Σ∗
and a relation T ⊆ Σ∗ × Σ∗ , we define T (I) to be the postimage of I under T , i.e., T (I) = {y | ∃x. x ∈ I ∧(x, y) ∈ T }.
Let id = {(x, x) | x ∈ Σ∗ } be the identity relation. We
define T n for all n ∈ N in the standard way by induction:
T 0 = id, and T k = T ◦T k−1 , where ◦ denotes the compositionof relations.
T ∗ denote the transitive closure of T , i.e.,
S∞ Let∗i
T = i=1 T . For any two sets A and B, we use A B todenote their symmetric difference, i.e., the set A \ B ∪ B \ A.
b) Finite Automata and Transducer: In this paper, automata/transducers are denoted in calligraphic fonts A, B, I, T
to represent automata/transducers, while the corresponding
languages/relations are denoted in roman fonts A, B, I, T .
A finite automaton (FA) is a tuple A = (Q, Σ, δ, q0 , F )where Q is a finite set of states, Σ is an alphabet, δ ⊆ Q ×
Σ × Q is a transition relation, q0 ∈ Q is the initial state,and F ⊆ Q is the set of final states. A run of A on a word
w = a1 a2 a3 · · · an is a sequence of states q0 , q1 , · · · , qn suchthat (qi , ai+1 , qi+1 ) ∈ δ. A run is accepting if the last stateqn ∈ F . A word is accepted by A if it has an accepting
run. The language of A, denoted by A, is the set of word
accepted by A. A language is regular if it can be recognised
by a finite automaton. A is a deterministic finite automaton(DFA) if |{q 0 | (q, a, q 0 ) ∈ δ}| ≤ 1 for each q ∈ Q and a ∈ Σ.
Let Σλ = Σ ∪ {λ}. A (finite) transducer is a tuple T =(Q, Σλ , δ, q0 , F ) where Q is a finite set of states, δ ⊆ Q ×
Σλ × Σλ × Q is a transition relation, q0 ∈ Q is the initialstate, and F ⊆ Q is the set of final states. We say that T islength-preserving if δ ⊆ Q × Σ × Σ × Q. We define relationδ ∗ ⊆ Q × Σ∗ × Σ∗ × Q as the smallest relation satisfying(1) (q, λ, λ, q) ∈ δ ∗ for any q ∈ Q and (2) (q1 , x, y, q2 ) ∈δ ∗ ∧ (q2 , a, b, q3 ) ∈ δ =⇒ (q1 , xa, yb, q3 ) ∈ δ ∗ . The relation
represented by T is the set {(x, y) | (q0 , x, y, q) ∈ δ ∗ ∧ q ∈F }. A relation is regular and length-preserving if it can be
represented by a length-preserving transducer.

Example 1 (Herman’s Protocol). Herman’s Protocol is a selfstabilising protocol for n processes (say with ids 0, . . . , n − 1)organised as a ring structure. A configuration in the Herman’s
Protocol is correct iff only one process has a token. The
protocol ensures that any system configuration where theprocesses collectively holding any odd number of tokens willalmost surely be recovered to a correct configuration. Moreconcretely, the protocol works iteratively. In each iteration,
the scheduler randomly chooses a process. If the process with
the number i is chosen by the scheduler, it will toss a coin
to decide whether to keep the token or pass the token to thenext process, i.e. the one with the number (i + 1)%n. If a
process holds two tokens in the same iteration, it will discard
both tokens. One safety property the protocol guarantees isthat every system configuration has at least one token.
The protocol and the corresponding safety property can bemodelled as a regular model checking problem (I, T , B). Eachprocess has two states; the symbol T denotes the state that theprocess has a token and N denotes the state that the process
does not have a token. The word NNTTNN denotes a system
configuration with six processes, where only the processes withnumbers 2 and 3 are in the state with tokens. The set of
initial configurations is I = N∗ T(N∗ TN∗ TN∗ )∗ , i.e., an odd
number of processes has tokens. The set of bad configuration is
B = N∗ , i.e., all tokens have disappeared. We use the regular3

Algorithm 1: The improved L∗ algorithm by Rivest andSchapire
Input: A teacher answers Mem(w) and Equ(A) about atarget regular language R and the initialobservation table (S, E, T ).
1 repeat2
while (S, E, T ) is not closed do
3
Find a pair (x, a) ∈ S × Σ such that∀y ∈ S : row E (xa) 6= row E (y). Extend S toS ∪ {xa} and update T using membership
queries accordingly;
4
Build a candidate DFA Ah = (S, Σ, δ, λ, F ), whereδ = {(s, a, s0 ) | s, s0 ∈ S ∧ row E (sa) = row E (s)},the empty string λ is the initial state, andF = {s | T (s) = > ∧ s ∈ S};
5
if Equ(Ah ) = (false, w), where w ∈ A R thenAnalyse w and add a suffix of w to E;
6 until Equ(Ah ) = true;
7 return Ah is the minimal DFA for R;

language E = ((T, T) + (N, N)) to denote the relation that aprocess is idle. The transition relation T can be specified as aunion of the following regular expressions: (1) E ∗ [Idle], (2)E ∗ (T, N)(T, N)E ∗ + (T, N)E ∗ (T, N) [Discard both tokens],and (3) E ∗ (T, N)(N, T)E ∗ + (N, T)E ∗ (T, N) [Pass the token].
IV. AUTOMATA L EARNING
Suppose R is a regular target language whose definition
is not directly accessible. Automata learning algorithms [8],[58], [44], [17] automatically infer a FA A recognising R. The
setting of an online learning algorithm assumes a teacher who
has access to R and can answer the following two queries:(1) Membership query Mem(w): is the word w a memberof R, i.e., w ∈ R? (2) Equivalence query Equ(A): is thelanguage of FA A equal to R, i.e., A = R? If not, it returns acounterexample w ∈ A R. The learning algorithm willthen construct a FA A such that A = R by interactingwith the teacher. Such an algorithm works iteratively: In each
iteration, it performs membership queries to get from theteacher information about R. Using the results of the queries, it
proceeds by constructing a candidate automaton Ah and makes
an equivalence query Equ(Ah ). If Ah = R, the algorithm
terminates with Ah as the resulting FA. Otherwise, the teacher
returns a word w distinguishing Ah from R. The learningalgorithm uses w to refine the candidate automaton of thenext iteration. In the last decade, automata learning algorithms
have been frequently applied to solve formal verification andsynthesis problems, c.f., [27], [24], [38], [37], [26], [31].
More concretely, below we explain the details of
the automata learning algorithm proposed by Rivest andSchapire [58] (RS), which is an improved version of the classic
L∗ learning algorithm by Angluin [8]. The foundation of thelearning algorithm is the Myhill-Nerode theorem, from which
one can infer that the states of the minimal DFA recognizing R
are isomorphic to the set of equivalence classes defined by thefollowing relations: x ≡R y iff ∀z ∈ Σ∗ : xz ∈ R ↔ yz ∈ R.
Informally, two strings x and y belong to the same state of theminimal DFA recognising R iff they cannot be distinguishedby any suffix z. In other words, if one can find a suffix z 0
such that xz 0 ∈ R and yz 0 ∈/ R or vice versa, then x and ybelong to different states of the minimal DFA.
The algorithm uses a data structure called observation table(S, E, T ) to find the equivalence classes correspond to ≡R ,where S is a set of strings denoting the set of identifiedstates, E is the set of suffixes to distinguish if two strings
belong to the same state of the minimal DFA, and T is amapping from (S ∪ (S · Σ)) · E to {>, ⊥}. The value ofT (w) = > iff w ∈ R. We use row E (x) = row E (y) as ashorthand for ∀z ∈ E : T (xz) = T (yz). That is, the strings x
and y cannot be identified as two different states using only
strings in the set E as the suffixes. Observe that x ≡R y
implies row E (x) = row E (y) for all E ⊆ Σ∗ . We say thatan observation table is closed iff ∀x ∈ S, a ∈ Σ : ∃y ∈ S :row E (xa) = row E (y). Informally, with a closed table, every
state can find its successors wrt. all symbols in Σ. Initially,
S = E = {λ}, and T (w) = Mem(w) for all w ∈ {λ} ∪ Σ.

The details of of the improved L∗ algorithm by Rivest
and Schapire can be found in Algorithm 1. Observe that, inthe algorithm, two strings x, y with x ≡R y will never besimultaneously contained in the set S. When the equivalence
query Equ(A) returns false together with a counterexamplew ∈ A R, the algorithm will perform a binary search overw using membership queries to find a suffix e of w and extend
E to E ∪{e}. The suffix e has the property that ∃x, y ∈ S, a ∈Σ : row E (xa) = row E (y) ∧ row E∪{e} (xa) 6= row E∪{e} (y),that is, add e to E will identify at least one more state. The
existence of such a suffix is guaranteed. We refer the readers
to [58] for the proof.
Proposition 1. [58] Algorithm 1 will find the minimal DFA R
for R using at most n equivalence queries and n(n + n|Σ|) +n log m membership queries, where n is the number of state of
R and m is the length of the longest counterexample returned
from the teacher.
Because each equivalence query with a false answer will
increase the size (number of states) of the candidate DFA byat least one and the size of the candidate DFA is bounded
by n according to the Myhill-Nerode theorem, the learningalgorithm uses at most n equivalence queries. The number ofmembership queries required to fill in the entire observationtable is bounded by n(n + n|Σ|). Since a binary searchis used to analyse the counterexample and the number ofcounterexample from the teacher is bounded by n, the numberof membership queries required is bounded by n log m.
We would like to introduce the other two important variantsof the L∗ learning algorithm. The algorithm proposed by
Kearns and Vazirani [44] (KV) uses a classification tree data
structure to replace the observation table data structure of theclassic L∗ algorithm. The algorithm of Kearns and Vazirani
has a similar query complexity to the one of Rivest and4Mem(w)
Learnerw ∈ T ∗ (I)?
yes or no
Equ(Ah )false, w

exist. Pathological cases where only non-regular inductive
invariant exist do not, however, seem to occur frequently inpractice, c.f., [21], [38], [20], [22], [60], [57], [50].
Answering a membership query on a word w, i.e., checking
whether w ∈ T ∗ (I), is the easy part: since T is lengthpreserving, we can construct an FA recognising Post |w| ={w0 | |w0 | = |w| ∧ w0 ∈ T ∗ (I)} and then check if
w ∈ Post |w| . In practice, Post |w| can be efficiently computed
and represented using BDDs and symbolic model checking.
For an equivalence query on a candidate FA Ah , we needto check if Ah can be used as an inductive invariant for the
regular model checking problem (I, T , B). More concretely,
we check the three conditions (1) I ⊆ Ah , (2) Ah ∩ B = ∅,and (3) T (Ah ) ⊆ Ah using Algorithm 2.

Teacher(1)I ⊆ Ah ?
(2)Ah ∩ B = ∅?
(3)T (Ah ) ⊆ Ah ?

(I, T , B) = true andan inductive
invariant Aor(I, T , B) = false anda word w ∈ T ∗ (I) ∩ B

Fig. 1. Overview: using automata learning to solve the regular model checking
problem (I, T , B). Recall that we use calligraphy font for automata/transducers and roman font for the corresponding languages/relations.

Schapire [58]; it uses at most n equivalence queries andn2 (n|Σ| + m) membership queries. However, the worst casebound of the number of membership queries is very loose. It
assumes the structure of the classification tree is linear, i.e.,each node has at most one child, which happens very rarely
in practice. In our experience, the algorithm of Kearns andVazirani usually requires a few more equivalence queries, witha significant lower number of membership queries comparing
to Rivest and Schapire when applied to verification problems.
The NL∗ algorithm [17] learns a non-deterministic finite
automaton instead of a deterministic one. More concretely,
it makes use of a canonical form of nondeterministic finite
automaton, named residual finite-state automaton (RFSA) toexpress the target regular language. In some examples, RFSA
can be exponentially more succinct than DFA recognising
the same languages. In the worst case, the NL∗ algorithm
uses O(n2 ) equivalence queries and O(m|Σ|n3 ) membership
queries to infer a canonical RFSA of the target language.
V. A LGORITHM

Algorithm 2: Answer equivalence query on candidate FA
Input: An FA Ah and an RMC problem (I, T , B)
1 if I 6⊆ Ah then2
Find a word w ∈ I \ Ah ;3
return (false, w) to the learner;
4 else if Ah ∩ B 6= ∅ then5
Find a word w ∈ Ah ∩ B;
6
if w ∈ T ∗ (I) then Output {cex = w,
(I, T , B) = false} and halt;
7
else return (false, w) to the learner;
8 else if T (Ah ) 6⊆ Ah then9
Find a pair of words (w, w0 ) ∈ T such that w ∈ Ah
but w0 ∈/ Ah ;
10
if w ∈ T ∗ (I) then return (false, w0 ) to the learner;
11
else return (false, w) to the learner;
12 else Output {inv = Ah , (I, T , B) = true} and halt;

We apply automata learning algorithms, including Angluin’sL∗ and its variants, to solve the regular model checking
problem (I, T , B). Those learning algorithms require a teacher
answering both equivalence and membership queries. Our
strategy is to design a “strict teacher” targeting the minimal
inductive invariant T ∗ (I). For a membership query on a word
w, the teacher checks if w ∈ T ∗ (I), which is decidable under
the assumption that T is length-preserving. For an equivalence
query on a candidate FA Ah , the teacher analyses if Ah canbe used as an inductive invariant in a proof of the problem(I, T , B). It performs one of the following actions dependingon the result of the analysis (Fig. 1):• Determine that Ah does not represent an inductive invariant, and return false together with an explanation w ∈ Σ∗
to the learner.
• Conclude that (I, T , B) = true, and terminate the learning process with an inductive invariant Ah as the proof.
• Conclude that (I, T , B) = false, and terminate thelearning with a word w ∈ T ∗ (I) ∩ B as an evidence.
Similar to the typical regular model checking approach, ourlearning-based technique tries to find a “regular proof”, whichamounts to finding an inductive invariant in the form of aregular language. Our approach is incomplete in general since
it could happen that there only non-regular inductive invariants

If the condition (1) is violated, i.e., I 6⊆ Ah , there is a wordw ∈ I \ Ah . Since I ⊆ T ∗ (I), the teacher can infer that w ∈T ∗ (I) \ Ah and return w as a positive counterexample to thelearner. A counterexample is positive if it represents a word in
the target language that was missing in the candidate language.
The definition negative counterexamples is symmetric.
If the condition (2) is violated, i.e., Ah ∩ B 6= ∅, there
is a word w ∈ Ah ∩ B. The teacher checks if w ∈ T ∗ (I)by constructing Post |w| and checking if w ∈ Post |w| . If
w 6∈ T ∗ (I), the teacher obtains that w ∈ Ah \ T ∗ (I) andreturns false together with w as a negative counterexample tothe learner. Otherwise, the teacher infers that w ∈ T ∗ (I) ∩ B
and outputs (I, T , B) = false with the word w as an evidence.
The case that the condition (3) is violated, i.e., T (Ah ) 6⊆
Ah , is more involved. There exists a pair of words (w, w0 ) ∈ Tsuch that w ∈ Ah ∧ w0 ∈/ Ah . The teacher will check if
w ∈ T ∗ (I). If it is, then the teacher knows that w0 ∈ T ∗ (I) ∧w0 ∈/ Ah and hence returns false together with w0 as a positive
counterexample to the learner. If w ∈/ T ∗ (I), then the teacher∗
knows that w ∈/ T (I) ∧ w ∈ Ah and hence returns false
together with w as a negative counterexample to the learner.
If all conditions hold, the “strict teacher” shows its generosity (Ah might not equal to T ∗ (I), but it will still pass) and5

concludes that (I, T , B) = true with a proof using Ah as theinductive invariant.

VI. E VALUATION
To evaluate our techniques, we have developed a prototype2
in Java and used the libalf library [18] as the default inferenceengine. We used our prototype to check safety properties
for a range of parameterised systems, including cache coherence protocols (German’s Protocol), self-stabilising protocols(Israeli-Jalfon’s Protocol and Herman’s Protocol), synchronisation protocols (Lehmann-Rabin’s Dining Philosopher Protocol), secure multi-party computation protocol (David Chaums’
Dining Cryptographers Protocol), and mutual exclusion protocols (Szymanski’s Protocol, Burn’s Protocol, Dijkstra’s Protocol, Lamport’s Bakery Algorithm, and Resource-Allocator
Protocol). Most of the examples we consider are standard
benchmarks in the literature of regular model checking (c.f.
[4], [5], [20], [22], [57]). Among them, German’s Protocol
and Kanban are more difficult than the other examples forfully automatic verification (c.f. [4], [5], [43]).
Based on these examples, we compare our learning methodwith existing techniques such as SAT-based learning [54],[55], [51], [52], extrapolating [16], [46], and abstract regularmodel checking (ARMC) [20], [21]. The SAT-based learning
approach encodes automata as Boolean formulae and exploits
a SAT-solver to search for candidate automata representing
inductive invariants. It uses automata-based algorithms toeither verify the correctness of the candidate or obtain acounterexample that can be further encoded as a Boolean
constraint. T(O)RMC [16], [46] extrapolates the limit of thereachable configurations represented by an infinite sequence ofautomata. The extrapolation is computed by first identifying
the increment between successive automata, and then overapproximating the repetition of the increment by adding loops
to the automata. ARMC is an efficient technique that integrates
abstraction refinement into the fixed-point computation. It
begins with an existential abstraction obtained by merging
states in the automata/transducers. Each time a spurious counterexample is found, the abstraction can be refined by splittingsome of the merged states. ARMC is among the most efficientalgorithms for regular model checking [38].
The comparison of those algorithms are reported in Table I,
running on a MinGW64 system with 3GHz Intel i7 processor,
2GB memory limit, and 60-second timeout. The experiments
show that the learning method is quite efficient: the resultsof our prototype are comparable with those of the ARMC
algorithm3 on all examples but Kanban, for which the minimal
inductive invariant, if it is regular, has at least 400 states.
On the other hand, our algorithm is significantly faster than
ARMC in two cases, namely German’s Protocol and Dining
Cryptographers. ARMC comes with a bundle of options andheuristics, but not all of them work for our benchmarks.
We have tested all the heuristics available from the tool andadopted the ones4 that had the best performance in our experi-

Theorem 1 (Correctness). If the algorithm from Fig. 1 terminates, it gives correct answer to the RMC problem (I, T , B).
To see this, observe that the algorithm provides an inductive
invariant when it concludes (I, T , B) = true and a word inT ∗ (I) ∩ B when it concludes (I, T , B) = false. In addition, if
one of the L∗ learning algorithms1 from Section IV is used,
we can obtain an additional result about termination:
Theorem 2 (Termination). When T ∗ (I) is regular, the algorithm from Fig. 1 is guaranteed to terminate in at most kiterations, where k is the size of the minimal DFA of T ∗ (I).
Proof. Observe that in the algorithm, the counterexample obtained by the learner in each iteration locates in the symmetricdifference of the candidate language and T ∗ (I). Hence, whenT ∗ (I) can be recognized by a DFA of k states, the algorithm
will not execute more than k iterations by Proposition 1.
Two remarks are in order. Firstly, the set T ∗ (I) tends tobe regular in practice, e.g., see [21], [38], [20], [22], [60],[57], [10], [11], [50], [49]. In fact, it is known that T ∗ (I) is
regular for many subclasses of infinite-state systems that canbe modelled in regular model checking [60], [50], [40], [11],[49] including pushdown systems, reversal-bounded countersystems, two-dimensional VASS (Vector Addition Systems
with States), and other subclasses of counter systems. Secondly, even in the case when T ∗ (I) is not regular, termination
may still happen due to the “generosity” of the teacher, which
will accept any inductive invariant as an answer.
Considerations on Implementation: The implementationof the learning-based algorithm is very simple. Since it isbased on standard automata learning algorithms and uses only
basic automata/transducer operations, one can find existing
libraries for them. The implementation only need to take careof how to answer queries. The core of our implementation
has only around 150 lines of code (excluding the parser ofthe input models). We provide a few suggestions to make theimplementation more efficient. First, each time when an FA
recognising Post k is produced, we store the pair (k, Post k ) ina cache. It can be reused when a query on any word of length
k is posed. We can also check if Post k ∩B = ∅. The algorithm
can immediately terminate and return (I, T , B) = false if
Post k ∩ B 6= ∅. Second, for each language inclusion test, if
the inclusion does not hold, we suggest to return the shortest
counterexample. This heuristic helped to shorten the average
length of strings sent for membership queries and hence
reduced the cost of answering them. Recall that the algorithm
needs to build the FA of Post k to answer membership queries.
The shorter the average length of query strings is, the fewer
instances of Post k have to be built.

2 Available at https://github.com/ericpony/safety-prover.
3 Available at http://www.fit.vutbr.cz/research/groups/verifit/tools/hades.
4 The heuristics are structure preserving, backward computation, and backward collapsing with all states being predicates. See [21] for explanations.

1 If N L∗ is used, the bound in Theorem 2 will increase to O(k 2 ).

6

Name
Bakery [32]Burns [4]Szymanski [59]German [36]Dijkstra [4]Dijkstra, ring [28], [33]Dining Crypto. [25]Coffee Can [52]Herman, linear [39]Herman, ring [39]Israeli-Jalfon [41]Lehmann-Rabin [47]
LR Dining Philo. [52]Mux Array [33]Res. Allocator [29]Kanban [5], [43]
Water Jugs [64]

The RMC problems#labelSinit
Tinit
Strans
3
3
3
5
12
3
3
10
11
9
9
118
581
3
3
17
42
1
1
13
12
3
3
13
14
10
30
17
6
8
18
13
2
2
4
4
2
2
4
9
2
3
6
24
6
4
4
14
4
4
4
3
6
3
3
4
3
3
3
7
3
25
48
98
11
5
6
23

Ttrans
19
125
412
9.5k
827
199
70
34
10
22
62
96
10
31
25
250
132

Sbad
3
3
13
4
3
3
12
5
1
1
1
3
3
3
4
37
5

Tbad
9
36
40
2112
126
36
70
8
1
1
1
13
4
18
9
68
12

Time
0.0s
0.2s
0.3s
4.8s
0.1s
1.4s
0.1s
0.0s
0.0s
0.0s
0.0s
0.1s
0.0s
0.0s
0.0s
t.o.
0.1s

RS
Sinv
6
8
43
14
9
22
32
3
2
2
4
8
4
5
5
–
24

Tinv
18
96
473
8134
378
264
448
18
4
4
8
48
16
30
15
–
264

Time
0.5s
1.1s
1.6s
t.o.
1.7s
0.9s
t.o.
0.2s
0.2s
0.4s
0.1s
0.5s
0.2s
0.4s
0.0s
t.o.
t.o.

SAT
Sinv
2
2
2
–
2
2
–
2
2
2
2
2
2
2
1
–
–

Tinv
5
10
21
–
24
14
–
7
4
4
4
11
6
7
3
–
–

T(O)RMC
Time
Sinv
Tinv
0.0s
6
11
0.1s
7
38
2.0s
51
102
t.o.
–
–
6.1s
8
83
t.o.
–
–
t.o.
–
–
0.1s
6
13
0.0s
2
4
0.0s
2
4
0.0s
4
8
0.8s
19
105
0.1s
7
18
0.2s
4
14
0.0s
4
9
t.o.
–
–
t.o.
–
–

ARMC
Time
0.0s
0.0s
0.1s
10s
0.3s
0.1s
7.2s
0.0s
0.0s
0.0s
0.0s
0.0s
0.0s
0.0s
0.0s
3.5s
0.0s

TABLE IC OMPARING THE PERFORMANCE OF DIFFERENT RMC TECHNIQUES . # LABEL STANDS FOR THE SIZE OF ALPHABET; S X AND T X STAND FOR THE NUMBERS
OF STATES AND TRANSITIONS , RESPECTIVELY, IN THE AUTOMATA / TRANSDUCERS . RS IS THE RESULT OF OUR PROTOTYPE USING R IVEST AND
S CHAPIRE ’ S VERSION OF L∗ ; SAT, T(O)RMC, AND ARMC ARE THE RESULTS OF THE OTHER THREE TECHNIQUES .

the set T ∗ (I) is regular, which is not guaranteed by approaches
based on a fixed-point computation (e.g., the ARMC [21]). An
interesting research question is whether L∗ algorithm can beeffectively used for verifying other properties, e.g., liveness.
Acknowledgements: We thank anonymous referees fortheir useful comments. Rümmer was supported by the Swedish
Research Council under grant 2014-5484.

ments. The performance of SAT-based learning is comparable
to the previous two approaches whenever inductive invariants
representable by automata with few states exist. However, as
its runtime grows exponentially with the sizes of candidate
automata, the SAT-based algorithm fails to solve four examples
that do not have small regular inductive invariants. T(O)RMC
seems to suffer from similar problems as it timeouts on all
examples that cannot be proved by the SAT-based approach.
Table II reports the results of the learning-based algorithm
geared with different automata learning algorithms implemented in libalf. As the table shows, these algorithms have similar performance on small examples; however, the algorithmof Rivest and Schapire [58] and the algorithm of Kearns andVarzirani [44] are significantly more efficient than the otheralgorithms on some large examples such as Szymanski andGerman. Table II shows that Kearns and Varzirani’s algorithm
can often find smaller inductive invariants (fewer states) thanthe other L∗ variants, which explains the performance difference. For NL∗ , our implementation pays an additional cost to
determinise the learned FA in order to answer the equivalence
queries; this cost is significant when a large invariant is needed.
Recall that our approach uses a “strict but generous teacher”.
Namely, the target language of the teacher is T ∗ (I) for an
RMC problem (I, T , B). We have tried the version wherea “flexible and generous teacher” is used, that is, the target
language of the teacher is the complement of (T −1 )∗ (B).
The performance, however, is worse than that of our current
version. This result may reflect the fact that the set T ∗ (I) is“more regular” (i.e., can be expressed by a DFA with fewer
states) than the set (T −1 )∗ (B) in practical cases.

R EFERENCES[1] P. A. Abdulla. Regular model checking. STTT, 14(2):109–118, 2012.
[2] P. A. Abdulla, M. F. Atig, Y. Chen, L. Holík, A. Rezine, P. Rümmer,
and J. Stenman. String constraints for verification. In CAV’14, pages
150–166.
[3] P. A. Abdulla, Y. Chen, L. Holík, R. Mayr, and T. Vojnar. Whensimulation meets antichains. In TACAS’10, pages 158–174.
[4] P. A. Abdulla, G. Delzanno, N. B. Henda, and A. Rezine. Regular model
checking without transducers (on efficient verification of parameterized
systems). In TACAS’07, pages 721–736.
[5] P. A. Abdulla, F. Haziza, and L. Holík. All for the price of few. In
VMCAI’13, pages 476–495.
[6] P. A. Abdulla, B. Jonsson, M. Nilsson, J. d’Orso, and M. Saksena.
Regular model checking for LTL(MSO). STTT, 14(2):223–241, 2012.
[7] P. A. Abdulla, B. Jonsson, M. Nilsson, and M. Saksena. A survey ofregular model checking. In CONCUR’04, pages 35–48.
[8] D. Angluin. Learning regular sets from queries and counterexamples.
Inf. Comput., 75(2):87–106, 1987.
[9] K. R. Apt and D. Kozen. Limits for automatic verification of finite-state
concurrent systems. IPL, 22(6):307–309, 1986.
[10] S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. FAST: accelerationfrom theory to practice. STTT, 10(5):401–424, 2008.
[11] S. Bardin, A. Finkel, J. Leroux, and P. Schnoebelen. Flat accelerationin symbolic model checking. In ATVA’05, pages 474–488.
[12] N. Bertrand and P. Fournier. Parameterized verification of many identicalprobabilistic timed processes. In FSTTCS’13, volume 24 of LIPIcs,
pages 501–513. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik.
[13] R. Bloem, S. Jacobs, A. Khalimov, I. Konnov, S. Rubin, H. Veith, and
J. Widder. Decidability of Parameterized Verification. Synthesis Lectures
on Distributed Computing Theory. Morgan & Claypool Publishers, 2015.
[14] B. Boigelot. Symbolic Methods for Exploring Infinite State Spaces. PhD
thesis, Université de Liège, 1999.
[15] B. Boigelot, A. Legay, and P. Wolper. Iterating transducers in the large(extended abstract). In CAV’03, pages 223–235.
[16] B. Boigelot, A. Legay, and P. Wolper. Omega-regular model checking.
In TACAS’04, pages 561–575.
[17] B. Bollig, P. Habermehl, C. Kern, and M. Leucker. Angluin-stylelearning of NFA. In IJCAI’09, pages 1004–1009.

VII. C ONCLUSION
The encouraging experimental results suggest that the performance of the L∗ algorithm for synthesising regular inductive invariants is comparable to the most sophisticatedalgorithm for regular model checking for proving safety. Froma theoretical viewpoint, learning-based approaches (including
ours and [54], [55], [38]) have a termination guarantee when7

Bakery
Burns
Szymanski
GermanDijkstraDijkstra, ring
Dining Crypto.
Coffee Can
Herman, linear
Herman, ring
Israeli-Jalfon
Lehmann-Rabin
LR D. Philo.
Mux Array
Res. Allocator
KanbanWater Jugs

Time
0.0s
0.2s
0.3s
4.8s
0.1s
1.4s
0.1s
0.0s
0.0s
0.0s
0.0s
0.1s
0.0s
0.0s
0.0s
>60s
0.1s

RS
Sinv
6
8
43
14
9
22
32
3
2
2
4
8
4
5
5
–
24

Tinv
18
96
473
8134
378
264
448
18
4
4
8
48
16
30
15
–
264

Time
0.0s
0.5s
2.4s
13s
0.4s
2.7s
0.2s
0.0s
0.0s
0.0s
0.0s
0.2s
0.2s
0.0s
0.0s
>60s
0.5s

L∗
Sinv
6
8
51
15
9
20
34
3
2
2
4
8
4
5
4
–
25

Tinv
18
96
561
8715
378
240
476
18
4
4
8
48
16
30
12
–
275

Time
0.1s
0.2s
1.2s
26s
0.1s
8.9s
0.2s
0.0s
0.0s
0.0s
0.0s
0.1s
0.0s
0.0s
0.0s
>60s
0.5s

L∗ c
Sinv
6
8
41
15
9
22
38
4
2
2
4
8
5
5
5
–
25

Tinv
18
96
451
8715
378
264
532
24
4
4
8
48
20
30
15
–
275

Time
0.0s
0.2s
0.3s
4.2s
0.2s
1.5s
0.1s
0.0s
0.0s
0.0s
0.0s
0.1s
0.0s
0.0s
0.0s
>60s
0.1s

KV
Sinv
6
8
41
14
9
14
19
3
2
2
4
8
4
5
5
–
24

Tinv
18
96
451
8134
378
168
266
18
4
4
8
48
16
30
15
–
264

Time
0.1s
0.4s
1.4s
40s
0.2s
1.8s
0.3s
0.0s
0.0s
0.0s
0.0s
0.2s
0.0s
0.0s
0.0s
>60s
0.5s

NL∗
Sinv
6
6
59
15
10
20
36
4
2
2
4
8
8
5
5
–
25

Tinv
18
72
649
8715
420
240
504
24
4
4
8
48
32
30
15
–
275

TABLE IIC OMPARING THE PERFORMANCE BASED ON DIFFERENT AUTOMATA LEARNING ALGORITHMS . T HE COLUMNS L∗ , L∗ c, RS, KV, AND NL∗ ARE THE∗
RESULTS OF THE ORIGINAL L ALGORITHM BY A NGLUIN [8], A VARIANT OF L∗ THAT ADDS ALL SUFFIXES OF THE COUNTEREXAMPLE TO COLUMNS ,THE VERSION BY R IVEST AND S HAPIRE [58], THE VERSION BY K EARNS AND VAZIRANI [44], AND THE NL∗ ALGORITHM [17], RESPECTIVELY.
[18] B. Bollig, J.-P. Katoen, C. Kern, M. Leucker, D. Neider, and D. R.
Piegdon. libalf: The automata learning framework. In CAV’10, pages
360–364.
[19] F. Bonchi and D. Pous. Checking NFA equivalence with bisimulations
up to congruence. In POPL’13, pages 457–468.
[20] A. Bouajjani, P. Habermehl, A. Rogalewicz, and T. Vojnar. Abstract
regular tree model checking. ENTCS, 149(1):37–48, 2006.
[21] A. Bouajjani, P. Habermehl, and T. Vojnar. Abstract regular model
checking. In CAV’04, pages 372–386.
[22] A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili. Regular model
checking. In CAV’00, pages 403–418.
[23] A. Bouajjani and T. Touili. Widening techniques for regular tree model
checking. STTT, 14(2):145–165, 2012.
[24] M. Chapman, H. Chockler, P. Kesseli, D. Kroening, O. Strichman, and
M. Tautschnig. Learning the language of error. In ATVA’15, pages
114–130.
[25] D. Chaum. The dining cryptographers problem: Unconditional senderand recipient untraceability. Journal of Cryptology, 1(1):65–75, 1988.
[26] Y. Chen, A. Farzan, E. M. Clarke, Y. Tsay, and B. Wang. Learning
minimal separating DFA’s for compositional verification. In TACAS’09,
pages 31–45.
[27] Y. Chen, C. Hsieh, O. Lengál, T. Lii, M. Tsai, B. Wang, and F. Wang.
PAC learning-based verification and model synthesis. In ICSE’16, pages
714–724.
[28] E. W. Dijkstra, R. Bird, M. Rogers, and O.-J. Dahl. Invariance and nondeterminacy [and discussion]. Philosophical Transactions of the Royal
Society of London A: Mathematical, Physical and Engineering Sciences,312(1522):491–499, 1984.
[29] A. F. Donaldson. Automatic techniques for detecting and exploiting
symmetry in model checking. PhD thesis, University of Glasgow, 2007.
[30] J. Esparza. Parameterized verification of crowds of anonymous processes. Dependable Software Systems Engineering, 45:59–71, 2016.
[31] A. Farzan, Y. Chen, E. M. Clarke, Y. Tsay, and B. Wang. Extending
automated compositional verification to the full class of omega-regular
languages. In TACAS’08, pages 2–17.
[32] W. Fokkink. Distributed Algorithms. MIT Press, 2013.
[33] L. Fribourg and H. Olsén. Reachability sets of parameterized rings asregular languages. ENTCS, 9:40, 1997.
[34] P. Garg, C. Löding, P. Madhusudan, and D. Neider. ICE: A robust
framework for learning invariants. In CAV’14, pages 69–87.
[35] P. Garg, C. Löding, P. Madhusudan, and D. Neider. Learning universallyquantified invariants of linear data structures. In CAV’13, pages 813–
829.
[36] S. M. German and A. P. Sistla. Reasoning about systems with many
processes. JACM, 39(3):675–735, 1992.
[37] O. Grinchtein, M. Leucker, and N. Piterman. Inferring network invariants
automatically. In IJCAR’06, pages 483–497.

[38] P. Habermehl and T. Vojnar. Regular model checking using inferenceof regular languages. ENTCS, 138(3):21–36, 2005.
[39] T. Herman. Probabilistic self-stabilization. IPL, 35(2):63–67, 1990.
[40] O. H. Ibarra. Reversal-bounded multicounter machines and their decision
problems. J. ACM, 25(1):116–133, 1978.
[41] A. Israeli and M. Jalfon. Token management schemes and random walks
yield self-stabilizing mutual exclusion. In PODC’90, pages 119–131.
[42] B. Jonsson and M. Nilsson. Transitive closures of regular relations forverifying infinite-state systems. In TACAS’00, pages 220–234.
[43] A. Kaiser, D. Kroening, and T. Wahl. Dynamic cutoff detection inparameterized concurrent programs. In CAV’10, pages 645–659.
[44] M. J. Kearns and U. V. Vazirani. An Introduction to Computational
Learning Theory. MIT press, 1994.
[45] Y. Kesten, O. Maler, M. Marcus, A. Pnueli, and E. Shahar. Symbolicmodel checking with rich assertional languages. TCS, 256(1-2):93–112,
2001.
[46] A. Legay. T(O)RMC: A tool for (ω)-regular model checking. In CAV’08,
pages 548–551.
[47] D. Lehmann and M. O. Rabin. On the advantages of free choice:a symmetric and fully distributed solution to the dining philosophers
problem. In POPL’81, pages 133–138.
[48] O. Lengál, A. W. Lin, R. Majumdar, and P. Rümmer. Fair termination
for parameterized probabilistic concurrent systems. In TACAS’17.
[49] J. Leroux and G. Sutre. Flat counter automata almost everywhere! In
ATVA’05, pages 489–503.
[50] A. W. Lin. Accelerating tree-automatic relations. In FSTTCS’12, pages
313–324.
[51] A. W. Lin, T. K. Nguyen, P. Rümmer, and J. Sun. Regular symmetry
patterns. In VMCAI’16, pages 455–475.
[52] A. W. Lin and P. Rümmer. Liveness of randomised parameterised
systems under arbitrary schedulers. In CAV’16, pages 112–133.
[53] N. A. Lynch, I. Saias, and R. Segala. Proving time bounds for
randomized distributed algorithms. In PODC’94, pages 314–323.
[54] D. Neider. Applications of Automata Learning in Verification and
Synthesis. PhD thesis, RWTH Aachen, 2014.
[55] D. Neider and N. Jansen. Regular model checking using solver
technologies and automata learning. In NFM, pages 16–31, 2013.
[56] D. Neider and U. Topcu. An automaton learning approach to solving
safety games over infinite graphs. In TACAS’16, pages 204–221.
[57] M. Nilsson. Regular Model Checking. PhD thesis, Uppsala Univ., 2005.
[58] R. L. Rivest and R. E. Schapire. Inference of finite automata using
homing sequences. Inf. Comput., 103(2):299–347, 1993.
[59] B. K. Szymanski. A simple solution to Lamport’s concurrent programming problem with linear wait. In ICS’88, pages 621–626.
[60] A. W. To and L. Libkin. Algorithmic metatheorems for decidable LTL
model checking over infinite systems. In FoSSaCS’10, pages 221–236.
[61] A. Vardhan. Learning To Verify Systems. PhD thesis, Department ofComputer Science, University of Illinois at Urbana-Champaign, 2006.

8

[62] A. Vardhan, K. Sen, M. Viswanathan, and G. Agha. Learning to verify
safety properties. In ICFME’04, pages 274–289.
[63] A. Vardhan and M. Viswanathan. LEVER: A tool for learning based
verification. In CAV’06, pages 471–474.
[64] Wikipedia. Liquid water pouring puzzles. https://en.wikipedia.org/
w/index.php?title=Liquid_water_pouring_puzzles&oldid=764748113,
2017. [Accessed: 24-February-2017].
[65] P. Wolper and B. Boigelot. Verifying systems with infinite but regularstate spaces. In CAV’98, pages 88–97.

λ
T
N
TT
TN

λ
⊥
>
⊥
⊥
>

N
T

T
N

Fig. 2. Using learning to solve the RMC problem (I, T , B) of Herman’s
Protocol. The table on the left is the content of the observation table used by
the automata learning algorithm of Rivest and Shaphire [58] and the automaton
on the right is the inferred candidate DFA.

VIII. A PPENDIX
We provide some more examples for regular model checking in the appendix.
Example 2 (RMC of the Herman’s Protocol). Consider the
RMC problem of Herman’s Protocol in Example 1. Initially,
several membership queries will be posed to the teacher toproduce the closed observation table on the left of Fig. 2. In
this example, the teacher returns > only for words containing
an odd number of the symbol T. The learner will then construct
the candidate FA Ah on the right of Fig. 2 and pose anequivalence query on Ah . Observe that Ah can be used as an
inductive invariant in a regular proof. It is easy to verify that
I = N∗ T(N∗ TN∗ TN∗ )∗ ⊆ Ah and Ah ∩ B = Ah ∩ N∗ = ∅.
The condition (3) T (Ah ) ⊆ Ah of a regular proof can beproved to be correct based on the following observation:
the FA Ah recognises exactly the set of all configurations
with an odd number of tokens. When tokens are discarded
in a transition, the total number of discarded tokens in allprocesses is always 2. The other two types of transitions will
not change the total number of tokens in the system. It follows
that taking a transition from any configurations in Ah will
arrive a configuration with an odd number of tokens, whichis still in Ah .
The verification of Herman’s Protocol finishes after the first
iteration of learning and hence we cannot see how the learningalgorithm uses a counterexample for refinement. Below weintroduce a slightly more difficult problem.
Example 3 (RMC of the Israeli-Jalfon’s Protocol). IsraeliJalfon’s Protocol is a routing protocol of n processes organised in a ring-shaped topology, where a process may hold atoken. Again we assume the processes are numbered from 0
to n − 1. If the process with the number i is chosen by thescheduler, it will toss a coin to decide to pass the token to
the left or right, i.e. the one with the number (i − 1)%n or(i + 1)%n. When two tokens are held by the same process,they will be merged. The safety property of interest is thatevery system configuration has at least one token. The protocol
and the corresponding safety property can be modelled as aregular model checking problem (I, T , B), together with theset of initial configurations I = (T + N)∗ T(T + N)∗ T(T + N)∗ ,i.e., at least two processes have tokens, and the set of bad
configurations B = N∗ , i.e., all tokens have disappeared.
Again we use the regular language E = ((T, T) + (N, N))9to denote the relation that a process is idle, i.e, the process
does not change its state. The transition relation T then canbe specified as a union of the regular expressions in Figure 3.
E ∗ (T, N)((T, T) + (N, T))E ∗ , ((T, T) + (N, T))E ∗ (T, N)E ∗ ((T, T) + (N, T))(T, N)E ∗ , (T, N)E ∗ ((T, T) + (N, T))(Pass the token right)(Pass the token left)

Fig. 3. The Transition Relation of Israeli-Jalfon’s Protocol

When the automata learning algorithm of Rivest andShaphire is applied to solve the RMC problem, we can obtainan inductive invariant with 4 states in 3 iterations. The firstcandidate FA in Fig. 4(a) is incorrect because it does notinclude the initial configuration TT. By analysing the counterexample TT, the learning algorithm adds the suffix T to theset E. The second candidate FA in Fig. 4(b) is still incorrect
because it contains an unreachable bad configuration NNN.
The learning algorithm analyses the counterexample NNN andadds the suffix N to the set E. This time it obtains the candidate
FA in Fig. 4(c), which is a valid regular inductive invariant.
λ
⊥
⊥
⊥

λ
T
N

T, N

(a) First candidate automaton

λ
T
TT
N
TN
TTT
TTN

λ
⊥
⊥
>
⊥
>
>
>

T
⊥
>
>
>
>
>
>

T, N

T, N

T, N
(b) Second candidate automaton

λ
T
N
TT
TN
NT
NN
TTT
TTN

λ
⊥
⊥
⊥
>
>
>
>
>
>

T
⊥
>
>
>
>
>
>
>
>

N
⊥
>
⊥
>
>
>
⊥
>
>

T

N
N

T, N

T

T, N

(c) Third candidate automaton
Fig. 4. Using learning to solve the RMC problem (I, T , B) of IsraeliJalfon’s Protocol. The table on the left of each sub-figure is the content of
the observation table used by the automata learning algorithm of Rivest andShaphire [58].

10