面向实时传值系统的模态逻辑及模型检测

实时传值系统是一种较普遍的并发系统。本项目从两个方面展开工作；首先建立能刻画实时与传值特征的模态逻辑系统，并研究其语义模型；其次引入近似或概率算法的思想，设计一个高效的模型检测算法，研究其算法杂度及正确性。本项目的研究将丰富面向并系统模态逻辑的相关工作，同时在实时传值系统的正确性验证方面也有重要实际价值。