报告题目：度量时序逻辑MTL{0,∞}的模型检测
报告时间：2016年12月1日下午3点
报告地点：砺志楼2楼210室
报告摘要：
模型检测是一种基于状态空间搜索的形式化验证技术，是提高系统正确性的重要手段。度量时序逻辑MTL{0,∞}是线性时序逻辑LTL的一种实时扩展，它能方便地用来表示实时系统的各种实时性质。我们将介绍实时系统的模型检测的基本概况、度量时序逻辑MTL{0,∞}的基本概念以及实时系统关于MTL{0,∞}性质的模型检测方法与工具。
|
报告人简介：李广元（http://lcs.ios.ac.cn/~ligy/），博士，中国科学院软件研究所计算机科学国家重点实验室研究员，主要从事实时系统的形式化验证技术与验证工具的研究。2009年他首次在国际上实现了时间自动机关于线性时序逻辑LTL的符号化模型检测工具，相关结果被国际同行作为“定理”、“命题”等在国际顶级刊物上加以引用，并被国外一些知名模型检测工具如UPPAAL、LTSmin以及DiVinE等用于时间自动机的活性性质和LTL性质的模型检测。此外，他还与丹麦科学家合
|
作实现了加权度量区间时序逻辑的统计模型检测以及度量区间时序逻辑的有效控制器合成。