Abstract
We present an algorithm for inferring a timed-automaton model of a system from information obtained by observing its external behavior. Since timed automata can not in general be determinized, we restrict our attention to systems that can be described by deterministic event-recording automata. In previous work we have presented algorithms for event-recording automata that satisfy the restriction that there is at most one transition per alphabet symbol from each state. This restriction was lifted in subsequent work by an algorithm based on the region graph.
In this paper, we extend previous work by considering the full class of event-recording automata, while still avoiding to base it on the (usually prohibitively large) region graph. Our construction deviates from previous work on inference of automata in that it first constructs a so called timed decision tree from observations of system behavior, which is thereafter folded into an automaton.
This work was supported in part by the Swedish Research Council, by the European Network of Excellence ARTIST2, and by the European Research Training Network Games.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126, 183–235 (1994)
Alur, R., Fix, L., Henzinger, T.: Event-clock automata: A determinizable class of timed automata. Theoretical Computer Science 211, 253–273 (1999)
Angluin, D.: Learning regular sets from queries and counterexamples. Information and Computation 75, 87–106 (1987)
Balcázar, J.L., 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)
Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: UPPAAL: a tool suite for the automatic verification of real-time systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996)
Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: A model-checking tool for real-time systems. In: Hu, A.J., Vardi, M.Y. (eds.) CAV 1998. LNCS, vol. 1427, pp. 546–550. Springer, Heidelberg (1998)
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)
Corbett, J., Dwyer, M., Hatcliff, J., Laubach, S., Pasareanu, C., Roby, Zheng, H.: Bandera: Extracting finite-state models from java source code. In: Proc. 22nd Int. Conf. on Software Engineering (June 2000)
Fernandez, J.-C., Jard, C., Jéron, T., Viho, C.: An experiment in automatic generation of test suites for protocols with verification technology. Science of Computer Programming 29 (1997)
Gold, E.M.: Language identification in the limit. Information and Control 10, 447–474 (1967)
Grinchtein, O., Jonsson, B., Leucker, M.: Learning of Event-Recording Automata. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 379–395. Springer, Heidelberg (2004)
Grinchtein, O., Jonsson, B., Leucker, M.: Inference of timed transition systems. ENCS 138(3), 87–99 (2005)
Groce, A., Peled, D., Yannakakis, M.: Adaptive Model Checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, p. 357. Springer, Heidelberg (2002)
Hagerer, A., Hungar, H., Niese, O., Steffen, B.: Model Generation by Moderated Regular Extrapolation. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 80–95. Springer, Heidelberg (2002)
Harel, D., Lachover, H., Naamad, A., Pnueli, A., Politi, M., Sherman, R., Shtull-Trauring, A., Trakhtenbrot, M.: STATEMATE: A working environment for the development of complex reactive systems. IEEE Trans. on Software Engineering 16(4), 403–414 (1990)
Henzinger, T., Manna, Z., Pnueli, A.: Temporal proof methodologies for timed transition systems. Information and Computation 112, 173–337 (1994)
Henzinger, T., Raskin, J.-F., Schobbens, P.-Y.: The Regular Real-Time Languages. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 580–591. Springer, Heidelberg (1998)
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)
Hungar, H., Niese, O., Steffen, B.: Domain-specific optimization in automata learning. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 315–327. Springer, Heidelberg (2003)
Kearns, M., Vazirani, U.: An Introduction to Computational Learning Theory. MIT Press, Cambridge (1994)
Maler, O., Pnueli, A.: On recognizable timed languages. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol. 2987, pp. 348–362. Springer, Heidelberg (2004)
Rivest, R., Schapire, R.: Inference of finite automata using homing sequences. Information and Computation 103, 299–347 (1993)
Schmitt, M., Ebner, M., Grabowski, J.: Test generation with autolink and testcomposer. In: Proc. 2nd Workshop of the SDL Forum Society on SDL and MSC - SAM 2000 (June 2000)
Springintveld, J., Vaandrager, F.: Minimizable timed automata. In: Jonsson, B., Parrow, J. (eds.) FTRTFT 1996. LNCS, vol. 1135, pp. 130–147. Springer, Heidelberg (1996)
Wilke, T.: Specifying timed state sequences in powerful decidable logics and timed automata. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 694–715. Springer, Heidelberg (1994)
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
Grinchtein, O., Jonsson, B., Pettersson, P. (2006). Inference of Event-Recording Automata Using Timed Decision Trees. In: Baier, C., Hermanns, H. (eds) CONCUR 2006 – Concurrency Theory. CONCUR 2006. Lecture Notes in Computer Science, vol 4137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11817949_29
Download citation
DOI: https://doi.org/10.1007/11817949_29
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-37376-6
Online ISBN: 978-3-540-37377-3
eBook Packages: Computer ScienceComputer Science (R0)