度量区间时序逻辑MITL的模型检测与控制器合成

The temporal logic MITL (metric interval temporal logic) is one of the most popular timed temporal logic. It is a real-time extension of linear-time temporal logic LTL, and it can be used conveniently to specify various real-time properties such as bounded safety and bounded liveness for real-time systems. Model checking is an algorithmic technique for verifying whether a system has some desired properties, and controller synthesis is an algorithmic technique for constructing a controller that satisfies some given specifications. Both techniques have been widely studied and used in the field of formal verification. Unfortunately, there is no model checking tool and controller synthesis tool available for MITL. This project aims to build a model checking tool and a controller synthesis tool for MITL. The main research includes: 1. Translating MITL into timed Büchi automata; 2. Symbolic model checking of MITL properties over timed automata; 3. Translating MITL into deterministic under-approximation/over-approximation timed Büchi automata; 4. Zone based LU-abstraction for timed game automata; 5. Controller synthesis tool for timed game automata with LTL winning conditions.

度量区间时序逻辑MITL是一种常用的实时逻辑,它是线性时序逻辑LTL的实时扩展，它使用带区间的时序算子表示时间约束,可以很方便地表示有界安全性、有界活性等各种实时性质。 模型检测是一种用于验证系统是否满足给定性质的算法技术,控制器合成是一种从规范出发自动构造满足规范的控制器的算法技术；两种技术都在形式验证领域得到广泛研究和应用。可惜的是，至今还没有关于MITL的模型检测工具和控制器合成工具。 项目的主要目标是实现MITL的模型检测工具和控制器合成工具。主要研究内容有：1．MITL到时间Büchi自动机的有效转换算法和工具；2．MITL关于时间自动机的符号化模型检测工具； 3.MITL到确定性时间Büchi自动机的(上、下)近似转换；4．时间博弈自动机的LU-抽象；5.时间博弈自动机关于LTL公式的控制器合成工具。

度量区间时序逻辑MITL和它的子逻辑MTL{0,∞}是线性时序逻辑LTL的实时扩展，被广泛应用于实时系统的形式规范，它们可以很方便地用来表示包括安全性、有界安全性、活性、有界活性等在内的各种实时性质。模型检测是一种用于验证系统是否满足给定性质的算法技术, 控制器合成是一种从规范出发用来构造满足给定规范的控制器的算法技术；两种技术都在形式验证领域得到广泛研究和应用。可惜的是，在本项目实施之前一直没有可用的关于MITL和MTL{0,∞}的模型检测工具和控制器合成工具。. 本项目主要致力于实现关于MITL和MTL{0,∞}的模型检测工具和控制器合成工具：. 1. 提出并实现了从所有MTL{0,∞}公式到非确定性时间Büchi自动机的一个有效转换方法，为实现MTL{0,∞}的模型检测奠定了基础；. 2. 实现了时间自动机关于MTL{0,∞}的一个模型检测工具CTAV2.0，据我们所知，这是国际上第一个关于度量区间时序逻辑的模型检测工具。此外，在CTAV2.0的基础上，我们还实现了关于MTL{0,∞}的多核模型检测工具CTAV3.0，提高了工具的性能；. 3. 为了实现MTL{0,∞}的控制器合成过程，提出了一个从度量区间时序逻辑MTL{0,∞}到上近似确定性时间Büchi自动机和下近似确定性时间Büchi自动机的有效转换过程，并实现在工具CASAAL中；. 4. 与丹麦奥尔堡大学UPPAAL研究小组合作，提出并实现了时间博弈自动机关于度量区间时序逻辑MTL{0,∞}的一个实用的、但不完备的控制器合成过程和集成工具链。