[00125172]投影时序逻辑的模型理论及应用

该项目是计算机软件理论领域前沿基础研究,对保障软件系统的正确性和可靠性有重要的应用价值。项目组在以下几方面取得了重要的进展： （1）创建了完整的投影时序逻辑（Projection Temporal Logic,PTL）系统,建立了相关的模型理论。 （2）证明了命题投影时序逻辑（Propositional PTL,PPTL）的可判定性,解决了命题区间时序逻辑（PITL）在无穷模型下25年悬而未决的判定问题;证明了PPTL和PITL的表达能力是完全正则的;证明了PPTL和PITL的复杂性是非基本的。 （3）建立了基于投影时序逻辑的建模理论和方法,定义了建模语言的的最小模型语义和操作语义。 （4）设计并实现了第一个基于区间的时序逻辑的模型检测器：基于SPIN的PPTL模型检测器和基于PTL的统一模型检测器。 （5）提出了网络软件最小节点联通支配集,以及基于Steiner树和贪婪算法的最小网络节点联通支配集构造方法,提高了网络系统模型检测的效率。 研究成果得到区间时序逻辑创始人Ben Moszkowski,以及来自英国Kent大学、加拿大滑铁卢大学、意大利信息技术中心、新加坡国立大学、英国York大学、德国微软创新中心、英国Leicster大学、英国Demontfort大学、丹麦科技大学、日本京都大学、日本国立情报研究所、日本法政大学、美国乔治华盛顿大学等同行专家以及中科院已故唐稚松院士的引用和好评。在理论研究基础上开发的可信软件理论、技术和工具已经成功应用于中国航天科工集团第二研究院706研究所承担的海军某指挥系统以及陕西多家软件公司承担的民用软件系统的开发中,取得了显著地经济效益。