对自动机模型学习问题的分析与研究

张圣迪

摘要：形式化方法在模型为导向的软件工程中起到非常重要的作用，其中模型检验已经成为软件验证和纠错的一种重要方法，而模型学习是对于模型检验的一种有效补充技术。本文将对模型学习的概念和研究意义进行介绍，汇总了几种常见的对于寄存器自动机和时间自动机的模型学习的方法，并提出了一種对于时间自动机进行学习模仿的算法思想，最后对于模型学习的主要研究方向进行了阐述。

关键词：模型学习；形式化方法；时间自动机；寄存器自动机

中图分类号：TP311 文献标识码：A

文章编号：1009-3044（2019）10-0171-03

开放科学（资源服务）标识码（OSID）：

1 引言

任何一个软硬件系统在开发之前都有一个事先预定的系统规约，然后根据系统的需求进行设计和开发。最后经过测试才能保证系统能够一定程度上完成需求规约中描述的功能和行为。如果我们想要对一个系统进行分析，可以采取在需求文档阶段进行仿真的方法，也可以对开发后的真实系统进行实际的测试分析。当用形式化的方法分析一个软硬件系统时，学者们希望通过某种手段推断系统的抽象模型，然后根据模型检验来对系统的行为进行分析。模型学习的目标是通过用观察得到的系统行为序列和相关的数据来构建软件和硬件系统的状态图模型，可以解决上述的系统模型建立问题。其中涉及的模型学习算法的设计和实现是一个非常具有研究价值的问题。从理论角度分析，这种形式化的方法更具有可信度和完备性。

本文对于近十年来可用性强的一些模型学习算法进行了汇总，其中设计的模型主要分为确定性有限自动机模型，寄存器自动机模型和时间自动机模型。并在之后提出了一个用于学习时间自动机的框架。

2 背景

有很多推断软件组件模型的方法，比如分析具体代码、挖掘系统日志、执行测试等等。也有很多不同种类的模型能支持这些推断方法，比如马尔可夫模型、变量之间的关系模型、类图模型等等。本文的关注点是在一种特定类型的模型之内，即状态图（又称自动机），其对于理解许多软件系统的行为至关重要，例如安全协议、网络协议和嵌入式控制软件。模型推断技术可以基于白盒或黑盒，区别在于是否需要访问代码。黑盒技术的优点是相对容易使用，并可以应用在我们没有代码访问权限或有效的白盒工具的情况下。主动学习的技术是通过主动地对软件进行实验测试来完成它们的任务的技术。此外，还有被动学习的方法，其中的模型是根据软件的许多的运行行为的集合而构建的。主动学习的优点是它能够提供软件组件的全部完备的行为的模型，而不像被动学习那样仅仅提供在实际操作期间发生的某系特定运行行为的模型。

近年来，模型学习技术已经具有了许多成功应用到不同领域的实际案例，比如西门子的电信系统的回归测试分析，法国电信的集成测试分析，在施普林格出版社线上会议服务系统的自动化测试分析，在沃尔沃科技公司的线控制动系统的需求测试分析等等。事实上，模型学习正在成为银行卡、网络协议、遗产软件等领域中能够实际使用的一种高效的漏洞寻找技术。

3 学习算法

3.1 确定性有限自动机

目前学术界对于确定性有限状态自动机的模型学习已经有了一些不错的研究成果。在1987 年，Angluin 发表了相关研讨论文[2]，她根据 Myhill-Nerode定理（对于给定一种语言L，和一对字符串x和y，定义一个能产生区别的延续字符串z，使得两个字符串xz和yz中只有一个属于L。对于这样的字符串的定义一种RL规则：如果对于x和y不存在上述的能区别的延续字符串z，则x RL y可以看出来，RL是字符串上的一种等价关系，可以利用这个关系将字符串的集合划分为若干个等价类。）表明可以使用询问方式来学习到有限自动机，并称之为MAT框架。在该框架中，学习被看作是一种博弈，其中学习者模块必须通过询问教师模块来推断一个未知的状态图的行为。学习者的任务是通过两种类型的询问来学习原始模型：成员查询：学习者询问一个行为序列是否是能被原始自动机接收，教师使用接收或拒绝来回答。等价查询：学习者通过成员查询所得的行为序列集合来构建一个初步的假设模型，然后向教师询问该假设模型与原始模型是否等价，即两个模型对于任一行为序列的接收能力是否等同。如果情况属实，教师回答「是」。否则教师回答「否」，并提供一个反例的行为序列来区分两个模型，并将反例返回给学习者。学习者通过反例继续修改假设模型，继续以上两种提问，直到教师对于等价查询回答「是」。

Angluin提出的L*算法的设计能够通过多项式数量级（多项式数的大小对应于规范的自动机的规模）的复杂度的成员查询和等价查询来学习自动机。L*算法只是一种简单的设计和表达，而后来更多学者对这个算法进行了扩展和优化，但是MAT框架依然是一种有效的模型学习框架。

3.2 寄存器自动机

尽管学习自动机模型的基本算法研究工作已经取得了进展，但是这些算法只能处理规模比较小的有限状态自动机，而且很难应用于实际的系统分析。能初步应用于部分领域的一种自动机模型称为寄存器自动机，这种自动机模型能够存储中间过程中产生的数据值，实现对数据流的部分操作，能够用于描述一部分实际系统的操作行为，比如模拟一个存储队列的行为。在寄存器自动机中，所有数据值都是完全对称的（只做数据值的判等，而不对数据值进行直接修改），在学习算法中可以利用这种对称性。在寄存器自动机的模型学习过程中，比较重要的一点是如何处理一个数据语句中那些需要被存入寄存器的值，因为这些值很可能之后要被用来与参数值进行比较或者用作输出。

Sofia Cassel等人定义了一种可以满足Mihill Nerode定理的特殊的寄存器自动机，并提出了对应这种自动机的模型学习算法SL*[3，4]。模型学习算法通常依赖于这种右同余关系来识别学习自动机的状态和迁移：如果两个语句的剩余语言一致，则这两个语句会到达同一状态。其基本思想是为寄存器自动机定义类似Nerode的同余，用来推断确定自动机的状态，迁移上的寄存器约束和迁移上寄存器的赋值。该算法利用了观察表以及自动机的对称性质，实现的基础数据结构被称为符号决策树。

学习寄存器自动机的另一种实用的方法[5]，是Aarts等人在软件工具Tomte中实现的。一种确定性的右不变的寄存器自动机，也是基于右同余的关系进行学习。Tomte能够支持学习带输入输出的寄存器自动机，整个算法需要多个辅助模块：原始的学习者可以学习构建一个有限的確定性Mealy机，再利用抽象模块可以学习一个限制种类的寄存器自动机，而预兆先知模块让学习种类更加宽泛的寄存器自动机成为可能，确定器模块可以帮助学习迁移上带有新输出的输入输出寄存器自动机。整个想学习过程的设计基于映射器的思想，并且被证明是学习寄存器自动机的一种有效方法。

3.3 时间自动机

时间自动机是一个带有有限时钟集合的有穷状态机，提供了一种简单而有效的方法来描述带有时间因素的系统状态转换图，属于混合自动机的一个重要分支。它主要用于对计算机软件和硬件系统的时间行为进行建模和分析，比如一般的实时系统和网络系统。对于时间自动机的检验目标主要集中于安全性和响应程度的性质检验。

瑞典乌普萨拉大学计算机系的Olga Grinchtein等人在MAT的模型学习框架下提出了对时间自动机的一个子类--确定性事件记录自动机的学习算法LSGDERA（学习带有明确时间监视的确定性事件记录自动机）[6]，通过确定性事件记录自动机与确定性有限自动机的同构性和相关的语言等价性，将学习确定性有限自动机的算法成功改进成为学习一个事件记录自动机的算法。另外他们对于一般的事件记录自动机，利用LSGDERA和相关的合并操作得到一个比较广泛的学习算法。他们的算法非常有开创性，但是算法的复杂度非常高且难以实现。

之后Olga又提出用时间决策树的方法[7]去学习一个时间确定性的事件记录自动机，在事件记录自动机中时钟变量记录的是一个事件前一次发生之后所度过的时间。对每一个事件，事件记录自动机维护一个时钟来保存这个时间变量。其接收的行为序列是时钟语句，这种时钟语句可以从一般的时间语句转换而来。该学习算法中提出了最强后置条件的设定，根据成员询问与等价询问生成和修改时间决策树，并在这个数据结构中结合最强后置条件来对状态节点进行划分，来产生自动机中的时间监视约束，并对统一行为的节点进行合并，最终将整个时间决策树折叠成一个时间确定性的事件记录自动机。它是第一个避免使用时间层域的概念来学习时间自动记录自动机的学习算法。它的优势在于能推广拓展到确定性的时间自动机，有强的表达能力，但是劣势在于高的复杂度。

荷兰代尔夫特理工大学的Sicco Verwer等人根据Miguel Bugalho等人提出了以DFA学习的红蓝边状态合并算法为基础的对于单个时钟的实时自动机进行模型学习的启发式状态合并算法[8]。根据系统对于抽样的时间行为轨迹样本的接受与否，将样本集合分为接受集合和拒绝集合，并根据这些行为轨迹集合生成相应的树形结构APTA（扩增前缀树接收结构）。在APTA的基础上可以对其中的结点进行三类操作：合并，分离，染色。该算法根据样本接受状态的一致性问题制定了相应的评分制度对操作进行评分，其中分高的操作先执行。最终APTA整合成一个待时间约束的确定性自动机，该自动机是单时钟，并且每次迁移都要重置时钟。这个算法有一定的实用性，但是在具体的实践应用中，开始时轨迹的样本是事先一次性确定好的，而最终该算法学习出实时自动机模型是与最初对系统行为的抽样紧密相关的。该算法属于被动学习的范畴，对于一个比较复杂的系统而言，我们不可能穷尽它所有的行为抽样，所以最终学习得到的模型和真正系统中的隐含模型很可能只是一个部分相交的关系。所以在使用这个算法时，为了得到一个更加精准的模型，就必须使最初的抽样覆盖更多的系统特征操作。

4 学习时间自动机的一种新方案

上面的模型学习过程有些设计到转化的问题，将一个难以学习的自动机模型通过一定条件制约转化成另一种较为简单学习的自动机模型，然后再进行学习处理，会让可学习的模型种类更加宽泛。

时间自动机是处理时间语句的自动机模型，而寄存器自动机是处理数据流语句的模型，两种模型虽然有不同的含义，但是在几个判定问题上具有相同的可判定性和复杂度结果。有研究[9]表明两种模型之间在特殊的语句形式和同构关系下可以产生相互的映射，并且能够保持一些特性，比如确定性。这使得我们可以对于其中一个种类的给定模型，计算出另一种类的结果模型，而两个模型的接收情况是针对特殊的语句来进行对应。根据这样的思想，我们可以将这种关系应用到对于时间自动机的学习中来，并取得了一些进展。通过将时间自动机计算生成对应的寄存器自动机，然后针对这个寄存器自动机进行模型学习，然后将学习得到的寄存器自动机模型转化为一个时间自动机的假设模型，最后得到的这个时间模型能够覆盖原本给定时间自动机的所有行为。整个过程（见图1）可以实现对原时间自动机的行为的模仿，最终时间自动机的满足特殊语句形式的运行行为路径可以在一定条件下还原为原本时间自动机的行为路径。但限制在于学习过程中的教师模块的设定较为特殊，而且最终产生的行为集合对原本的行为集合是一种包含关系。

5 研究方向

上面所有的学习过程大都无法保证我们得到的模型和原模型是完全等价的，一般是包含所有的原始自动机的行为或者不能判定。而判定等价所需要的计算力是难以达到。所以一致性的测试是非常重要的一个问题。目前已知的一个可行的方案是通过输入语句上的概率分布应用来让学习得到的模型更加可靠，这是一种概率近似正确的策略，能够在保证学习结果基本可用的前提下大量减少学习过程的复杂度，缺点是可能对目标系统有其他的限制。这种策略要考虑如何在可用性和复杂度之间取得平衡，我们仍需要投入大量的研究来揭示其对真正实际系统项目的学习效果。

另外，在实际应用中对于不同的系统的情况，可以考虑制定不同的学习策略。比如在部分系统内部已知的情况下，可以缩减学习模型的范围，可认为是白盒技术与黑盒的技术的结合使用；对于不同的系统还能使用不用的对应辅助模块，类似之前算法中涉及的映射器模块，可能又因为系统本身特点的不同而呈现不同的特殊定制模块来辅助整个学习过程。定制化可能成为工业化道路上的一个有效策略，但是整个学习过程的前置代价会比较大。

6 总结

本文对于模型学习的概念进行了介绍，并对相关模型的学习算法进行了简述，并提出了一个时间自动机的模型学习方法，最后提出了模型学习流程研究的现阶段需要探索的方向。模型学习仍处于发展的阶段，我们希望越来越多的学者能够投入相关的研究工作，为模型学习的工业化提供更多的支持，这对于形式化方法的发展和软件的有效验证都有非常重要的意义。

参考文献：

[1] Frits Vaandrager. Model learning[J] .Communications of the ACM， 2017，（60） 2： 86-95.

[2] Dana Angluin. Learning regular sets from queries and counterexamples[J]. Information & Computation， 1987， 75（2）：87-106.

[3] Malte Isberner， Falk Howar， and Bernhard Steffen. Learning register automata：from languages to program structures. Machine Learning， 96（1-2）：65–98， 2014.

[4] Falk Howar， Bernhard Steffen， Bengt Jonsson， and Sofia Cassel. Inferring canonical register automata. In Viktor Kuncak and Andrey Rybalchenko， editors， Verification， Model Checking， and Abstract Interpretation， volume 7148 of Lecture Notesin Computer Science， pages 251–266.Springer Berlin Heidelberg，2012.

[5] F Aarts.Tomte： Bridging the Gap between Active Learning and Real-World Systems. PhD thesis， Radboud University Nijmegen， October 2014.

[6] Grinchtein O， Jonsson B， Leucker M. Learning of event-recording automata[J]. Lecture Notes in Computer Science， 2004， 3253：379-395.

[7] Grinchtein O， Jonsson B， Pettersson P. Inference of event-recording automata using timed decision trees[J]. Lecture Notes in Computer Science， 2006， 4137：435-449.

[8] Verwer S，Weerdt M D，Witteveen C.An algorithm for learning real-time automata[J].Proceedings of the BENELEARN，2007，pp.33-42.

[9] Figueira D， Hofman P ， Lasota S. Relating timed and register automata[J].Mathematical Structures in Computer Science， 2016， 26（06）：993-1021.

【通聯编辑：梁书】