Introduction

A state machine M consists of a set S of states that includes the initial states I and a binary relation T over states. (s, s ) ∈ T is called a transition. Reachable states R M of M are inductively1 defined as follows: I ⊆ R M , and if s ∈ R M and (s, s ) ∈ T , then s ∈ R M . A distributed system DS can be formalized as M and many desired properties of DS can be expressed as invariants of M . An invariant of M is a state predicate p of M such that p holds for all s ∈ R M .

To prove that p is an invariant of M , it suffices to find an inductive invariant q of M such that q(s) ⇒ p(s) for each s ∈ S. An inductive invariant q of M is a state predicate of M such that (∀s 0 ∈ I) q(s 0 ) and (∀(s, s ) ∈ T ) (q(s) ⇒ q(s )). Note that an inductive invariant of M is an invariant of M but not vice versa.

Finding an inductive invariant q (or conjecturing a lemma q) is one of the most intellectual activities in ITP 2 . This activity requires human users to profoundly understand the system under verification or M formalizing the system to some extent. The users must rely on some reliable sources that let them get better understandings of the system and/or M to conduct the non-trivial task, namely lemma conjecture. For this end, our experiences on ITP tell us that it is useful to get better understandings of R M . Some characteristics of R M can be used to systematically construct a state predicate q i that is a part of q.

s ∈ S is characterized by some values that are called observable values. Based on our experiences on ITP, the characteristics of R M are correlations among observable values of the elements of R M . Generally, the number of the elements of R M is unbounded and then a huge number of reachable states are generated from M . The task of extracting correlations among a huge number of data (reachable states in our case) is the role of Machine Learning (ML).

We have conducted two case studies on Alternating Bit Protocol (ABP, a simplified version of Sliding Window Protocol used in TCP) and Simple Communication Protocol (SCP, a simplified version of ABP) using a framework in which Progol, an ILP system, has been mainly used to extract some characteristics of the reachable states of their state machines formalizing the protocols. Before the two case studies reported in this paper, we (especially the third author) had conducted verification case studies in which it is proved that both protocols enjoy what is called the reliable communication property that whenever the current data to be delivered is i, the data upto i or i − 1 have been successfully delivered to the receiver from the sender without any duplications nor drops. Through those verification case studies, we drew four possible reachable state patterns (see Fig. 5) for SCP and six possible reachable state patterns (see Fig. 6) for ABP. Those state patterns can be used as oracles for judging if learned hypotheses are reasonably good.

The rest of the paper is organized as follows. Sect. 2 introduces our motivation together with some background knowledge of systems verification with ITP and Sect. 3 briefly shows the verification process on the case studies. Sect. 4 describes our framework that is a combination of the tools used to construct an ILP input from a system specification that is suitable for a theorem prover. Sect. 5 summaries the results on some experiments for the case studies using our framework to extract the characteristics of R M with ILP. Sect. 6 mentions some related work. Sect. 7 concludes the paper and mentions some future directions.

Preliminary

Systems verification is a research area aiming at rigorously checking if systems satisfy desired properties. ITP is a formal verification technique in which mathematical models are made for systems and desired properties are treated as theo-rems of the mathematical models. State machines are used as such mathematical models. For example, it is possible to check if an e-commerce protocol satisfies the property that if an acquirer authorizes a payment, then both the buyer and seller concerned always agree on it [1]. Logics, theories, techniques and tools for theorem proving have been advanced a lot, e.g. logical decision procedures used in SMT [2]. However, some non-trivial interactions between human users and theorem provers are still needed to conduct proofs that non-trivial state machines enjoy non-trivial properties. One of the most intellectual activities in such interactions is to conjecture lemmas.

To formally verify that a system satisfies a desired property with ITP, the system is first formalized as a state machine M that is described in a formal specification language. A state predicate p is described in the same or a different specification language for the property. An interactive theorem prover is used to prove that p is an invariant of M . We use a proof score approach to systems verification called the OTS/CafeOBJ method3 , in which CafeOBJ, an algebraic specification language and system used as a specification language for M and p and also as an interactive theorem prover. There are three main activities in the OTS/CafeOBJ method to conduct ITP: application of simultaneous structural induction (SSI), case analysis (CA) and use of lemmas (including lemma conjecture).

Let us consider a mutual exclusion protocol called TAS as an example. TAS written in an Algol-like language is shown in Fig. 1 (a). TAS uses lock to control processes such that there is at most one process in Critical Section (or at cs). Initially, lock is false and each process is in Remainder Section (or at rs). test&set(b) atomically sets b true and returns false if b is false, and just returns true otherwise. TAS is formalized as a state machine M TAS whose transitions are depicted in Fig. 1 (b) and (c). The arrow on which try x and [b = f] are attached is interpreted as follows: if process x is at rs and b is false in a given state, then x moves to cs and b is set true. The arrow on which exit x is attached is interpreted as follows: if process x is at cs, then x moves to rs and b is set false. Note that transitions are declared in terms of equations in the OTS/CafeOBJ method. One desired property TAS should enjoy is the mutual exclusion property. Let mx(s, x, y) be (pc(s, x) = cs ∧ pc(s, y) = cs ⇒ x = y), where s is a state x, y are process identifiers and pc(s, x) is the location (rs or cs) where process x is in state s, and let mx(s) be (∀x, y ∈ Pid) mx(s, x, y), where Pid is the set of all process identifiers. To verify that TAS enjoys the property, all we have to do is to prove that mx(s) is an invariant of M TAS .

Fig. 2 shows a snip of a proof tree that mx(s) is an invariant of M TAS , although proofs are written as texts in the OTS/CafeOBJ method. Given a state s and a process identifier k, try(s, k) is the state obtained by applying transition try k in s, exit(s, k) is the state obtained by applying transition exit k in s, and lock(s) is the Boolean value stored in variable lock in s. SSI on s is first used to split the initial goal into three sub-cases. What to do for the three sub- cases is to show mx(s 0 , i, j), mx(s, i, j) ⇒ mx(try(s, k), i, j) and mx(s, i, j) ⇒ mx(exit(s, k), i, j), respectively, where s 0 is an arbitrary initial state, s is an arbitrary state, and i, j, k are arbitrary process identifiers. CA is then repeatedly used until what to show reduces either true or false. Any case in which what to show reduces true is discharged. For any case in which what to show reduces false, we need to conjecture lemmas4 . Let us consider the case marked Case A in Fig. 2 in which mx(s, i, j) ⇒ mx(try(s, k), i, j) reduces false. Therefore, Case A needs a lemma. Let lem1(s, i) be such a lemma. We will soon describe how to conjecture the lemma. lem1(s, i) ⇒ (mx(s, i, j) ⇒ mx(try(s, k), i, j) reduces true, discharging Case A, provided that we prove that (∀x ∈ Pid) lem1(s, x) is an invariant of M TAS . The proof needs mx(s, i, j) as a lemma. This is why we use simultaneous structural induction.

Let P and Q be the sets of states that correspond to predicates p and q, respectively. S, I, R M , P and Q can be depicted as shown in Fig. 3. Proving that p is an invariant of M is the same as proving R ⊆ P . Let (s, s ) ∈ T be an arbitrary transition. In each induction case or a subcase of each induction case, all needed is basically to show p(s) ⇒ p(s ) so as to prove that p is an invariant of M . There are four possible situations: (1) s, s ∈ P , (2) s ∈ P and s ∈ P , (3) s, s ∈ P , and (4) s ∈ P and s ∈ P. p(s) ⇒ p(s ) holds for (1), ( 2) and ( 3), but does not for (4). To complete the proof that p is an invariant of M , we need to know s ∈ R M for (4), namely that s' is not reachable for (4). To this end, we need to conjecture a lemma q such that q does not hold for s'. Case A in Fig. 2 is an instance of (4). Case A is characterized with pc(s, k) = cs, lock(s) = false, i = k, j = k, and pc(s, i) = cs (that are attached to the path to Case A from the root), from which we can systematically conjecture the following lemma:

¬(pc(s, k) = rs ∧ ¬lock(s) ∧ i = k ∧ j = k ∧ pc(s, i) = cs)

. This lemma could be used to discharge Case A, but lemmas should be shorter because we need to prove that lemmas are invariants of M . Any state predicate that implies the lemma could be a lemma, one of which is ¬(pc(s, i) = cs ∧ ¬lock(s)) that is equivalent to pc(s, i) = cs ⇒ lock(s) that is lem1(s, i). The systematic way to conjecture lemmas may not work for larger examples than TAS because case analysis may have to be repeated too many times until what to show reduces either true or false. Even if we reach the case in which what to show reduces false, a lemma conjectured could be so long that we may find it trouble to prove that the lemma is an invariant of M .

Our experiences on ITP tell us that better understandings of M and/or how M behaves let us conjecture useful lemmas to complete the proof concerned. Moreover, the properties we are interested in are invariants in this paper. Therefore, it suffices to get better understandings of R M . In general, R M contains an infinite number of states, and the task of extracting knowledge from such a huge database is the role of ML. However, classical machine-learning techniques only work for a database whose elements are expressed in propositional form, while our database consists of system states expressed in first-order form. There is the ML technique that can deal with first-order forms: Inductive Logic Programming (ILP). This is why we use ILP. Let PQueue and BQueue be the sets of queues of BNPair and queues of Bool, respectively. The difference between ABP and SCP is as follows. dc ∈ PQueue and ac ∈ BQueue are used in ABP. snd1, rec1, snd2, rec2, drp1 and drp1 in ABP are quite similar to those in SCP, although the top element of each queue is taken into account in ABP. ABP has two more classes of transitions dup1 and dup2. If dc and ac are not empty, then dup1 and dup2 duplicates the top element of dc and ac, respectively, in ABP. Let M ABP be a state machine formalizing ABP.

One property SCP and ABP should enjoy is what is called the reliable communication property. The property can be described as follows: all data up to the current one d or the previous one d − 1 have been successfully delivered to Receiver without any duplicates nor any drops. To verify that SCP and ABP enjoy the property, all we have to do is to prove that the following state predicate is an invariant of M SCP and M ABP , respectively: ((sb = rb) ⇒ (buf = ). Let rcp be the state predicate. We may explicitly write rcp(s), where s is a state. Conducting the formal verification that rcp is an invariant of M SCP and gradually getting better understandings of SCP, we have realized that the reachable states of M SCP can be classified into the four state patterns shown in Fig. 5, and lemmas can be conjectured from the four state patterns. To prove that rcp(s) is an invariant of M SCP , we first apply SSI to s, generating seven sub-cases (or sub-goals). One sub-case is the induction case in which rec2 is taken into account. Let us consider the induction case. The case is first split into two sub-cases based on the condition of rec2: (1) dc is empty and (2) dc is not empty. Case ( 1 Conducting the formal verification that rcp is an invariant of M ABP and gradually getting better understandings of ABP, we have realized that the reachable states of M ABP can be classified into the six state patterns shown in Fig. 6, and lemmas can be conjectured from the six state patterns.

Framework

ILP is a machine learning technique for constructing concept definitions (logic programs) from examples and a logical domain theory (background knowledge) [5]. In general setting, an ILP learning task is defined as follows. To fully describe a learning task in ILP, we need to clearly define B, H, E together with E + and E − . Since our learning task is to characterize R M , E is a set of system states consisting of reachable states (E + ) and unreachable states (E − ). Then, H is a logic program that is an approximate definition of R M such that it is expected to be able to judge if a given state is reachable for M . Note that it is in general impossible to construct a computable predicate that can always judge if a given state is reachable for M from the undecidability of the reachability problem. Finally, B is a set of clauses that define data structures, types, predicates, etc. used in E and to construct H.

We have designed a framework for our purpose. The architecture of the framework is shown in Fig. 7. An input to the framework is an equational system specification of a state machine of which we would like to extract the characteristics of the reachable states. An equational specification is written in CafeOBJ and suited for ITP. An equational specification is first translated into a rewrite theory specification written in Maude (a sibling language of CafeOBJ) with an automatic translator YAST [6]. A rewrite theory specification is suited for model checking. The Maude search command, a bounded model checker for invariants, is then used to generate reachable states that are positive examples in our learning task. Possible unreachable states that are negative examples in our learning task are generated as follows. Given a state predicate that is likely to be an invariant of a state machine concerned, we randomly generate states and then produce each of the states that does not satisfy the state predicate as an unreachable state. Those states generated as E are expressed in Maude, which should be converted into unit Horn clauses in Prolog.

Types and data structures used in an equational specification should be converted into Horn clauses in Prolog so that they can be used as B. For example, natural numbers specified in CafeOBJ is as follows: Moreover, user defined functions in equations should be converted into Horn clauses. For example, let us consider the following function: op mk : Nat → List eq mk(0) = 0 . eq mk(s(X)) = s(X) | mk(X) .

where List is the type (sort) for lists of natural numbers, and nil and _|_ are the constructors of List

Experiments

We have experimented with normal learning mode (with both positive and negative examples) and with positive example only mode (with positive examples only) to learn hypotheses from various collections of system states (from 100 to 5000 for SCP case and from 500 to 10000 for ABP case). The results with both learning modes were almost the same.

Therefore, in the rest of the section, we describe some sets of clauses extracted from various collections of reachable states with learning from positive only mode [7]. Moreover, the clauses are compared with the state patterns shown in Fig. 5 and Fig. 6 to explain which characteristics are extracted. We also describe how to conjecture lemmas from the learned hypotheses.

Simple Communication Protocol

With respect to the background knowledge describing some data types, such as Boolean values, natural numbers in Peano style and lists of natural numbers together with some auxiliary functions described in Mode Declarations for constructing clauses (the descriptions of the functions are shown in Appendix A), the experiments on SCP produced various sets of clauses from various collections of reachable states. Based on the quality of what have been obtained from each set of clauses, we have realized that the experiments on around 1000 states are good enough for our learning task.

Some constraints have been used to generate reachable states used as positive examples so as to make computational burden not too big and make learned hypotheses reasonably good. Among the constraints used are as follows. Each natural number n used in each reachable state was to satisfy the condition 1 ≤ n ≤ 10. This is because otherwise natural numbers are inductively defined, forcing Progol to be loaded with too big computational burden. Each collection has been generated from a different state that is reachable from an initial state.

We have conducted multiple experiments and obtained multiple sets of learned axioms. Among them, we have selected one (called Set 1) that is most likely to be closer to the four state patterns. Set 1 has been learned by Progol with Mode declaration in Appendix A and is as follows: state(A, B, C, D, c(p(A, B)), c(E)) : -mk(B, D) . state(A, B, A, C, c(p(D, E state(A, B, A, C, c(p(A, B

)), c(A)) : -mk(B, [B | C]) .

where p(b, n) denotes p, n and c is used to construct non-empty cells. The clauses define the predicate that takes six arguments whose types are declared in Mode declaration 1. The six arguments correspond to sb, rb, d, buf , dc, and ac, respectively. The first clause in Set 1 says that if buf is the list that consists of d, d − 1, . . . , 0 in this order, then the head is reachable. The head also says that dc consists of the pair of sb and p. Therefore, the clause extracts the characteristics shared by State Pattern 2 and State Pattern 3. The second clause in Set 1 says that if sb is different from the first element b in the pair b, n of dc and buf is the list that consists of d − 1, . . . , 0 in this order, then the head is reachable. The head also says that rb and the Boolean value in ac are the same as sb. Therefore, the clause extracts almost all characteristics of State Pattern 4. The clause does not mention the second element n in the pair b, n of dc. The third clause in Set 1 says that if buf is the list that consists of d − 1, . . . , 0 in this order, then the head is reachable. The head also says that sb, rb, the first element b in the pair b, n of dc, and the Boolean value in ac are the same. The clause perfectly extracts the characteristics of State Pattern 1.

If the set {state( − → x ) : Since such a perfect set of clauses cannot be learned in general due to the undecidability of the reachability problem, however, this is not the way we can use to conjecture lemmas from learned hypotheses. Moreover, the formula constructed by n i=0 cond i ( − → x ) must be too long to be used effectively, even if it is the strongest inductive invariant.

-cond i ( − → x ) | i = 1, . . . ,Let cond i ( − → x ) be pre i ( − → x ), con i ( − → x ), oth i ( − → x )

, where oth i ( − → x ) may be void. We

suppose that if pre k ( − → x ) holds, then each cond i ( − → x ) for i ∈ {1, . . . , n} − {k} does not hold. Then, pre k ( − → x ) ⇒ con k ( − → x ) is one possible candidate of lemma. If there exist more than one such k, say k 1 , . . . , k m , then m j=1 (pre kj ( − → x ) ⇒ con kj ( − → x ))

is one possible candidate of lemma. This is basically how we conjecture lemmas from learned axioms (or hypotheses) or state patterns, such as the four state patterns for SCP and the six state patterns for ABP. The third axiom of the learned ones for SCP contains rb = b, dc = c( b, n ), sb, d = b, n as part of the condition. If rb = b, the condition of the second axiom does not hold. The first axiom has sb, d = b, n as part of the condition. Therefore, according to the way to conjecture lemma, we can conjecture dc = c( b, n ) ∧ rb = b ⇒ sb, d = b, n as one lemma. This lemmas is the same as the one conjectured from the four state patterns in Sect. 3.

Alternating Bit Protocol

ABP is a modified version of SCP such that its channels are unbounded. Therefore, we need to define some more complex data structures: queues of pairs of Boolean values and natural numbers -used for dc, and queues of Boolean values -used for ac. Moreover, some auxiliary functions for these data structures are also defined as shown in Appendix B. From the experiments, it was sufficient to use about 1500 reachable states for our learning task. In addition to the same constraints used to generate reachable states in the experiments for SCP, some more constraints were used. For example, each queue used in each reachable state contains at least two elements. Since more recursively defined data structures are used in ABP than in SCP, Progol spends more resources (both computational and spatial resources) to search and compute candidates of learned hypotheses and often reaches the limitation of resources. Hence, the learned hypotheses in the experiments for ABP were not as good as those for SCP. Each set of learned hypotheses does not extract many characteristics of the reachable states of ABP. For example, let us consider the following set of clauses learned with Mode Declaration 2 in Appendix A. We suspected that we did not use enough background knowledge so that some very important characteristics on dc and ac could be extracted in the experiment in which the last set of clauses were learned. The important characteristics on dc is that dc contains at most one gap such that two adjacent pairs b, i and next( b, i ) appear at most once in dc, where next( b, i ) = ¬b, i + 1 . We have added two predicates gap0 and gap1 whose definitions are found in Appendix A. Then, the following set of clauses have been learned by Progol:

state(A, B, C, D, [p(A, B) | E], [A | F ]) : -neg(A, C), gap0(p(A, B), E) . state(A, B, C, D, [p(A, B) | E], [C | F ]) : -mk(B, D), gap0(p(A, B), E) . state(A, B, A, C, [p(D, E) | F ], [A | G]) : -neg(A, D), succ(E, B), mk(B, [B | C]) . gap1(p(A, B), F ) . state(A, B, A, C, [p(A, B) | D], [A | E]) : -mk(B, [B | C]), gap0(p(A, B), D) .

The third clause more precisely extracts the characteristics of State Pattern 6 showing in Fig. 6, including the important characteristics of dc. Since the third clause is the only one in which gap1(p(A, B), F ) holds, we can conjecture a lemma from this clause. gap1(p(A, B), F ) can be rephrased as follows: dc = ps1@(p1, p2, ps2)

∧ p1 = p2 ∧ (p3 ∈ ps1 ⇒ p3 = p1) ∧ (p4 ∈ ps4 ⇒ p4 = p2),

where @ is the concatenation function of queues. Therefore, we can conjecture the following:

(dc = ps1@(p1, p2, ps2) ∧ p1 = p2 ∧ (p3 ∈ ps1 ⇒ p3 = p1)∧ (p4 ∈ ps4 ⇒ p4 = p2)) ⇒ (p2 = sb, d ∧ buf = d − 1, . . . , 0)

This lemma is very useful to prove that ABP enjoys the reliable communication protocol.

Honestly speaking, it is not easy to systematically come up with gap0 and gap1 from the formal specification of ABP. This has something to do with what is called Predicate Invention [8]. It is one piece of our future work to systematically discover some predicate, such as gap0 and gap1 that do not explicitly appear in formal specifications. We anticipate that Meta-interpretive learning and its implementation M etagol [9] will help us do so.

Related Work

ML has been used to find lemmas in ACL2 [10]. Their tool can calculate the similarity between the current proof and other proofs in a given proof library containing many existing proofs that have already been proved. Their tool finds an existing proof whose structure is most likely to be similar to that of the current proof, and proposes lemmas for the current proof that are constructed from the lemmas used for the existing proof.

ILP has been successfully integrated with model checking [11]. Although a model checker systematically finds a counterexample demonstrating that a system specification (or a model) does not enjoy a property, human users are supposed to revise the system specification so that the revised version can enjoy the property. They propose a way to systematically conduct such a revision for the system specification with an ILP system that uses a counterexample found by a model checker as a negative example, a witness constructed according to the property concerned as a positive example, and a system specification as the background knowledge.

Our way to use an ILP system is different from the two above mentioned studies. We use an ILP system to extract the characteristics of the reachable states of a state machine as learned clauses (hypotheses) from which lemmas could be conjectured.

Conclusion and Future Work

We have reported on case studies in which Progol has been mainly used to extract the characteristics of the reachable states of M SCP and M ABP . We have compared them with the state patterns we had manually learned from our ITP experiences for SCP and ABP. We have not formally proved that the four and six state patterns exactly cover all reachable states of M SCP and M ABP , respectively. But, our experiences on conjecturing lemmas based on the state patterns say that they are most likely to do so and very useful for lemma conjecture. It would be possible to generate different state patterns by combining and dividing those state patterns. From a lemma conjecture point of view, however, the four and six state patterns for SCP and APB are very useful. The learned hypotheses (a set of clauses) for SCP is very close to the four state patterns if not exactly the same. If gap0 and gap1 are used, the learned hypotheses for ABP is also close to the six state patterns. Otherwise, the learned hypotheses for ABP do not capture the important characteristics on dc appearing in State Pattern 6.

We have also described how to conjecture lemmas based on the learned hypotheses. This demonstrate that our approach is likely to be promising for lemma conjecture.

But, there are lots more things left to do. In our experiments, gap0 and gap1 have been provided by human beings. It is not trivial to come up with such predicates because they do not explicitly appear in an equational specification written in CafeOBJ. It is called predicate invention to come up with new predicates from a program or specification in which those predicates are not explicitly used. Metagol has implemented a mechanism with which predicate invention is doable. One piece of our future work is to come up with a method in which Metagol is mainly used to invent new predicates, such as gap1 and gap1. We need to conduct more case studies in which our approach is applied to other protocols and algorithms, such as Paxos and the Chandy-Lamport snapshot algorithm. Another piece of our future work is to come up with how to select the best one among several sets of learned axioms without knowing any oracles in advance and/or how to integrate multiple sets of learned axioms so as to obtain a better one.