Article

From Passive to Active: Learning Timed Automata Efficiently

Authors:

Bernhard K. Aichernig,

Andrea Pferscher,

Martin TapplerAuthors Info & Claims

NASA Formal Methods: 12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11–15, 2020, Proceedings

Pages 1 - 19

https://doi.org/10.1007/978-3-030-55754-6_1

Published: 11 May 2020 Publication History

Abstract

Model-based testing is a promising technique for quality assurance. In practice, however, a model is not always present. Hence, model learning techniques attain increasing interest. Still, many learning approaches can only learn relatively simple types of models and advanced properties like time are ignored in many cases. In this paper we present an active model learning technique for timed automata. For this, we build upon an existing passive learning technique for real-timed systems. Our goal is to efficiently learn a timed system while simultaneously minimizing the set of training data. For evaluation we compared our active to the passive learning technique based on 43 timed systems with up to 20 locations and multiple clock variables. The results of

18 060

experiments show that we require only 100 timed traces to adequately learn a timed system. The new approach is up to 755 times faster.

References

[1]

Aichernig BK et al. Seidl M, Tillmann N, et al. Model-based mutation testing of an industrial measurement device Tests and Proofs 2014 Cham Springer 1-19

[2]

Aichernig BK, Brandl H, Jöbstl E, and Krenn W UML in action: a two-layered interpretation for testing ACM SIGSOFT Softw. Eng. Notes 2011 36 1 1-8

[3]

Aichernig BK, Lorber F, and Ničković D Veanes M and Viganò L Time for mutants — model-based mutation testing with timed automata Tests and Proofs 2013 Heidelberg Springer 20-38

[4]

Aichernig BK and Tappler M Barrett C, Davies M, and Kahsai T Learning from faults: mutation testing in active automata learning NASA Formal Methods 2017 Cham Springer 19-34

[5]

Alur R and Dill DL A theory of timed automata Theor. Comput. Sci. 1994 126 2 183-235

[6]

Alur R, Fix L, and Henzinger TA Event-clock automata: a determinizable class of timed automata Theor. Comput. Sci. 1999 211 1–2 253-273

[7]

Angluin D Learning regular sets from queries and counterexamples Inf. Comput. 1987 75 2 87-106

[8]

Asarin, E., Maler, O., Pnueli, A., Sifakis, J.: Controller synthesis for timed automata. IFAC Proc. 31(18), 447–452 (1998)., http://www.sciencedirect.com/science/article/pii/S1474667017420325, Special issue on the 5th IFAC Conference on System Structure and Control 1998 (SSC 1998), Nantes, France, 8–10 July

[9]

Behrmann G, David A, and Larsen KG Bernardo M and Corradini F A tutorial on Uppaal Formal Methods for the Design of Real-Time Systems 2004 Heidelberg Springer 200-236

[10]

Berg T, Grinchtein O, Jonsson B, Leucker M, Raffelt H, and Steffen B Cerioli M On the correspondence between conformance testing and regular inference Fundamental Approaches to Software Engineering 2005 Heidelberg Springer 175-189

[11]

Bornot S, Sifakis J, and Tripakis S de Roever W-P, Langmaack H, and Pnueli A Modeling urgency in timed systems Compositionality: The Significant Difference 1998 Heidelberg Springer 103-129

[12]

Dima C Real-time automata J. Autom. Lang. Comb. 2001 6 1 3-23

[13]

Grinchtein O, Jonsson B, and Leucker M Learning of event-recording automata Theor. Comput. Sci. 2010 411 47 4029-4054

[14]

Grinchtein O, Jonsson B, and Pettersson P Baier C and Hermanns H Inference of event-recording automata using timed decision trees CONCUR 2006 – Concurrency Theory 2006 Heidelberg Springer 435-449

[15]

Hessel A, Larsen KG, Nielsen B, Pettersson P, and Skou A Petrenko A and Ulrich A Time-optimal real-time test case generation using Uppaal Formal Approaches to Software Testing 2004 Heidelberg Springer 114-130

[16]

Koza, J.R.: Genetic Programming: On the Programming of Computers by Means of Natural Selection. Complex Adaptive Systems. MIT Press (1993). ISBN 978-0-262-11170-6

[17]

Lin S-W, André É, Dong JS, Sun J, and Liu Y Bultan T and Hsiung P-A An efficient algorithm for learning event-recording automata Automated Technology for Verification and Analysis 2011 Heidelberg Springer 463-472

[18]

Mao H, Chen Y, Jaeger M, Nielsen TD, Larsen KG, and Nielsen B Learning deterministic probabilistic automata from a model checking perspective Mach. Learn. 2016 105 2 255-299

[19]

de Matos Pedro A, Crocker PA, and de Sousa SM Margaria T and Steffen B Learning stochastic timed automata from sample executions Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change 2012 Heidelberg Springer 508-523

[20]

Mediouni BL, Nouri A, Bozga M, and Bensalem S Barrett C, Davies M, and Kahsai T Improved learning for stochastic timed models by state-merging algorithms NASA Formal Methods 2017 Cham Springer 178-193

[21]

Pastore, F., Micucci, D., Mariani, L.: Timed k-tail: automatic inference of timed automata. In: 2017 IEEE International Conference on Software Testing, Verification and Validation, ICST 2017, Tokyo, Japan, 13–17 March 2017, pp. 401–411. IEEE Computer Society (2017)., http://ieeexplore.ieee.org/xpl/mostRecentIssue.jsp?punumber=7922464

[22]

Peled DA, Vardi MY, and Yannakakis M Black box checking J. Autom. Lang. Comb. 2002 7 2 225-246

[23]

Pferscher, A.: Active model learning of timed automata via genetic programming. Master’s thesis, Graz University of Technology, Graz, Austria (2019). https://diglib.tugraz.at/active-model-learning-of-timed-automata-via-genetic-programming-2019

[24]

Pferscher, A., Tappler, M.: Supplemental materials for “From passive to active: learning timed automata efficiently” (2020)., https://figshare.com/articles/Supplemental_Materials_for_From_Passive_to_Active_Learning_Timed_Automata_Efficiently_/9976211/1

[25]

García Soto M, Henzinger TA, Schilling C, and Zeleznik L Dillig I and Tasiran S Membership-based synthesis of linear hybrid automata Computer Aided Verification 2019 Cham Springer 297-314

[26]

Springintveld J, Vaandrager FW, and D’Argenio PR Testing timed automata Theor. Comput. Sci. 2001 254 1–2 225-257

[27]

Tappler M, Aichernig BK, Larsen KG, and Lorber F André É and Stoelinga M Time to learn – learning timed automata from tests Formal Modeling and Analysis of Timed Systems 2019 Cham Springer 216-235

[28]

Tretmans J Hierons RM, Bowen JP, and Harman M Model based testing with labelled transition systems Formal Methods and Testing 2008 Heidelberg Springer 1-38

[29]

Utting M, Pretschner A, and Legeard B A taxonomy of model-based testing approaches Softw. Test. Verification Reliab. 2012 22 5 297-312

[30]

Verwer, S., de Weerdt, M., Witteveen, C.: An algorithm for learning real-time automata. In: Benelearn 2007: Proceedings of the Annual Machine Learning Conference of Belgium and the Netherlands, Amsterdam, The Netherlands, 14–15 May 2007, pp. 128–135 (2007)

[31]

Verwer S, de Weerdt M, and Witteveen C Sempere JM and García P A likelihood-ratio test for identifying probabilistic deterministic real-time automata from positive data Grammatical Inference: Theoretical Results and Applications 2010 Heidelberg Springer 203-216

[32]

Walkinshaw N, Derrick J, and Guo Q Cavalcanti A and Dams DR Iterative refinement of reverse-engineered models by model-based testing FM 2009: Formal Methods 2009 Heidelberg Springer 305-320

Cited By

Teng YZhang MAn J(2024)Learning Deterministic Multi-Clock Timed AutomataProceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3641513.3650124(1-11)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3641513.3650124
Kogel PSchwabe WGlesner S(2024)MMLT/ik: Efficiently Learning Mealy Machines with Local Timers by Using Imprecise Symbol FiltersQuantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems10.1007/978-3-031-68416-6_9(143-159)Online publication date: 10-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-68416-6_9
Aichernig BTappler MWallner F(2023)Benchmarking Combinations of Learning and Testing Algorithms for Automata LearningFormal Aspects of Computing10.1145/360536036:1(1-37)Online publication date: 21-Jun-2023
https://dl.acm.org/doi/10.1145/3605360
Show More Cited By

Index Terms

From Passive to Active: Learning Timed Automata Efficiently
1. General and reference

Index terms have been assigned to the content through auto-classification.

Recommendations

AALpy: An Active Automata Learning Library
Automated Technology for Verification and Analysis
Abstract
AALpy is an extensible open-source Python library providing efficient implementations of active automata learning algorithms for deterministic, non-deterministic, and stochastic systems. We put a special focus on the conformance testing aspect in ...
AALpy: an active automata learning library
Abstract
AALpy is an extensible open-source Python library providing efficient implementations of active automata learning algorithms for deterministic, non-deterministic, and stochastic systems. We put a special focus on the conformance testing aspect in ...
Learning of event-recording automata

In regular inference, a regular language is inferred from answers to a finite set of membership queries, each of which asks whether the language contains a certain word. One of the most well-known regular inference algorithms is the L^* algorithm due to ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

NASA Formal Methods: 12th International Symposium, NFM 2020, Moffett Field, CA, USA, May 11–15, 2020, Proceedings

May 2020

447 pages

ISBN:978-3-030-55753-9

DOI:10.1007/978-3-030-55754-6

Editors:
Ritchie Lee
NASA Ames Research Center, Moffett Field, CA, USA
,
Susmit Jha
SRI International, Menlo Park, CA, USA
,
Anastasia Mavridou
KBR Inc., NASA Ames Research Center, Moffett Field, CA, USA
,
Dimitra Giannakopoulou
NASA Ames Research Center, Moffett Field, CA, USA

© Springer Nature Switzerland AG 2020.

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 11 May 2020

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

15
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Teng YZhang MAn J(2024)Learning Deterministic Multi-Clock Timed AutomataProceedings of the 27th ACM International Conference on Hybrid Systems: Computation and Control10.1145/3641513.3650124(1-11)Online publication date: 14-May-2024
https://dl.acm.org/doi/10.1145/3641513.3650124
Kogel PSchwabe WGlesner S(2024)MMLT/ik: Efficiently Learning Mealy Machines with Local Timers by Using Imprecise Symbol FiltersQuantitative Evaluation of Systems and Formal Modeling and Analysis of Timed Systems10.1007/978-3-031-68416-6_9(143-159)Online publication date: 10-Sep-2024
https://dl.acm.org/doi/10.1007/978-3-031-68416-6_9
Aichernig BTappler MWallner F(2023)Benchmarking Combinations of Learning and Testing Algorithms for Automata LearningFormal Aspects of Computing10.1145/360536036:1(1-37)Online publication date: 21-Jun-2023
https://dl.acm.org/doi/10.1145/3605360
Kogel PKlös VGlesner S(2023)Learning Mealy Machines with Local TimersFormal Methods and Software Engineering10.1007/978-981-99-7584-6_4(47-64)Online publication date: 21-Nov-2023
https://dl.acm.org/doi/10.1007/978-981-99-7584-6_4
Bruyère VPérez GStaquet GVaandrager F(2023)Automata with TimersFormal Modeling and Analysis of Timed Systems10.1007/978-3-031-42626-1_3(33-49)Online publication date: 19-Sep-2023
https://dl.acm.org/doi/10.1007/978-3-031-42626-1_3
Waga M(2023)Active Learning of Deterministic Timed Automata with Myhill-Nerode Style CharacterizationComputer Aided Verification10.1007/978-3-031-37706-8_1(3-26)Online publication date: 17-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-37706-8_1
Dierl SHowar FKauffman SKristjansen MGuldstrand Larsen KLorber FMauritz M(2023)Learning Symbolic Timed Models from Concrete Timed DataNASA Formal Methods10.1007/978-3-031-33170-1_7(104-121)Online publication date: 16-May-2023
https://dl.acm.org/doi/10.1007/978-3-031-33170-1_7
Yang XBeg OKenigsberg MJohnson T(2022)A Framework for Identification and Validation of Affine Hybrid Automata from Input-Output TracesACM Transactions on Cyber-Physical Systems10.1145/34704556:2(1-24)Online publication date: 11-Apr-2022
https://dl.acm.org/doi/10.1145/3470455
Pferscher AAichernig B(2022)Fingerprinting and analysis of Bluetooth devices with automata learningFormal Methods in System Design10.1007/s10703-023-00425-y61:1(35-62)Online publication date: 1-Aug-2022
https://dl.acm.org/doi/10.1007/s10703-023-00425-y
Xu RAn JZhan B(2022)Active Learning of One-Clock Timed Automata Using Constraint SolvingAutomated Technology for Verification and Analysis10.1007/978-3-031-19992-9_16(249-265)Online publication date: 25-Oct-2022
https://dl.acm.org/doi/10.1007/978-3-031-19992-9_16
Show More Cited By

View Options

View options

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents