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

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

项目编号： No.61472406

项目类型： 面上项目

立项/批准年度： 2015

项目学科： 自动化技术、计算机技术

项目作者： 李广元

作者单位： 中国科学院软件研究所

项目金额： 80万元

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

中文关键词： 模型检测；实时系统；实时逻辑；时间自动机；控制器合成

英文摘要： 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.

英文关键词： model checking;real-time systems;timed temporal logic;timed automata;controller synthesis