欢迎您！东篱公司
退出
-
申报数据库
-
立项数据库
-
成果数据库
-
项目获奖数据库
中文摘要：
Clarke和McMillan提出了利用mu演算和OBDDs符号模型检测时态逻辑的方法,这些方法是非常有效的，能用于验证许多具有极大状态空间的实际系统（状态个数可以超过10^20）．但是，这些方法不能检测知识逻辑．而时态认知逻辑能更精确地描述分布式领域中系统和协议的规范．文章首先讨论了Kripke结构和mu演算的扩展，然后提出了利用扩展mu演算和OBDDs符号模型检测时态认知逻辑的方法。
英文摘要：
Clarke and McMillan presented symbolic approaches to model check temporal logics via mu-calculus and OBDDs. These approaches are very efficient and can be applied to verify many practical systems with extremely large state spaces in excess of 1020 states. However, these approaches cannot model check knowledge logics. But temporal logics of knowledge can describe more accurately the desirable specification of systems and protocols in distributed systems. In this paper, the symbolic approaches for model checking the temporal logic of knowledge via extended mu-calculus and OBDDs are discussed mainly. First the Kripke structure and mu-calculus are extended. Then the symbolic approaches for model checking temporal logics of knowledge via extended mu-calculus and OBDDs are presented.
同期刊论文项目
同项目期刊论文
An ID-Based Partially blind signature scheme with adaptive delegation for networked embedded
systems
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
位置：