Using Language Inference to Verify Omega-Regular Properties

A novel machine learning based approach was proposed recently as a complementary technique to the acceleration based methods for verifying infinite state systems. In this method, the set of states satisfying a fixpoint property is learnt as opposed to being iteratively computed. We extend the machine learning based approach to verifying general

ω

-regular properties that include both safety and liveness. To achieve this, we first develop a new fixpoint based characterization for the verification of

ω

-regular properties. Using this characterization, we present a general framework for verifying infinite state systems. We then instantiate our approach to the context of regular model checking where states are represented as strings over a finite alphabet and the transition relation of the system is given as a finite state transducer; unlike previous learning based algorithms, we make no assumption about the transducer being length-preserving. Using Angluin’s L* algorithm for learning regular languages, we develop an algorithm for verification of

ω

-regular properties of such infinite state systems. The algorithm is a complete verification procedure for systems for whom the fixpoint can be represented as a regular set. We have implemented the technique in a tool called

Lever

and use it to analyze some examples.