微信服务号

微信订阅号

2025年3月24日 12:21 星期一
首页 > 过刊浏览>2022年第33卷第8期 >2797-2814. DOI:10.13328/j.cnki.jos.006599
PDF HTML阅读 XML下载 导出引用 引用提醒
运用时间分类树的确定单时钟时间自动机学习
作者:
作者简介:

米钧日(1995－),男,硕士生,主要研究领域为组合验证,时间自动机理论,模型学习;
安杰(1990－),男,博士,主要研究领域为形式化方法,机器学习,模型学习,系统识别;
张苗苗(1971－),女,博士,研究员,博士生导师,主要研究领域为智能系统学习,人工智能的形式化验证,模型学习和验证;
杜博闻(1991－),男,博士生,主要研究领域为人工智能,智能系统,移动计算与软件工程.

通讯作者:

张苗苗,E-mail:miaomiao@tongji.edu.cn

中图分类号:

TP311

基金项目:

国家自然科学基金(61972284,62032019)


Learning Deterministic One-clock Timed Automata Based on Timed Classification Tree
Author:
  • 摘要
    • | |
  • 访问统计
    • |
  • 参考文献 [30]
    • |
  • 相似文献 [20]
    • | | |
  • 文章评论
    摘要:

    时间自动机的模型学习算法旨在通过提供输入和观察输出构建软硬件系统的形式化模型.确定性单时钟时间自动机的学习是其中的一个重要研究方向,但是该算法具有一定的局限性,在状态较多时学习速度较慢,很难应用到复杂的系统中.由此,提出了一种改进的学习算法,使用逻辑时间分类树代替逻辑时间观察表作为学习算法的内部数据结构,有效地减少了成员查询次数,降低了算法的空间复杂度,并能够高效率地构建假设自动机.最后进行了相关实验,实验结果表明,提出的改进算法减少了60%左右的成员查询和5%左右的等价查询.同时在该实验中,改进算法的学习速度最高可提高45倍以上.

    Abstract:

    Model learning of timed automata (TA) aims to build a formal model of software and hardware systems by external inputs and outputs. Learning of deterministic one-clock TA is one of the important research directions, but current algorithm has some limitations and is difficult to be applied to complex systems. Therefore, an improved learning algorithm is proposed, which uses logical-time classification tree instead of logical-time observation table as the internal data structure of the learning algorithm, effectively reducing the number of membership queries and the space complexity of the algorithm. In addition, it can efficiently construct hypothetical automata. Finally, relevant experiments have been carried out, and the experimental results show that the improved algorithm proposed in this study reduces the number of member queries by 60% and the number of equivalent queries by 5%. At the same time, in this experiment, the learning speed of the improved algorithm can be increased by more than 50 times at most.

    参考文献
    [1] Angluin D.Learning regular sets from queries and counterexamples.Information&Computation, 1987, 75(2):87-106.
    [2] Aarts F, Kuppens H, Tretmans GJ, et al.Improving active mealy machine learning for protocol conformance testing.Machine Learning, 2014, 96(1-2):189-224.
    [3] Shahbaz M, Groz R.Inferring mealy machines.In:Proc.of the 2nd World Congress on Formal Methods.2009.207-222.
    [4] Isberner M, Howar F, Steffen B.The open-source learnlib-A framework for active automata learning.In:Proc.of the 27th Int'l Conf.on Computer Aided Verification (CAV).2015.487-495.
    [5] Bollig B, Habermehl P, Kern C, et al.Angluin-style learning of NFA.In:Proc.of the 21st Int'l Joint Conf.on Artificial Intelligence (IJCAI).2009.1004-1009.
    [6] Drews S, D'Antoni L.Learning symbolic automata.In:Proc.of the 23rd Int'l Conf.on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).2017.173-189.
    [7] Maler O, Mens I.Learning regular languages over large alphabets.In:Proc.of the 20th Int'l Conf.on Tools and Algorithms for the Construction and Analysis of Systems (TACAS).2014.485-499.
    [8] Argyros G, D'Ani L.The learnability of symbolic automata.In:Proc.of the 30th Int'l Conf.on Computer Aided Verification (CAV).2018.427-445.
    [9] Howar F, Steffen B, Jonsson B, et al.Inferring canonical register automata.In:Proc.of the 13th Int'l Conf.on Verification, Model Checking, and Abstract Interpretation (VMCAI).2012.251-266.
    [10] Cassel S, Howar F, Jonsson B, et al.Active learning for extended finite state machines.Formal Aspects of Computing, 2016, 28(2):233-263.
    [11] Aarts F, Fiterau-Brostean P, Kuppens H, et al.Learning register automata with fresh value generation.In:Proc.of the 12th Int'l Colloquium on Theoretical Aspects of Computing (ICTAC).2015.165-183.
    [12] Farzan A, Chen Y, Clarke EM, et al.Extending automated compositional verification to the full class of omega-regular languages.In:Proc.of the Int'l Conf.on Tools&Algorithms for the Construction&Analysis of Systems.2009.
    [13] Li Y, Chen YF, Zhang L, et al.A novel learning algorithm for Büchi automata based on family of DFAs and classification trees.Information and Computation, 2020(2), 104678.
    [14] Tappler M, Aichernig BK, Bacci G, et al.L*-based learning of markov decision processes (Extended Version).In:Proc.of the Formal Methods-The Next 30 Years-Third World Congress (FM 2019).LNCS 11800, 2019.651-669.
    [15] Wang J, Zhan N, Feng X, et al.Overview of formal methods.Ruan Jian Xue Bao/Journal of Software, 2019, 30(1):33-61(in Chinese with English abstract).http://www.jos.org.cn/9825-1000/5652.htm[doi:10.13328/j.cnki.jos.005652].
    [16] An J, Wang L, Zhan B, et al.Learning real-time automata.SCIENCE CHINA Information Sciences, 2020, 10.
    [17] An J, Chen M, Zhan B, et al.Learning one-clock timed automata.In:Proc.of the Int'l Conf.on Tools and Algorithms for the Construction and Analysis of Systems.Cham:Springer, 2020.444-462.
    [18] Shen W, An J, Zhan B, et al.PAC learning of deterministic one-clock timed automata.In:Proc.of the Int'l Conf.on Formal Engineering Methods.Cham:Springer, 2020.129-146.
    [19] Isberner M, Howar F, Steffen B.The TTT algorithm:A redundancy-free approach to active automata learning.In:Proc.of the 5th Int'l Conf.on Runtime Verification (RV).2014.307-322.
    [20] Grinchtein O, Jonsson B, Pettersson P.Inference of eventrecording automata using timed decision trees.In:Proc.of the Int'l Conf.on Concur-concurrency Theory.Berlin, Heidelberg:Springer, 2006.
    [21] Rivest RL, Schapire RE.Inference of finite automata using homing sequences.Information&Computation, 1993, 103(2):299-347.
    [22] Argyros G, Stais I, Kiayias A, et al.Back in black:Towards formal, black box analysis of sanitizers and filters.In:Proc.of the 2016 IEEE Symp.on Security and Privacy (SP).IEEE, 2016.
    [23] Vaandrager FW.Model learning.Communications of the ACM, 2017, 60(2):86-95.
    [24] Verwer S, de Weerdt M, Witteveen C.Efficiently identifying deterministic real-time automata from labeled data.Machine Learning, 2012, 86(3):295-333.
    [25] Verwer S, de Weerdt M, Witteveen C.The efficiency of identifying timed automata and the power of clocks.Information&Computation, 2011, 209(3):606-625.
    [26] Grinchtein O, Jonsson B, Leucker M.Learning of event-recording automata.Theoretical Computer Science, 2010, 411(47):4029-4054.
    [27] Henry L, Jéron T, Markey N.Active learning of timed automata with unobservable resets.In:Proc.of the 18th Int'l Conf.on Formal Modeling and Analysis of Timed Systems (FORMATS).2020.144-160.
    [28] Vaandrager FW, Bloem R, Ebrahimi M.Learning mealy machines with one timer.In:Proc.of the 15th Int'l Conf.on Language and Automata Theory and Applications (LATA).2021.157-170.
    附中文参考文献:
    [15] 王戟,詹乃军,冯新宇,刘志明.形式化方法概貌.软件学报, 2019, 30(1):33-61.http://www.jos.org.cn/1000-9825/5652.htm[doi:10.13328/j.cnki.jos.005652]
    引证文献
    网友评论
    网友评论
    分享到微博
    发 布
引用本文

米钧日,张苗苗,安杰,杜博闻.运用时间分类树的确定单时钟时间自动机学习.软件学报,2022,33(8):2797-2814

复制
分享
文章指标
  • 点击次数:
  • 下载次数:
  • HTML阅读次数:
  • 引用次数:
历史
  • 收稿日期:2021-09-26
  • 最后修改日期:2021-10-14
  • 在线发布日期: 2022-01-28
  • 出版日期: 2022-08-06
文章二维码
友情链接:中国科学院软件研究所中国计算机学会中国科学院国家自然科学基金委员会CCF数字图书馆Int'l J of Softw Info计算机系统应用
您是第19727817位访问者
版权所有：中国科学院软件研究所 京ICP备05046678号-3
地址：北京市海淀区中关村南四街4号,邮政编码：100190
电话：010-62562563 传真：010-62562533 Email：jos@iscas.ac.cn
技术支持：北京勤云科技发展有限公司

京公网安备 11040202500063号