Abstract
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.
Chapter PDF
References
Abdulla, P.A., Jonsson, B., Nilson, M., d’Orso, J., Saksena, M.: Regular model checking for LTL(MSO). In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 348–360. Springer, Heidelberg (2004)
Angluin, D.: Learning regular sets from queries and counterexamples. Inform. Comput. 75(2), 87–106 (1987)
Bouajjani, A., Habermehl, P., Vojnar, T.: Abstract regular model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 372–386. Springer, Heidelberg (2004)
Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403–418. Springer, Heidelberg (2000)
Bouajjani, A., Legay, A., Wolper, P.: Handling liveness properties in (ω-)regular model-checking. In: Proc. of Infinity 2004, London, UK (2004)
Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional mucalculus. In: Proccedings of the First Annual Symposium on Logic in Computer Science, Washington, D.C, pp. 267–278. IEEE Computer Society Press, Los Alamitos (1986)
Emerson, E.A.: Temporal and modal logic. In: Leeuwen, J.V. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 995–1072. Elsevier, Amsterdam (1990)
Fribourg, L., Olsén, H.: Reachability sets of parametrized rings as regular languages. In: Proc. 2nd Int. Workshop on Verification of Infinite State Systems (INFINITY 1997). Elsevier Science, Amsterdam (1997)
Habermehl, P., Vojnar, T.: Regular model checking using inference of regular languages. In: Proc. of Infinity 2004, London, UK (2004)
Jonsson, B., Nilsson, M.: Transitive closures of regular relations for verifying infinite-state systems. In: Schwartzbach, M.I., Graf, S. (eds.) TACAS 2000. LNCS, vol. 1785, pp. 220–234. Springer, Heidelberg (2000)
LEVER. Learning to verify tool (2004), http://osl.cs.uiuc.edu/~vardhan/lever.html
Oncina, J., Garcia, P.: Inferring regular languages in polynomial update time. In: Pattern Recognition and Image Analysis. Series in Machine Perception and Artificial Intelligence, vol. 1, pp. 49–61. World Scientific, Singapore (1992)
Pnueli, A., Shahar, E.: Liveness and acceleration in parameterized verification. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855. Springer, Heidelberg (2000)
Thomas, W.: Automata on infinite objects. In: Leeuwen, J.V. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 133–191. Elsevier, Amsterdam (1990)
Touili, T.: Regular model checking using widening techniques. In: ENTCS, vol. 50. Elsevier, Amsterdam (2001)
Vardhan, A., Sen, K., Viswanathan, M., Agha, G.: Actively learning to verify safety for fifo automata. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 494–505. Springer, Heidelberg (2004)
Vardhan, A., Sen, K., Viswanathan, M., Agha, G.: Learning to verify safety properties. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 274–289. Springer, Heidelberg (2004)
Vardhan, A., Sen, K., Viswanathan, M., Agha, G.: Using language inference to verify omega-regular properties (2004), http://osl.cs.uiuc.edu/docs/omegaLearn2.pdf (full version)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Vardhan, A., Sen, K., Viswanathan, M., Agha, G. (2005). Using Language Inference to Verify Omega-Regular Properties. In: Halbwachs, N., Zuck, L.D. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2005. Lecture Notes in Computer Science, vol 3440. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-31980-1_4
Download citation
DOI: https://doi.org/10.1007/978-3-540-31980-1_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-25333-4
Online ISBN: 978-3-540-31980-1
eBook Packages: Computer ScienceComputer Science (R0)