具体 地：（1）建立了投影时序逻辑 PTL 的模型理论，提出并证明了该逻辑的 182 个 定理和 536 个逻辑规则；建立了 PTL 和 PPTL 的公理系统，并证明了它的合理性 和完备性；解决了 PPTL 和基于区间的命题时序逻辑 PITL 的长期悬而未决的判定 问题；证明了基于区间的时序逻辑的非初等复杂性及 PPTL 的完全正则表达能力； 提出了多核并发程序形式化模型，即柱面计算模型。（2）提出了以投影时序逻 辑 PTL 可执行子集为基础的集建模、仿真和验证为一体的并行程序设计语言 MSVL，给出了 MSVL 的最小模型语义、操作语义和公理语义；解决了时序逻辑面 向实际程序设计中的框架难题；建立了基于 MSVL 的集建模、仿真和验证为一体 的统一验证理论。（3）采取新的途径，提出了多项式抽象模型精化算法，避免 了图灵奖获得者 Clarke 等人提出的精化方法中的指数爆炸问题；提出了线性的 虚假路径检测算法，克服了原虚假反例路径检测中的多项式时间复杂度；提出了 基于构建极大独立集的近似算法，使得构建最小联通支配集的效率得到大幅提 升，有效缩减网络软件系统模型检测中的状态空间，提高了验证效率。（4）研 制了建模、仿真和验证工具集 MSV，支持 C、Verilog、VHDL 程序和 Petri 网的 自动验证。在理论研究的基础上研制的软件工具 MSV 已成功应用于中国航天科技 集团五〇二研究所承担的航天器控制系统软件验证中，为国家重大工程成功实施 做出重要贡献，取得了显著的经济和社会效益。 获奖情况：高等学校科学研究优秀成果奖自然科学一等奖。