Theory of formal specification and verification of concurrency systems and real-time systems based on linear logic

给出了并发系统，特别是实时并发系统的形式化说明和形式化验证的逻辑方法，该方法在密集时间设置中包含量化的时间约束。在项目的前半部分，我们给出了一个在密集实时设置下验证基本安全性和其他相关属性（成员属性、约会属性、活跃属性等）的具体算法。我们还给出了从规范（在自然描述语言的框架中编写）自动转换为线性逻辑规范的理论。然后在项目的后半段，我们将我们的理论扩展到动态实时系统，其中代理/参与者的数量和时间约束的形式是动态变化的。并将线性逻辑方法与传统的模型检验和时间自动机方法进行了比较。

We gave a logical method for formal specification and formal verification of concurrent systems, in particular real-time concurrent systems, which contains quantified time constraints in the dense-time setting.In the first half of the project we gave a concrete algorithm for verification of the basic safety and other related properties (the membership property, the appointment property, the liveness property, etc.) in the dense real-time setting. We also gave a theory of automated transformation from a specification (written in the framework of natural description language) into a linear logical specification.Then in the second half of the project we extended our theories to dynamic real-time systems where the number of agents/participants and the form of time-constraints are dynamically changed. We also compared our linear logical method with the traditional model checking and the timed automata method.