Inconsistency-Tolerant Hierarchical Probabilistic CTL Model Checking: Logical Foundations and Illustrative Examples

被引：2

作者：

Kamide, Norihiro ^{[1
]}

机构：

[1] Teikyo Univ, Dept Informat & Elect Engn, Fac Sci & Engn, Toyosatodai 1-1, Utsunomiya, Tochigi 3208551, Japan

来源：

INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING | 2022年 / 32卷 / 01期

关键词：

Probabilistic temporal logic; inconsistency-tolerant temporal logic; hierarchical temporal logic; probabilistic model checking; inconsistency-tolerant model checking; hierarchical model checking; clinical reasoning verification; COMPUTATION-TREE LOGIC; TEMPORAL LOGIC;

D O I：

10.1142/S0218194022500061

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

In this study, an inconsistency-tolerant hierarchical probabilistic computation tree logic (IHpCTL) is developed to establish a new extended model-checking paradigm referred to as IHpCTL model checking, which is intended to verify randomized, open, large, and complex concurrent systems. The proposed IHpCTL is constructed based on several previously established extensions of the standard probabilistic temporal logic known as probabilistic computation tree logic (pCTL), which is widely used for probabilistic model checking. IHpCTL is shown to be embeddable into pCTL and is relatively decidable with respect to pCTL. This means that the decidability of pCTL with certain probability measures implies the decidability of IHpCTL. The results indicate that we can effectively reuse the previously proposed pCTL model-checking algorithms for IHpCTL model checking. Moreover, in this study, some new illustrative examples for clinical reasoning verification are addressed based on IHpCTL model checking.

引用

页码：131 / 162

页数：32