Abstract
Techniques for inferring a regular language, in the form of a finite automaton, from a sufficiently large sample of accepted and nonaccepted input words, have been employed to construct models of software and hardware systems, for use, e.g., in test case generation. We intend to adapt these techniques to construct state machine models of entities of communication protocols. The alphabet of such state machines can be very large, since a symbol typically consists of a protocol data unit type with a number of parameters, each of which can assume many values. In typical algorithms for regular inference, the number of needed input words grows with the size of the alphabet and the size of the minimal DFA accepting the language. We therefore modify such an algorithm (Angluin’s algorithm) so that its complexity grows not with the size of the alphabet, but only with the size of a certain symbolic representation of the DFA. The main new idea is to infer, for each state, a partitioning of input symbols into equivalence classes, under the hypothesis that all input symbols in an equivalence class have the same effect on the state machine. Whenever such a hypothesis is disproved, equivalence classes are refined. We show that our modification retains the good properties of Angluin’s original algorithm, but that its complexity grows with the size of our symbolic DFA representation rather than with the size of the alphabet. We have implemented the algorithm; experiments on synthesized examples are consistent with these complexity results.
Supported in part by the Swedish Research Council, and by the FP6 Network of Excellence ARTIST2.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.): Model-Based Testing of Reactive Systems. LNCS, vol. 3472. Springer, Heidelberg (2005)
Ball, T., Rajamani, S.: The SLAM project: Debugging system software via static analysis. In: Proc. 29th ACM Symp. on Principles of Programming Languages, pp. 1–3 (2002)
Corbett, J., Dwyer, M., Hatcliff, J., Laubach, S., Pasareanu, C., Robby, Z.H.: Bandera: Extracting finite-state models from java source code. In: Proc. 22nd Int. Conf. on Software Engineering (2000)
Henzinger, T., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc.29th ACM Symp. on Principles of Programming Languages, pp. 58–70 (2002)
Holzmann, G.: Logic verification of ANSI-C code with SPIN. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 131–147. Springer, Heidelberg (2000)
Hagerer, A., Hungar, H., Niese, O., Steffen, B.: Model generation by moderated regular extrapolation. In: Kutsche, R.-D., Weber, H. (eds.) ETAPS 2002 and FASE 2002. LNCS, vol. 2306, pp. 80–95. Springer, Heidelberg (2002)
Hungar, H., Niese, O., Steffen, B.: Domain-specific optimization in automata learning. In: Proc.15th Int. Conf. on Computer Aided Verification (2003)
Groce, A., Peled, D., Yannakakis, M.: Adaptive model checking. In: Katoen, J.-P., Stevens, P. (eds.) ETAPS 2002 and TACAS 2002. LNCS, vol. 2280, pp. 357–370. Springer, Heidelberg (2002)
Peled, D., Vardi, M.Y., Yannakakis, M.: Black box checking. In: FORTE/PSTV, pp. 225–240. Kluwer, Dordrecht (1999)
Ammons, G., Bodik, R., Larus, J.: Mining specificatoins. In: Proc. 29th ACM Symp. on Principles of Programming Languages, pp. 4–16 (2002)
Cobleigh, J., Giannakopoulou, D., Pasareanu, C.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) ETAPS 2003 and TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003)
Angluin, D.: Learning regular sets from queries and counterexamples. Information and Computation 75, 87–106 (1987)
Balcázar, J., Díaz, J., Gavaldá, R.: Algorithms for learning finite automata from queries: A unified view. In: Advances in Algorithms, Languages, and Complexity, pp. 53–72. Kluwer, Dordrecht (1997)
Dupont, P.: Incremental regular inference. In: Miclet, L., de la Higuera, C. (eds.) ICGI 1996. LNCS, vol. 1147, pp. 222–237. Springer, Heidelberg (1996)
Gold, E.M.: Language identification in the limit. Information and Control 10, 447–474 (1967)
Kearns, M., Vazirani, U.: An Introduction to Computational Learning Theory. MIT Press, Cambridge (1994)
Rivest, R., Schapire, R.: Inference of finite automata using homing sequences. Information and Computation 103, 299–347 (1993)
Trakhtenbrot, B., Barzdin, J.: Finite automata: behaviour and synthesis. North-Holland, Amsterdam (1973)
Raffelt, H., Steffen, B., Berg, T.: Learnlib: a library for automata learning and experimentation. In: FMICS 2005, pp. 62–71. ACM Press, New York (2005)
Gold, E.M.: Complexity of automaton identification from given data. Information and Control 37, 302–320 (1978)
Blom, J., Jonsson, B.: Automated test generation for industrial erlang applications. In: Proc. 2003 ACM SIGPLAN workshop on Erlang, Uppsala, Sweden, pp. 8–14 (2003)
Garavel, H., Lang, F., Mateescu, R.: An overview of cadp (2002) Newsletter (2001)
Steffen, B., Margaria, T., Raffelt, H., Niese, O.: Efficient test-based model generation of legacy systems. In: HLDVT 2004, pp. 95–100. IEEE Computer Society Press, Los Alamitos (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berg, T., Jonsson, B., Raffelt, H. (2006). Regular Inference for State Machines with Parameters. In: Baresi, L., Heckel, R. (eds) Fundamental Approaches to Software Engineering. FASE 2006. Lecture Notes in Computer Science, vol 3922. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11693017_10
Download citation
DOI: https://doi.org/10.1007/11693017_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33093-6
Online ISBN: 978-3-540-33094-3
eBook Packages: Computer ScienceComputer Science (R0)