联手形式化方法专业委员会：“时间自动机”术语发布 | CCF术语快线
开篇导语：
本期新增术语新词：时间自动机(timed automata)。时间自动机是指在有限自动机上增加有限个同步运行的时钟所构成的模型，属于形式化方法中的形式化模型。
时间自动机(Timed Automata)
作者：李国强（上海交通大学）
InfoBox：
中文名：时间自动机
外文名：Timed Automata
简写：TA
学科：形式化方法
基本简介：
时间自动机[1]是一个对实时系统进行建模和验证的模型。它可以理解成一个带有限个时钟集合的有限自动机。每个时钟都是一个取值范围为0或正数的变量，且同步运行。时间自动机状态之间的转换要满足边上时钟约束才可能发生，且这种转换不消耗时间，在状态转移中，某些时钟可以被重置为0。只要满足当前状态中的时钟约束，时间自动机的时间可以在这个状态中流逝。换言之，时间自动机是用有限个实数值变量扩展的有限自动机。
时间自动机有一些扩展模型，如时钟除了可以流逝，还可以在某些条件下停止的停表自动机(stopwatch timed automata)[2]；时钟值可以进行加一或减一操作的可调整时间自动机(updatable timed automata)[3]；时钟与状态转换中的输入字符相绑定的事件时间自动机(event-clock timed automata)[4]；以及对时钟数量进行限制的单时钟时间自动机(one-clock timed automata)[5]，双时钟时间自动机(two-clock timed automata)[6]等。这些扩展的模型都从表达能力上改变了时间自动机的性质。
时间自动机能够获得足够的关注，一个主要原因是它有一个成功的形式化工具UPPAAL[7]，由瑞典乌普萨拉大学和丹麦的奥尔堡大学联合实现。该工具可以做形式化建模、验证、仿真以及代码自动生成，在学术界和工业界均获得很大的成功。
发展历程：
时间自动机由阿勒和迪尔在1994年提出[1]。在最初的时间自动机定义中，系统能在当前状态停留任意长时间。在两个状态切换时，有三个参数：输入字符、时间约束以及重置时钟集合。其中，时间约束可以是时钟值与整数间的比较（被称为无对角线约束），也可以是时钟值之间的比较（被称为对角线约束）。所以，当从一个状态切换到另外一个状态，必须满足当前时钟所表示的时间满足时间约束，切换之后，在重置时钟集合里的时钟被置为0两个条件。在之后的应用研究中，研究者发现允许在当前状态停留任意长时间不利于为实际系统建模。因而在每个状态中增加了一个时间约束，称之为不变量[8]。只有当前时钟所表示的时间满足不变量，系统才能在状态中停留。这样定义的时间自动机逐步成为通用的时间自动机定义。研究表明，时间自动机中对角线约束以及不变量都是语法糖，具有这些特征的时间自动机可以转化为等价的没有这些特征的时间自动机[8]。当然，这一结论仅在时间自动机成立，在其各种扩展模型中不一定会成立。2004年，研究者发现在状态切换中将时钟置0的时间自动机和将时钟置成某个整数区间中任意一个值的时间自动机等价且相互可以转换 [8]，这样建模更适合时间自动机及其扩展模型的理论研究，而通用的时间自动机定义则适合工程化建模。时间自动机是用有限个实数值变量扩展的有限自动机，其可判定结论是通过将实数值区域化(region)[1]，区域化可以理解成实数值上的有限个等价类。虽然可以将实数离散化，但状态有指数级膨胀，不利于实现；后来研究者提出了时区化(zone)[8]，时区化是区域化的一种紧致表示方式，虽然在理论上没有降低复杂度，但在可以有较高效率的实现。2004年，研究者使用数字词(digiword)来表示区域[9]，因而将实数域的时间表示成为良结构推导系统(well-structured transition system, WSTS)[10]，这以证明技巧大大推进了时间系统的判定性证明的简洁性和通用性，使得一系列复杂时间系统，如稠密时间下推系统(dense-timed pushdown systems)[11]、嵌套时间自动机(nested timed automata)[12] 等模型借助了良结构推导系统的证明方法，得到了模型各性质可判定性的证明。
应用领域：
如同其他自动机模型一样，时间自动机被广泛地应用于时序系统的形式化建模、形式化验证、仿真、代码自动生成及模型自动修复[13]，借助UPPAAL等高效工具，领域包括web服务[14]，调度任务系统[15]、嵌入式系统[16]等。
参考文献
1. R. Alur, D.L. Dill. A Theory of Timed Automata. Theoretical Computer Science, Vol. 126, 183–235, 1994.
2. F. Cassez, K. Larsen. The Impressive Power of Stopwatches. In Proc. of CONCUR'00, 138-152,2000.
返回首页
