Method for Combining Paraconsistency and Probability in Temporal Reasoning

  • Kamide Norihiro
    Faculty of Science and Engineering, Department of Information and Electronic Engineering, Teikyo University
  • Koizumi Daiki
    Faculty of Commerce, Department of Information and Management Science, Otaru University of Commerce

この論文をさがす

説明

<p>Computation tree logic (CTL) is known to be one of the most useful temporal logics for verifying concurrent systems by model checking technologies. However, CTL is not sufficient for handling inconsistency-tolerant and probabilistic accounts of concurrent systems. In this paper, a paraconsistent (or inconsistency-tolerant) probabilistic computation tree logic (PpCTL) is derived from an existing probabilistic computation tree logic (pCTL) by adding a paraconsistent negation connective. A theorem for embedding PpCTL into pCTL is proven, thereby indicating that we can reuse existing pCTL-based model checking algorithms. A relative decidability theorem for PpCTL, wherein the decidability of pCTL implies that of PpCTL, is proven using this embedding theorem. Some illustrative examples involving the use of PpCTL are also presented.</p>

収録刊行物

被引用文献 (3)*注記

もっと見る

参考文献 (33)*注記

もっと見る

関連プロジェクト

もっと見る

詳細情報 詳細情報について

問題の指摘

ページトップへ