Abstract
Active learning of timed languages is concerned with the inference of timed automata by observing some of the timed words in their languages. The learner can query for the membership of words in the language, or propose a candidate model and ask if it is equivalent to the target. The major difficulty of this framework is the inference of clock resets, which are central to the dynamics of timed automata but not directly observable.
Interesting first steps have already been made by restricting to the subclass of event-recording automata, where clock resets are tied to observations. In order to advance towards learning of general timed automata, we generalize this method to a new class, called reset-free event-recording automata, where some transitions may reset no clocks.
Central to our contribution is the notion of invalidity, and the algorithm and data structures to deal with it, allowing on-the-fly detection and pruning of reset hypotheses that contradict observations. This notion is a key to any efficient active-learning procedure for generic timed automata.
This work was partially funded by ANR project Ticktac (ANR-18-CE40-0015).
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
Notes
- 1.
In order to avoid overloading the explanation, we call the observation and graph partial because we do not mention some of the observations that would be necessary to have the implementation property.
References
An, J., Chen, M., Zhan, B., Zhan, N., Zhang, M.: Learning one-clock timed automata. In: Biere, A., Parker, D. (eds.) TACAS 2020. LNCS, vol. 12078, pp. 444–462. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-45190-5_25
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
Alur, R., Fix, L., Henzinger, T.A.: Event-clock automata: a determinizable class of timed automata. Theor. Comput. Sci. 211(1–2), 253–273 (1999)
Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87–106 (1987)
Angluin, D.: Queries and concept learning. Mach. Learn. 2(4), 319–342 (1987). https://doi.org/10.1023/A:1022821128753
Angluin, D.: Negative results for equivalence queries. Mach. Learn. 5, 121–150 (1990). https://doi.org/10.1023/A:1022692615781
Bertrand, N., Stainer, A., Jéron, T., Krichen, M.: A game approach to determinize timed automata. In: Hofmann, M. (ed.) FoSSaCS 2011. LNCS, vol. 6604, pp. 245–259. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-19805-2_17
Grinchtein, O., Jonsson, B., Pettersson, P.: Inference of event-recording automata using timed decision trees. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 435–449. Springer, Heidelberg (2006). https://doi.org/10.1007/11817949_29
Grinchtein, O.: Learning of timed systems. Ph.D. thesis, Uppsala University, Sweden (2008)
Henry, L., Jéron, T., Markey, N.: Active learning of timed automata with unobservable resets. Technical Report. arXiv:2007.01637, April 2020
Tappler, M., Aichernig, B.K., Larsen, K.G., Lorber, F.: Time to learn – learning timed automata from tests. In: André, É., Stoelinga, M. (eds.) FORMATS 2019. LNCS, vol. 11750, pp. 216–235. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-29662-9_13
Verwer, S., Weerdt, M., Witteveen, C.: Efficiently learning simple timed automata. In: Proceedings of the Second International Workshop on the Induction of Process Models at ECML PKDD, pp. 61–68 (2008)
Verwer, S., Weerdt, M., Witteveen, C.: Efficiently identifying deterministic real-time automata from labeled data. Mach. Learn. 86, 295–333 (2012). https://doi.org/10.1007/s10994-011-5265-4
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Henry, L., Jéron, T., Markey, N. (2020). Active Learning of Timed Automata with Unobservable Resets. In: Bertrand, N., Jansen, N. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2020. Lecture Notes in Computer Science(), vol 12288. Springer, Cham. https://doi.org/10.1007/978-3-030-57628-8_9
Download citation
DOI: https://doi.org/10.1007/978-3-030-57628-8_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-57627-1
Online ISBN: 978-3-030-57628-8
eBook Packages: Computer ScienceComputer Science (R0)