构建度量区间时序逻辑的时间自动机

实时系统的安全性至关重要，使用模型检测工具对其进行形式化分析是提高 其安全性的重要手段。我们已有的实时系统模型检测工具CTAV 目前可以验证 LTL 描述的性质。本文工作的最终目的是让CTAV 能够验证实时时序逻辑，即， 使得CTAV 同样可以直接验证由实时时序逻辑描述的连续时间域上的实时性质。 度量区间时序逻辑MITL 是常用的一种关于实时系统的性质规范语言。已有 不少文献讨论过MITL 到时间Büchi 自动机的转换，但由于过程较复杂，大多数 仅限于理论研究，并没有与时间Büchi 自动机的空性判定过程结合成为一个可用 的关于MITL 的模型检测工具。 为了开发可用的关于MITL 性质的模型检测工具，本文采用与CTAV 中待验 证系统模型一致的pointwise 语义模型，选取了MITL 的一个可以较高效的进行模型检测的子类——MITL≤/<。在表达能力方面，这个子集能够描述实时系统模 型检测实际过程中常见的实时性质。 本文给出了将MITL≤/<公式转化为等价的基于迁移的扩展时间Büchi 自动机 的算法过程，并讨论了转化中逻辑公式重写规则的正确性和完备性问题。基于迁 移的扩展时间Büchi 自动机是时间Büchi 自动机的一种变体。二者最主要的区别在于它们采用了不同类型的Büchi 接受条件。文中给出的构造算法是将原先应用于非实时领域的Tableau 方法扩展调整，并应用于实时连续领域。Tableau 方法的关键之一是公式重写规则。而为了保证结果自动机仅存在有限多个状态，在重写规则中定义不动子公式是至关重要的。本文给出的在pointwise 语义模型下的公式重写规则，借用了此前在continuous 语义模型下已有的将时钟变量作为时序算子的约束直接引入公式中来保证重写规则中存在不动子公式的思想，并对其进行了修改，使原先性质自动机的时钟递减变为时钟递增，与系统自动机中的时钟行走方式一致。这省去了下一步将性质自动机和系统自动机相乘判空时，因为时钟行走方式不一致而引起的麻烦。另外，本文将MITL≤/<中的某些公式扩展为包含时钟约束的新的公式。这样，在定义重写公式时，不仅保证重写规则中存在不动子公式，也保证结果自动的前进性。 本文还根据构造算法实现了转化工具MITLCon。与Marc Geilen 和Dennis Dames 实现的逻辑转化工具相比，MITLCon 显著地减少了结果自动机节点和迁 移的数量，从而降低了结果自动机的大小，有利于进一步的模型检测过程。