欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
时态认知逻辑已被广泛应用于分布式系统和协议的规范描述，模型检测时态认知规范已成为一个新的研究领域，因此着重研讨时态认知规范的“On the Fly”模型检测算法．在“On the Fly”模型检测时态逻辑描述规范的基础上，根据自动机理论、深度优先方法和知识的语义，提出了“On the Fly”模型检测时态认知规范的算法，该算法在模型检测带有知识算子的时态规范时，在找到一个反例之前，往往只需构造系统的部分甚至小部分状态空间，从而避免了时态认知规范的模型检测中内存不足和状态爆炸等问题，实现了“On the Fly”模型检测时态认知规范，并且算法的复杂性是多项式时间的．最后，通过该方法在验证TMN密码协议中的应用来作为一个例子说明该方法的有效性．
英文摘要：
Temporal logics of knowledge have been widely used in the distributed systems community and in the expression for the specifications of protocols. The model checking for temporal logics of knowledge becomes a new and important research domain. So approaches to the ＂on the fly＂ model checking the temporal logics of knowledge are discussed. Based on the ＂on the fly＂ model checking approaches for temporal logics, and according to automata theory and the semantics of knowledge, the ＂on the fly＂ model checking approaches to the temporal logics of knowledge are presented. These approaches, making the model checking for the specifications with knowledge operators, need only to construct a small portion of state space of system before a counterexample is found, and so avoid memory-shortage and state-explosion and realize ＂on the fly＂ model checking for the tempora.l logic of knowledge. And the time complexity of the algorithm is polynomial. Finally, the application to the verification of the TMN cryptographic protocol is illustrated to show the effectiveness of the approach.
同期刊论文项目
同项目期刊论文
Estimating Confidence Intervals for Structural Differences between Contrast Groups with Missing Data
POP Algorithm: Kernel-Based Imputation to Treat Missing Values in Knowledge Discovery from Databases
Genetic-algorithm-based Strategy for Identifying Association Rules without Specifying Actual Minimum
期刊信息
位置：