运用时间分类树的确定单时钟时间自动机学习-米钧日，张苗苗，安杰，杜博闻.pdf

上善若水

264

19页

0次

2022-05-19

免费下载

软件学报 ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn

Journal of Software, [doi: 10.13328/j.cnki.jos.006599] http://www.jos.org.cn

运用时间分类树的确定单时钟时间自动机学习

∗

米钧日

张苗苗

安

杰

杜博闻

(同济大学软件学院,上海, 201804)

(Max Planck Institute for Software Systems, Germany, 67663)

(University of Warwick, UK, CV4 7AL)

通讯作者: 张苗苗, E-mail: miaomiao@tongji.edu.cn

摘要:时间自动机的模型学习算法旨在通过提供输入和观察输出构建软硬件系统的形式化模型.确定性单时钟时

间自动机的学习是其中的一个重要研究方向,但是该算法具有一定的局限性,在状态较多时学习速度较慢,很难应用

到复杂的系统中.由此,我们提出了一种改进的学习算法,使用逻辑时间分类树代替逻辑时间观察表作为学习算法的

内部数据结构,有效地减少了成员查询次数,降低了算法的空间复杂度,并能够高效率地构建假设自动机.最后我们

进行了相关实验,实验结果表明,本文提出的改进算法减少了 60%左右的成员查询和 5%左右的等价查询.同时在该

实验中,改进算法的学习速度最高可提高 45 倍以上.

关键词: 模型学习;主动学习;确定性单时钟时间自动机;时间语言;逻辑时间分类树;

中图法分类号: TP311

中文引用格式: 米钧日, 张苗苗, 安杰, 杜博闻. 基于时间分类树的单时钟时间自动机的学习. 软件学报.

http://www.jos.org.cn/1000-9825/6599.htm

英文引用格式: Mi JR, Zhang MM, An J, Du BW. Learning Deterministic One-clock Timed Automata Based via Timed

Classification Tree. Ruan Jian Xue Bao/Journal of Software, 2022(in Chinese). http://www.jos.org.cn/1000-9825/6599.htm

Learning Deterministic One-clock Timed Automata Based via Timed Classification Tree

MI Jun-Ri

, ZHANG Miao-Miao

, AN Jie

, DU Bo-Wen

(School of Software, Tongji University, Shanghai 201804, China)

(Max Planck Institute for Software Systems, Germany, 67663)

(University of Warwick, UK, CV4 7AL)

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 timed automata is one of the important research directions, but current algorithm has some

limitations and is difficult to be applied to complex systems. Therefore, we propose an improved learning algorithm, 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, we have carried out relevant experiments, and the experimental results show that the improved algorithm

proposed in this paper 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.

Key words: model learning; deterministic one clock timed automata; timed language; logic timed classification tree

1987 年,Angluin 提出的一种名为



的模型学习算法

[1]

.给定一个正则语言 L,该算法可以在多项式时间内学

习得到一个最小的识别目标语言 L 的确定性有限自动机(Deterministic Finite Automata,简称 DFA).该算法构造

∗ 基金项目: 国家自然科学基金(61972284, 62032019)

收稿时间: 2021-09-05; 修改时间: 2021-10-14; 采用时间: 2022-01-10; jos 在线出版时间: 2022-01-28

Journal of Software

软件学报

了基于两个角色:老师(Teacher)和学生(Leaner)的主动学习框架,即老师掌握目标语言,学生可以通过成员查询

和等价查询两种问题来向老师学习该语言.其中,成员查询指的是判断给定的一个字(word)是否属于目标自动

机的语言(Language),老师可以回答“是”或“否”;等价查询指的是判断构造的猜想自动机的语言是否与目标

语言相等,老师可以回答“是”或“否”,并且在给出否定回答时提供一个字(word)作为反例以表示两个语言的

差异.算法的过程如下:首先学生通过多次成员查询获取一些字的查询结果,并将这些字和查询结果存放在一张

观察表中,当获取到足够信息并通过操作使得观察表满足封闭性(closed)和一致性(consistent)时,学生利用观察

表中的信息构造出一个 DFA 作为当前对目标语言的假设,然后通过等价查询判断该假设是否正确.如果正确,

学习算法结束,即当前假设的语言与目标语言相等.如果不正确,学生根据老师给出的反例进行新的成员查询,

收集更多信息,并进一步构造新的假设自动机.该过程直至当前假设自动机的等价查询结果为真,即构造的假设

自动机的语言与目标自动机的语言相等.

在此基础上,国内外学者将模型学习算法扩展到了更多的形式模型,例如 Mealy 机

[2-4]

,非确定有限自动机

[5]

符号自动机

[6-8]

,寄存器自动机

[9-11]

,Büchi 自动机

[12,13]

，马尔科夫决策过程

[14]

等.这些算法在形式化模型的建模

和验证

[15]

有着很多应用.最近两年,安杰等人在观察表中引入了时间信息,提出了实时自动机(Real Timed

Automata,简称 RTA)以及确定性单时钟时间自动机(Deterministic One-Clock Timed Automata,简称 DOTA)的模

型学习算法

[16,17]

.沈炜等人将 PAC(Probably Approximately Correct Leaning)理论应用到 DOTA 的等价查询算法

中,为等价查询提供错误率和置信度等统计保证,从而为 DOTA 的模型学习在实际场景中的应用提供了理论支

持

[18]

然而,目前文献

[17]

基于观察表的 DOTA 的模型学习算法具有一定的局限性,状态较多时学习速度较慢,难以

应用到较为复杂的实际系统中.通过对该算法进行分析,我们发现该算法主要存在以下两个问题:

(1) 在理论复杂度方面,存在大量冗余的成员查询.具体如下,当等价查询不满足时,老师给出一个反例,学

生处理这个反例的方法是将反例的所有前缀加入到观察表中.由于并不是所有的前缀都携带了修改

假设的有效信息,这种处理方式必然会在观察表中增加冗余的前缀,且这些前缀在后续的学习过程中

会持续产生冗余的成员查询等负面影响,从而降低了学习算法的效率.

(2) 在实际运行方面,构造满足封闭性和一致性的观察表的操作耗时很多.具体如下,在学习算法执行过

程中,学生不断地对假设 DOTA 进行迭代更新.每次迭代,学生都需要重新检查观察表并通过相应操作

使得观察表满足封闭性和一致性,然后根据观察表构建出一个新的假设 DOTA.当观察表的规模较大

时,相关操作耗时明显,而在模型学习理论中这些操作的时间复杂度均被忽视.再者,对于迭代前后的

两个假设 DOTA 来说,其迁移信息大体相同,仅有少量改动.但由于观察表只能隐式地保存这些迁移信

息,所以即使是两个假设中相同的状态迁移,也需要学生重新进行计算才能得到,这是该学习算法效

率低的另一个原因

对于一些不带时间信息的形式模型的模型学习算法,国内外学者提出了一些优化算法,其中使用分类树代

替观察表作为算法的内部数据结构是一种较为通用的方案.该方案在 DFA 和符号自动机的模型学习算法中都

取得了较好的效果

[8][19]

.基于相关工作的启发,针对文献

[17]

中灰盒情形下 DOTA 的学习,我们提出了改进的学习

算法并给予实现.我们的主要工作总结如下:

(1) 受到文献

[20]

的启发,我们在分类树中扩展了时钟信息,提出了逻辑时间分类树的概念.基于逻辑时间

分类树,我们提出了改进的 DOTA 学习算法,该算法可以对反例进行分析找到假设和目标自动机第一

次分歧的错误下标,并且对该错误下标进行处理.从而降低了成员查询的数量,提高学习的速度,这从

根本上解决了上述的第一个问题.

(2) 运用逻辑时间分类树的相关操作取代了耗时的观察表检查和相应操作,并且在逻辑时间分类树中增

加了叶节点迁移用以存放假设自动机的迁移信息,使学生不需要复杂的计算即可获得假设 DOTA 的

状态迁移信息,从而提高了构造假设 DOTA 的效率,这解决了上述的第二个问题.

(3) 我们实现了改进的 DOTA 学习算法,并与现有的 DOTA 学习算法在灰盒情形下进行了比较和评估,实

of 19

免费下载

软件学报计算机技术

关注

评论