Using language inference to verify omega-regular properties
By
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.
BibTeX
@inproceedings{conf/tacas/VardhanSVA05,
author = "Vardhan, Abhay and Sen, Koushik and Viswanathan, Mahesh
and Agha, Gul",
editor = "Halbwachs, Nicolas and Zuck, Lenore D.",
title = "Using Language Inference to Verify Omega-Regular
Properties",
booktitle = "TACAS",
crossref = "conf/tacas/2005",
ee = "http://dx.doi.org/10.1007/978-3-540-31980-1_4",
keywords = "formal methods",
pages = "45-60",
year = "2005",
}
@proceedings{conf/tacas/2005,
editor = "Halbwachs, Nicolas and Zuck, Lenore D.",
title = "Tools and Algorithms for the Construction and Analysis of
Systems, 11th International Conference, TACAS 2005, Held as Part
of the Joint European Conferences on Theory and Practice of
Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005, Proceedings",
isbn = "3-540-25333-5",
publisher = "Springer",
series = "Lecture Notes in Computer Science",
volume = "3440",
year = "2005",
}