Method for Combining Paraconsistency and Probability in Temporal Reasoning

DOI Web Site Web Site 3 Citations 33 References
  • 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

Search this article

Description

<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>

Journal

Citations (3)*help

See more

References(33)*help

See more

Related Projects

See more

Keywords

Details 詳細情報について

Report a problem

Back to top