Abstraction in Model Checking Probabilistic Real-Time Temporal Logic of Knowledge

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

doi:10.3969/j.issn.0372-2112.2013.07.016

您当前的位置：

首页 >

文章列表页 >

Abstraction in Model Checking Probabilistic Real-Time Temporal Logic of Knowledge

更新时间：2025-07-16

- Abstraction in Model Checking Probabilistic Real-Time Temporal Logic of Knowledge
- Acta Electronica Sinica Vol. 41, Issue 7, Pages: 1343-1351(2013)
- 作者机构：
  
  江苏大学计算机科学与通信工程学院,江苏,镇江,212013
- 作者简介：
- 基金信息：
- DOI：10.3969/j.issn.0372-2112.2013.07.016
  CLC： TP301
- Published：2013
- 稿件说明：
移动端阅览
LIU Zhi-feng, SUN Bo, ZHOU Cong-hua. Abstraction in Model Checking Probabilistic Real-Time Temporal Logic of Knowledge[J]. Acta Electronica Sinica, 2013, 41(7): 1343-1351.
DOI：

LIU Zhi-feng, SUN Bo, ZHOU Cong-hua. Abstraction in Model Checking Probabilistic Real-Time Temporal Logic of Knowledge[J]. Acta Electronica Sinica, 2013, 41(7): 1343-1351. DOI： 10.3969/j.issn.0372-2112.2013.07.016.

摘要

概率实时时态认知逻辑PTACTLK模型检测面临着与传统模型检测同样的挑战

即状态空间爆炸问题.抽象是缓解状态空间爆炸问题的最为有效的方法之一.为了缓解概率实时时态认知逻辑模型检测中的状态空间爆炸问题

我们给出了一种抽象技术:对于PTACTLK中的实时部分PTACTL

采用抽象离散时钟赋值

把概率实时解释系统的无限状态空间转化成有限形式;对于PTACTLK中的认知算子K

给出了抽象状态关于智体认知等价的定义.定义了概率实时解释系统的抽象模型

给出了抽象模型上概率实时时态认知逻辑的语义

并证明了由抽象技术演绎得到的抽象模型是原始模型的上近似.最后通过一个通信协议来说明抽象技术的有效性.

Abstract

The same challengs facing model checkings in probabilistic real-time temporal logic of knowledge PTACTLK is the same as traditional model one.That is the state space explosion problem.Abstraction is one of the most effective methods to alleviate the state space explosion problem.In order to alleviate the problem of the state space explosion in model checking probabilistic real-time temporal logic of knowledge

an abstraction technique is presented.For the real time part of PTACTLK

that is PTACTL

we adopt the abstract discrete clock valuations

and the infinite state space of a probabilistic real time was interpreted into a finite form.For the epistemic operator K in PTACTLK

the definition of epistemic equivalent to an agent between abstract states is given.We define the abstract model of the interpreted system in a probabilistic real time and present the semantics of PTACTLK on the abstract model.We prove that the abstract model obtained by using the abstraction techniques is the upper approximation of the original model.At last

a simple communication protocol is adopted to illustrate the effectiveness of our abstraction techniques.

关键词

Keywords

references

Views

1279

下载量

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

Transfer of Reinforcement Learning:The State of the Art

Precisely Detecting Buffer Overflow Vulnerabilities

Related Author

Sheng

WANG Sheng

RONG Mei

ZHANG Guang-quan

WANG Cong-yin

ZHUANG Lei

YIN Chuan-long

ZHU Xue-yang

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

⁰