Synthesize Models for Quantitative Analysis Using Automata Learning

  • Yu-Fang ChenEmail author
  • Hsiao-Chen Chung
  • Wen-Chi Hung
  • Ming-Hsien Tsai
  • Bow-Yaw Wang
  • Farn Wang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11704)


We apply a probably approximately correct learning algorithm for multiplicity automata to generate quantitative models of system behaviors with a statistical guarantee. Using the generated model, we give two analysis algorithms to estimate the minimum and average values of system behaviors. We show how to apply the learning algorithm even when the alphabet is not fixed. The experimental result is encouraging; the estimation made by our approach is almost as precise as the exact reference answer obtained by a brute-force enumeration.


  1. 1.
    Android Studio: The Monkey tester (2017). Accessed 01 August 2017
  2. 2.
    Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Angluin, D.: Queries and concept learning. Mach. Learn. 2(4), 319–342 (1988)MathSciNetGoogle Scholar
  4. 4.
    Beimel, A., Bergadano, F., Bshouty, N.H., Kushilevitz, E., Varricchio, S.: Learning functions represented as multiplicity automata. JACM 47(3), 506–530 (2000)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Bergadano, F., Varricchio, S.: Learning behaviors of automata from multiplicity and equivalence queries. SIAM J. Comput. 25(6), 1268–1280 (1996)MathSciNetCrossRefGoogle Scholar
  6. 6.
    Berstel, J., Reutenauer, C.: Rational Series and Their Language. Monographs in Theoretical Computer Science. An EATCS Series, vol. 12. Springer, Heidelberg (1988)CrossRefGoogle Scholar
  7. 7.
    Boggs, P.T., Tolle, J.W.: Sequential quadratic programming. Acta Numerica 4, 1–51 (1995)MathSciNetCrossRefGoogle Scholar
  8. 8.
    Carlyle, J., Paz, A.: Realizations by stochastic finite automata. J. Comput. Syst. Sci. 5(1), 26–40 (1971)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Chen, Y.F., et al.: PAC learning-based verification and model synthesis. In: ICSE, pp. 714–724 (2016)Google Scholar
  10. 10.
    Fliess, M.: Matrices de Hankel. J. Math. Pures Appl. 53(9), 197–222 (1974)MathSciNetzbMATHGoogle Scholar
  11. 11.
    Goldreich, O., Goldwasser, S., Ron, D.: Property testing and its connection to learning and approximation. JACM 45(4), 653–750 (1998)MathSciNetCrossRefGoogle Scholar
  12. 12.
    Herd, B., Miles, S., McBurney, P., Luck, M.: Quantitative analysis of multiagent systems through statistical model checking. In: Baldoni, M., Baresi, L., Dastani, M. (eds.) EMAS 2015. LNCS (LNAI), vol. 9318, pp. 109–130. Springer, Cham (2015). Scholar
  13. 13.
    Kwiatkowska, M.: Quantitative verification: models, techniques and tools. In: ESEC/FSE, pp. 449–458. ACM (2007)Google Scholar
  14. 14.
    Legay, A., Delahaye, B., Bensalem, S.: Statistical model checking: an overview. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol. 6418, pp. 122–135. Springer, Heidelberg (2010). Scholar
  15. 15.
    Nesterov, Y.: Squared functional systems and optimization problems. In: Frenk, H., Roos, K., Terlaky, T., Zhang, S. (eds.) High Performance Optimization. Applied Optimization, vol. 33, pp. 405–440. Springer, Boston (2000). Scholar
  16. 16.
    Ohnishi, H., Seki, H., Kasami, T.: A polynomial time learning algorithm for recognizable series. IEICE Trans. Inf. Syst. 77(10), 1077–1085 (1994)Google Scholar
  17. 17.
    Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202–215. Springer, Heidelberg (2004). Scholar
  18. 18.
    Silberschatz, A., Galvin, P.B., Gagne, G.: Operating System Concepts, 8th edn. Wiley Publishing, Hoboken (2008)zbMATHGoogle Scholar
  19. 19.
    Valiant, L.G.: A theory of the learnable. CACM 27(11), 1134–1142 (1984)CrossRefGoogle Scholar
  20. 20.
    Walkinshaw, N.: Assessing test adequacy for black-box systems without specifications. In: Wolff, B., Zaïdi, F. (eds.) ICTSS 2011. LNCS, vol. 7019, pp. 209–224. Springer, Heidelberg (2011). Scholar
  21. 21.
    Zuliani, P., Platzer, A., Clarke, E.M.: Bayesian statistical model checking with application to stateflow/simulink verification. FMSD 43(2), 338–367 (2013)zbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  • Yu-Fang Chen
    • 1
    Email author
  • Hsiao-Chen Chung
    • 1
  • Wen-Chi Hung
    • 1
    • 2
  • Ming-Hsien Tsai
    • 1
  • Bow-Yaw Wang
    • 1
  • Farn Wang
    • 2
  1. 1.Institute of Information ScienceAcademia SinicaTaipeiTaiwan
  2. 2.Graduate Institute of Electronic EngineeringNational Taiwan UniversityTaipeiTaiwan

Personalised recommendations