The Model Checking Problem of Computing Tree Logic Based on Generalized Possibility Measures

LIANG Chang-jian; LI Yong-ming

doi:10.3969/j.issn.0372-2112.2017.11.010

您当前的位置：

首页 >

文章列表页 >

The Model Checking Problem of Computing Tree Logic Based on Generalized Possibility Measures

更新时间：2025-07-16

- The Model Checking Problem of Computing Tree Logic Based on Generalized Possibility Measures
- Acta Electronica Sinica Vol. 45, Issue 11, Pages: 2641-2648(2017)
- 作者机构：
  
  1. 陕西师范大学数学与信息科学学院,陕西,西安,710119
  2. 商丘师范学院数学与统计学院,河南,商丘,476000
  3. 陕西师范大学数学与信息科学学院,陕西,西安,710119
  4. 商丘师范学院数学与统计学院,河南,商丘,476000
- 作者简介：
- 基金信息：
  
  National Natural Science Foundation of China (No.11271237, No.11671244, No.11401363, No.11501345);Research Fund for the Doctoral Program of Higher Education of China (No.20130202110001)
- DOI：10.3969/j.issn.0372-2112.2017.11.010
  CLC： TP301.2
- Published Online：25 November 2017，
  
  Published：2017
- 稿件说明：
移动端阅览
LIANG Chang-jian, LI Yong-ming. The Model Checking Problem of Computing Tree Logic Based on Generalized Possibility Measures[J]. Acta Electronica Sinica, 2017, 45(11): 2641-2648.
DOI：

LIANG Chang-jian, LI Yong-ming. The Model Checking Problem of Computing Tree Logic Based on Generalized Possibility Measures[J]. Acta Electronica Sinica, 2017, 45(11): 2641-2648. DOI： 10.3969/j.issn.0372-2112.2017.11.010.

摘要

本文首先分别给出了约束可达，总是可达这两个公式在广义可能性计算树逻辑（GPoCTL）中的另外两种等价形式；其次讨论了基于广义可能性测度的计算树逻辑的模型检测问题，将GPoCTL的模型检测问题规约为经典的CTL模型检测问题，利用截集的方法，给出了计算GPoCTL的模型检测问题的算法及其复杂度，并通过实例分析说明了这种算法的可行性；最后，研究了具有公平性假设的GPoCTL模型检测问题的计算复杂度，得到了与上面相似的结论.

Abstract

Firstly

two alternative equivalent forms of GPoCTL state formulas

until

always

are given respectively.Secondly

it shows that the model checking problem of GPoCTL can be reduced to which of CTL

its algorithm is given through the method of cut set

and whose availability is explained with an example analysis

as a result

the time complexity of the algorithm is obtained.Finally

the properties of the GPoCTL model checking problem with fairness assumptions

which are similar to the GPoCTL

are studied by the similar method with GPoCTL.

关键词

Keywords

references

Views

240

下载量

CSCD

Alert me when the article has been cited

提交

Tools

Publicity Resources

Computation Tree Logic Model Checking for Nondeterminisitc Fuzzy Kripke Structure

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

Related Author

LI Yong-ming

PAN Hai-yu

FAN Yan-huan

Sheng

WANG Sheng

RONG Mei

ZHANG Guang-quan

WANG Cong-yin

Related Institution

Department of Mathematics in National Normal College, Qinghai Normal University

College of Computer Science and Technology, Taizhou University

College of Computer Science Shaanxi Normal University Xi'an Shaanxi China

Department of Mathematics in National Normal College Qinghai Normal University Xining Qinghai China

College of Computer Science and Technology Taizhou University Taizhou Jiangsu China

⁰