Case studies on extracting the characteristics of the reachable states of state machines formalizing communication protocols with inductive logic programing

A distributed system DS can be formalized as a state machine 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 reachable states of M. To verify that DS enjoys a desired property, namely to prove that p is an invariant of M, we often need to find other invariants as lemmas, which is one of the most intellectual activities in Interactive Theorem Proving (ITP). For this end, our experiences on ITP tell us that it is useful to get better understandings of the reachable states R_M of M. We report on case studies in which Progol, an Inductive Logic Programming (ILP) system, has been used to extract the characteristics of the reachable states of state machines formalizing communication protocols. The case studies demonstrate that ILP has potential abilities to extract the characteristics of R_M.