research-article

Open access

Learning Nondeterministic Real-Time Automata

Authors:

Miaomiao ZhangAuthors Info & Claims

ACM Transactions on Embedded Computing Systems (TECS), Volume 20, Issue 5s

Article No.: 99, Pages 1 - 26

https://doi.org/10.1145/3477030

Published: 22 September 2021 Publication History

All formats PDF

Abstract

We present an active learning algorithm named NRTALearning for nondeterministic real-time automata (NRTAs). Real-time automata (RTAs) are a subclass of timed automata with only one clock which resets at each transition. First, we prove the corresponding Myhill-Nerode theorem for real-time languages. Then we show that there exists a unique minimal deterministic real-time automaton (DRTA) recognizing a given real-time language, but the same does not hold for NRTAs. We thus define a special kind of NRTAs, named residual real-time automata (RRTAs), and prove that there exists a minimal RRTA to recognize any given real-time language. This transforms the learning problem of NRTAs to the learning problem of RRTAs. After describing the learning algorithm in detail, we prove its correctness and polynomial complexity. In addition, based on the corresponding Myhill-Nerode theorem, we extend the existing active learning algorithm NL* for nondeterministic finite automata to learn RRTAs. We evaluate and compare the two algorithms on two benchmarks consisting of randomly generated NRTAs and rational regular expressions. The results show that NRTALearning generally performs fewer membership queries and more equivalence queries than the extended NL* algorithm, and the learnt NRTAs have much fewer locations than the corresponding minimal DRTAs. We also conduct a case study using a model of scheduling of final testing of integrated circuits.

References

[1]

Bernhard K. Aichernig, Andrea Pferscher, and Martin Tappler. 2020. From passive to active: Learning timed automata efficiently. In Proceedings of the 12th International Symposium NASA Formal Methods, NFM 2020(LNCS, Vol. 12229). Springer, 1–19.

Digital Library

[2]

Rajeev Alur and David L. Dill. 1994. A theory of timed automata. Theoretical Computer Science 126, 2 (1994), 183–235.

Digital Library

[3]

Rajeev Alur, P. Madhusudan, and Wonhong Nam. 2005. Symbolic compositional verification by learning assumptions. In Proceedings of the 17th International Conference on Computer Aided Verification, CAV 2005(LNCS, Vol. 3576). Springer, Heidelberg, 548–562.

Digital Library

[4]

Jie An, Mingshuai Chen, Bohua Zhan, Naijun Zhan, and Miaomiao Zhang. 2020. Learning one-clock timed automata. In Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2020(LNCS, Vol. 12078). Springer, Heidelberg, 444–462.

Digital Library

[5]

Jie An, Lingtai Wang, Bohua Zhan, Naijun Zhan, and Miaomiao Zhang. 2020. Learning real-time automata. SCIENCE CHINA Information Sciences (2020). https://www.sciengine.com/doi/10.1007/s11432-019-2767-4.In press.

[6]

Jie An, Naijun Zhan, Xiaoshan Li, Miaomiao Zhang, and Wang Yi. 2018. Model checking bounded continuous-time extended linear duration invariants. In Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC 2018. ACM, 81–90.

Digital Library

[7]

Dana Angluin. 1987. Learning regular sets from queries and counterexamples. Information and Computation 75, 2 (1987), 87–106.

Digital Library

[8]

Benedikt Bollig, Peter Habermehl, Carsten Kern, and Martin Leucker. 2009. Angluin-style learning of NFA. In Proceedings of the 21st International Joint Conference on Artificial Intelligence, IJCAI 2009. 1004–1009.

Digital Library

[9]

Filippo Bonchi and Damien Pous. 2013. Checking NFA equivalence with bisimulations up to congruence. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013. ACM, 457–468.

Digital Library

[10]

Ben Caldwell, Rachel Cardell-Oliver, and Tim French. 2016. Learning time delay mealy machines from programmable logic controllers. IEEE Trans Autom. Sci. Eng. 13, 2 (2016), 1155–1164. https://doi.org/10.1109/TASE.2015.2496242

[11]

Colin de la Higuera. 2010. Grammatical Inference: Learning Automata and Grammars. Cambridge University Press.

Digital Library

[12]

François Denis, Aurélien Lemay, and Alain Terlutte. 2001. Residual finite state automata. In Proceedings of the 18th Annual Symposium on Theoretical Aspects of Computer Science, STACS 2001(LNCS, Vol. 2010). Springer, Heidelberg, 144–157.

[13]

François Denis, Aurélien Lemay, and Alain Terlutte. 2004. Learning regular languages using RFSAs. Theoretical Computer Science 313, 2 (2004), 267–294.

Digital Library

[14]

Dorothy E. Denning and Giovanni Maria Sacco. 1981. Timestamps in key distribution protocols. Commun. ACM 24, 8 (1981), 533–536.

Digital Library

[15]

Catalin Dima. 2001. Real-time automata. Journal of Automata, Languages and Combinatorics 6, 1 (2001), 3–23.

[16]

Samuel Drews and Loris D'Antoni. 2017. Learning symbolic automata. In Proceedings of the 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017(LNCS, Vol. 10205). Springer, Heidelberg, 173–189.

[17]

Paul Fiterau-Brostean, Ramon Janssen, and Frits W. Vaandrager. 2016. Combining model learning and model checking to analyze TCP implementations. In Proceedings of the 28th International Conference on Computer Aided Verification, CAV 2016(LNCS, Vol. 9780). Springer, Heidelberg, 454–471.

[18]

Olga Grinchtein, Bengt Jonsson, and Martin Leucker. 2010. Learning of event-recording automata. Theoretical Computer Science 411, 47 (2010), 4029–4054.

Digital Library

[19]

Léo Henry, Thierry Jéron, and Nicolas Markey. 2020. Active learning of timed automata with unobservable resets. In Proceedings of the 18th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2020(LNCS, Vol. 12288). Springer, 144–160.

Digital Library

[20]

Xiangyu Jin, Jie An, Bohua Zhan, Naijun Zhan, and Miaomiao Zhang. 2021. Inferring nonlinear switched dynamical systems. Formal Aspects of Computing (2021).

Digital Library

[21]

Oded Maler and Amir Pnueli. 1995. On the learnability of infinitary regular sets. Information and Computation 118, 2 (1995), 316–326.

Digital Library

[22]

Ronald L. Rivest and Robert E. Schapire. 1993. Inference of finite automata using homing sequences. Information and Computation 103, 2 (1993), 299–347.

Digital Library

[23]

Jana Schmidt, Asghar Ghorbani, Andreas Hapfelmeier, and Stefan Kramer. 2013. Learning probabilistic real-time automata from multi-attribute event logs. Intelligent Data Analysis 17, 1 (2013), 93–123.

[24]

Miriam García Soto, Thomas A. Henzinger, Christian Schilling, and Luka Zeleznik. 2019. Membership-based synthesis of linear hybrid automata. In Proceedings of the 31st International Conference on Computer Aided Verification, CAV 2019(LNCS, Vol. 11561). Springer, Heidelberg, 297–314.

[25]

Martin Stigge, Pontus Ekberg, Nan Guan, and Wang Yi. 2011. The digraph real-time task model. In Proceedings of the 17th IEEE Real-Time and Embedded Technology and Applications Symposium, RTAS 2011. IEEE Computer Society, 71–80.

Digital Library

[26]

Martin Tappler, Bernhard K. Aichernig, Kim Guldstrand Larsen, and Florian Lorber. 2019. Time to learn - learning timed automata from tests. In Proceedings of the 17th International Conference on Formal Modeling and Analysis of Timed Systems, FORMATS 2019(LNCS, Vol. 11750). Springer, 216–235.

Digital Library

[27]

Frits W. Vaandrager. 2017. Model learning. Commun. ACM 60, 2 (2017), 86–95.

Digital Library

[28]

Frits W. Vaandrager, Roderick Bloem, and Masoud Ebrahimi. 2021. Learning mealy machines with one timer. In Proceedings of the 15th International Conference on Language and Automata Theory and Applications, LATA 2021(LNCS, Vol. 12638). Springer, 157–170.

Digital Library

[29]

Sicco Verwer. 2010. Efficient Identification of Timed Automata: Theory and practice. Ph.D. Dissertation. Delft University of Technology, Netherlands.

[30]

Sicco Verwer, Mathijs de Weerdt, and Cees Witteveen. 2009. One-clock deterministic timed automata are efficiently identifiable in the limit. In Proceedings of the 3rd International Conference on Language and Automata Theory and Applications, LATA 2009(LNCS, Vol. 5457). Springer, 740–751.

Digital Library

[31]

Sicco Verwer, Mathijs de Weerdt, and Cees Witteveen. 2011. The efficiency of identifying timed automata and the power of clocks. Information and Computation 209, 3 (2011), 606–625.

Digital Library

[32]

Sicco Verwer, Mathijs de Weerdt, and Cees Witteveen. 2012. Efficiently identifying deterministic real-time automata from labeled data. Machine Learning 86, 3 (2012), 295–333.

Digital Library

[33]

Sicco Verwer, Mathijs De Weerdt, and Cees Witteveen. 2007. An algorithm for learning real-time automata. Electrical Engineering Mathematics & Computer Science (2007).

[34]

Gail Weiss, Yoav Goldberg, and Eran Yahav. 2018. Extracting automata from recurrent neural networks using queries and counterexamples. In Proceedings of the 35th International Conference on Machine Learning, ICML 2018(PMLR, Vol. 80). PMLR, 5244–5253.

[35]

Gail Weiss, Yoav Goldberg, and Eran Yahav. 2019. Learning deterministic weighted automata with queries and counterexamples. In Proceedings of the 33rd Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019. 8558–8569.

Digital Library

Cited By

Lin YLi HFaccio D(2024)Human Multi-Activities Classification Using mmWave Radar: Feature Fusion in Time-Domain and PCANetSensors10.3390/s2416545024:16(5450)Online publication date: 22-Aug-2024
https://doi.org/10.3390/s24165450
Alhazmi AAlanazi MAlshehry AAlshahry SJaszek JDjukic CBrown AJackson KChodavarapu V(2024)Intelligent Millimeter-Wave System for Human Activity Monitoring for TelemedicineSensors10.3390/s2401026824:1(268)Online publication date: 2-Jan-2024
https://doi.org/10.3390/s24010268
Liu ALin YSundaresan K(2024)View-agnostic Human Exercise Cataloging with Single MmWave RadarProceedings of the ACM on Interactive, Mobile, Wearable and Ubiquitous Technologies10.1145/36785128:3(1-23)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678512
Show More Cited By

Index Terms

Learning Nondeterministic Real-Time Automata
1. Computer systems organization
  1. Real-time systems
    1. Real-time languages
2. Theory of computation
  1. Formal languages and automata theory
    1. Regular languages

Recommendations

Nondeterministic fuzzy automata

To handle fuzzy uncertainty in system modeling, nondeterministic finite automata have been generalized into fuzzy automata. After a reexamination of the notions of fuzzy automata in the literature, we ascertain that the fundamental property-...
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 ...
Converting two-way nondeterministic unary automata into simpler automata

We show that, on inputs of length exceeding 5n2, any n-state unary two-way nondeterministic finite automaton (2nfa) can be simulated by a (2n+2)-state quasi-sweeping 2nfa. Such a result, besides providing a “normal form” for 2nfa's, enables us to get a ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Embedded Computing Systems

ACM Transactions on Embedded Computing Systems Volume 20, Issue 5s

Special Issue ESWEEK 2021, CASES 2021, CODES+ISSS 2021 and EMSOFT 2021

October 2021

1367 pages

ISSN:1539-9087

EISSN:1558-3465

DOI:10.1145/3481713

Editor:
Tulika Mitra
National University of Singapore, Singapore

Issue’s Table of Contents

Copyright © 2021 Copyright held by the owner/author(s). Publication rights licensed to ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Journal Family

ACM Journals for the Design of Smart and Connected Systems

Publication History

Published: 22 September 2021

Accepted: 01 July 2021

Revised: 01 June 2021

Received: 01 April 2021

Published in TECS Volume 20, Issue 5s

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Refereed

Funding Sources

Deutsche Forschungsgemeinschaft
CAS Pioneer Hundred Talents Program
NSFC

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

20
Total Citations
View Citations
536
Total Downloads

Downloads (Last 12 months)199
Downloads (Last 6 weeks)42

Reflects downloads up to 14 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Lin YLi HFaccio D(2024)Human Multi-Activities Classification Using mmWave Radar: Feature Fusion in Time-Domain and PCANetSensors10.3390/s2416545024:16(5450)Online publication date: 22-Aug-2024
https://doi.org/10.3390/s24165450
Alhazmi AAlanazi MAlshehry AAlshahry SJaszek JDjukic CBrown AJackson KChodavarapu V(2024)Intelligent Millimeter-Wave System for Human Activity Monitoring for TelemedicineSensors10.3390/s2401026824:1(268)Online publication date: 2-Jan-2024
https://doi.org/10.3390/s24010268
Liu ALin YSundaresan K(2024)View-agnostic Human Exercise Cataloging with Single MmWave RadarProceedings of the ACM on Interactive, Mobile, Wearable and Ubiquitous Technologies10.1145/36785128:3(1-23)Online publication date: 9-Sep-2024
https://dl.acm.org/doi/10.1145/3678512
Feng YDai SZhang QWang ZZhang XZhou Y(2024)M3Pose: Multi-Person 3D Pose Estimation Using Sparse Millimeter-Wave Radar Point CloudsPattern Recognition and Computer Vision10.1007/978-981-97-8795-1_34(504-517)Online publication date: 18-Oct-2024
https://dl.acm.org/doi/10.1007/978-981-97-8795-1_34
Li ZChen HCai JXue Y(2024)Segmentation and Quality Assessment of Continuous Fitness Movements Based on VisionAdvanced Intelligent Computing Technology and Applications10.1007/978-981-97-5612-4_9(96-107)Online publication date: 5-Aug-2024
https://dl.acm.org/doi/10.1007/978-981-97-5612-4_9
Pei JCao ZWang G(2024)mmWave Radar Point Cloud Based Pose Estimation with Residual Blocks for Rehabilitation ExerciseIntelligent Networked Things10.1007/978-981-97-3948-6_7(65-74)Online publication date: 10-Jul-2024
https://doi.org/10.1007/978-981-97-3948-6_7
Zhang JLiu HXie XTong XLiu XLi K(2024)Personalized mmWave Signal Synthesis for Human SensingWireless Artificial Intelligent Computing Systems and Applications10.1007/978-3-031-71467-2_22(267-279)Online publication date: 14-Nov-2024
https://doi.org/10.1007/978-3-031-71467-2_22
Li WLiu RWang SCao DJiang WEskicioglu RHuang PPatwari N(2023)Egocentric Human Pose Estimation using Head-mounted mmWave RadarProceedings of the 21st ACM Conference on Embedded Networked Sensor Systems10.1145/3625687.3625799(431-444)Online publication date: 12-Nov-2023
https://dl.acm.org/doi/10.1145/3625687.3625799
Wu YChiang HShirmohammadi SHsu CZimmermann RShirmohammadi SGriwodz CHefeeda MWang M(2023)A Dataset of Food Intake Activities Using Sensors with Heterogeneous Privacy Sensitivity LevelsProceedings of the 14th ACM Multimedia Systems Conference10.1145/3587819.3592553(416-422)Online publication date: 8-Jun-2023
https://doi.org/10.1145/3587819.3592553
Paliwal ISolanki DJoshi V(2023)Better Utilization of NDFA Over DFA with the Existing Problems2023 IEEE International Conference on ICT in Business Industry & Government (ICTBIG)10.1109/ICTBIG59752.2023.10456171(1-5)Online publication date: 8-Dec-2023
https://doi.org/10.1109/ICTBIG59752.2023.10456171
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

HTML Format

View this article in HTML Format.

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 Article

Media

Figures

Other

Tables

View Issue’s Table of Contents