Advertisement

Using Language Inference to Verify Omega-Regular Properties

  • Abhay Vardhan
  • Koushik Sen
  • Mahesh Viswanathan
  • Gul Agha
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3440)

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.

References

  1. 1.
    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)CrossRefGoogle Scholar
  2. 2.
    Angluin, D.: Learning regular sets from queries and counterexamples. Inform. Comput. 75(2), 87–106 (1987)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    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)CrossRefGoogle Scholar
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    Bouajjani, A., Legay, A., Wolper, P.: Handling liveness properties in (ω-)regular model-checking. In: Proc. of Infinity 2004, London, UK (2004)Google Scholar
  6. 6.
    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)Google Scholar
  7. 7.
    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)Google Scholar
  8. 8.
    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)Google Scholar
  9. 9.
    Habermehl, P., Vojnar, T.: Regular model checking using inference of regular languages. In: Proc. of Infinity 2004, London, UK (2004)Google Scholar
  10. 10.
    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)CrossRefGoogle Scholar
  11. 11.
    LEVER. Learning to verify tool (2004), http://osl.cs.uiuc.edu/~vardhan/lever.html
  12. 12.
    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)CrossRefGoogle Scholar
  13. 13.
    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)Google Scholar
  14. 14.
    Thomas, W.: Automata on infinite objects. In: Leeuwen, J.V. (ed.) Handbook of Theoretical Computer Science, vol. B, pp. 133–191. Elsevier, Amsterdam (1990)Google Scholar
  15. 15.
    Touili, T.: Regular model checking using widening techniques. In: ENTCS, vol. 50. Elsevier, Amsterdam (2001)Google Scholar
  16. 16.
    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)CrossRefGoogle Scholar
  17. 17.
    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)CrossRefGoogle Scholar
  18. 18.
    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)

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Abhay Vardhan
    • 1
  • Koushik Sen
    • 1
  • Mahesh Viswanathan
    • 1
  • Gul Agha
    • 1
  1. 1.Dept. of Computer ScienceUniv. of Illinois at Urbana-ChampaignUSA

Personalised recommendations