Three-Valued Abstraction for Model Checking the Probabilistic Temporal Logic of Knowledge

ZHOU Cong-hua; SUN Bo; LIU Zhi-feng; GE Yun

doi:10.3969/j.issn.0372-2112.2012.10.025

您当前的位置：

首页 >

文章列表页 >

Three-Valued Abstraction for Model Checking the Probabilistic Temporal Logic of Knowledge

更新时间：2025-07-16

- Three-Valued Abstraction for Model Checking the Probabilistic Temporal Logic of Knowledge
- Acta Electronica Sinica Vol. 40, Issue 10, Pages: 2052-2061(2012)
- 作者机构：
  
  1. 江苏大学计算机科学与通信工程学院,镇江,212013
  2. 南京大学电子科学与工程学院,南京,210093
- 作者简介：
- 基金信息：
- DOI：10.3969/j.issn.0372-2112.2012.10.025
  CLC： TP301
- Published：2012
- 稿件说明：
移动端阅览
ZHOU Cong-hua, SUN Bo, LIU Zhi-feng, et al. Three-Valued Abstraction for Model Checking the Probabilistic Temporal Logic of Knowledge[J]. Acta Electronica Sinica, 2012, 40(10): 2052-2061.
DOI：

ZHOU Cong-hua, SUN Bo, LIU Zhi-feng, et al. Three-Valued Abstraction for Model Checking the Probabilistic Temporal Logic of Knowledge[J]. Acta Electronica Sinica, 2012, 40(10): 2052-2061. DOI： 10.3969/j.issn.0372-2112.2012.10.025.

摘要

为缓解概率时态认知逻辑模型检测中的状态空间爆炸问题

提出了概率时态认知逻辑的三值抽象技术.具体研究内容包括:定义抽象模型及模型上概率时态认知逻辑的三值语义

依据状态空间等价划分建立初始抽象模型

并证明抽象技术对概率时态认知逻辑的满足性保持关系;提出概率时态认知逻辑模型检测算法;依据初始模型检测的结果

给出利用最小证据和最小反例引导的抽象系统的求精过程.最后通过Dining Cryptographer协议说明了抽象技术的应用

及其在约简系统状态空间方面的效果.

Abstract

In order to overcome the state explosion problem in model checking the probabilistic temporal logic of knowledge

a three-valued abstraction is proposed.Our work includes three parts:first the three-value semantics of the probabilistic temporal logic of knowledge is defined on the abstract model

and the initial abstract model is build according to the equivalence partition of state space

and the preservation of satisfaction under the abstraction is proved;second the model checking algorithm of the probabilistic temporal logic of knowledge is proposed;third how to refine the abstraction by the minimal witnesses and counterexamples generated in model checking is shown.Finally

the abstraction is applied in model checking the Dining Cryptographer protocols.

关键词

Keywords

references

Views

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Research on Interaction Modeling and Mismatch Checking of Time-Aware Web Services

Exact Acceleration of Real-Time Model Checking Based on Parking Cycle

Specification and Verification of Web Service Composition Based on XYZ/ADL

Precisely Detecting Buffer Overflow Vulnerabilities

Model Checking: Theories, Techniques and Applications

Related Author

Sheng

WANG Sheng

RONG Mei

ZHANG Guang-quan

WANG Cong-yin

ZHUANG Lei

YIN Chuan-long

SHI Hui-juan

Related Institution

Shenzhen Tourism CollegeJinan UniversityShenzhenGuangdong 518053China

State Key Laboratory of Computer ScienceChinese Academy of ScienceBeijing 100190China

School of Computer Science and TechnologySoochow UniversitySuzhouJiangsu 215006China

Shenzhen Tourism College,Jinan University

State Key Laboratory of Computer Science,Chinese Academy of Science

⁰