Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Inconsistency-tolerant Temporal Logics <s> Generalizations.- Intuitionistic minimal and intuitionistic information processing.- Functional completeness for substructural subsystems of IPL.- Formulas-as-types for substructural subsystems of IPL.- Constructive minimal and constructive information processing.- Functional completeness for substructural subsystems of N.- The constructive typed ?-calculus ?c and formulas-as-types for N?.- Monoid models and the informational interpretation of substructural propositional logics. <s> BIB001 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Inconsistency-tolerant Temporal Logics <s> The temporal logics pCTL and pCTL* have been proposed as tools for the formal specification and verification of probabilistic systems: as they can express quantitative bounds on the probability of system evolutions, they can be used to specify system properties such as reliability and performance. In this paper, we present model-checking algorithms for extensions of pCTL and pCTL* to systems in which the probabilistic behavior coexists with nondeterminism, and show that these algorithms have polynomial-time complexity in the size of the system. This provides a practical tool for reasoning on the reliability and performance of parallel systems. <s> BIB002 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Inconsistency-tolerant Temporal Logics <s> In this paper the branching time logic pCTL* is defined. pCTL* expresses quantitative bounds on the probabilities of correct behavior; it can be interpreted over discrete Markov processes. A bisimulation relation is defined on finite Markov processes, and shown to be sound and complete with respect to pCTL*. We extend the universe of models to generalized Markov processes in order to support notions of refinement, abstraction, and parametrization. Model checking pCTL* over generalized Markov processes is shown to be elementary by a reduction to RCF. We conclude by describing practical and theoretical avenues for further work. <s> BIB003 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Inconsistency-tolerant Temporal Logics <s> It has been widely recognized that inconsistencies often appear and are inevitable when specifying large and complex concurrent systems. The logic QCL (quasi-classical logic) has therefore been developed for handling such specifications. But, on the one hand, temporal aspects, significant for ensuring the correct behavior of concurrent systems, cannot be specified by QCL, on the other hand, Classical temporal logics like CTL (computation tree logic) fail for system specifications with inconsistent information due to the trivial inference problem. To bridge this gap, in this paper a non-classical temporal logic QCTL (quasi-classical temporal logic) is introduced, including a novel semantics in term of paraKripke structures and a sound and complete proof system. It is paraconsistent, i.e., it can be used to non-trivially reason about inconsistent system specifications. Furthermore, an example is presented, showing the use of QCTL for reasoning about concurrent systems containing inconsistent information. <s> BIB004 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Inconsistency-tolerant Temporal Logics <s> Inconsistency-tolerant reasoning and paraconsistent logic are of growing importance not only in Knowledge Representation, AI and other areas of Computer Science, but also in Philosophical Logic. In this paper, a new logic, paraconsistent linear-time temporal logic (PLTL), is obtained semantically from the linear-time temporal logic LTL by adding a paraconsistent negation. Some theorems for embedding PLTL into LTL are proved, and PLTL is shown to be decidable. A Gentzentype sequent calculus PLTω for PLTL is introduced, and the completeness and cut-elimination theorems for this calculus are proved. In addition, a display calculus δPLTω for PLTL is defined. <s> BIB005 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Inconsistency-tolerant Temporal Logics <s> This paper introduces a new temporal logic, SPCTL.SPCTL is an extension of the well-known computation tree logic (CTL).The complexity of the model-checking problem of SPCTL is settled.An illustrative example for medical diagnosis is presented based on SPCTL. A formal method is proposed for modeling and verifying inconsistency-tolerant temporal reasoning with hierarchical information. For this purpose, temporal logic called sequential paraconsistent computation tree logic (SPCTL) is obtained from computation tree logic by adding a paraconsistent negation connective and some sequence modal operators. SPCTL can appropriately represent both inconsistency-tolerant reasoning by the paraconsistent negation connective and hierarchical information by the sequence modal operators. The validity, satisfiability, and model-checking problems of SPCTL are shown to be EXPTIME-complete, deterministic EXPTIME-complete, and deterministic PTIME-complete, respectively. Illustrative examples for inconsistency-tolerant temporal reasoning with hierarchical information are presented using the proposed SPCTL. <s> BIB006 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Inconsistency-tolerant Temporal Logics <s> 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, which indicates that we can reuse existing pCTL-based model checking algorithms. Some illustrative ::: ::: examples involving the use of PpCTL are also presented. <s> BIB007
In comparison with the standard non-paraconsistent temporal logics CTL * , CTL, and LTL, inconsistencytolerant (paraconsistent) logics can be appropriately used in inconsistency-tolerant situations   BIB001 . Typical examples of non-temporal paraconsistent logics include Belnap and Dunn's useful four-valued logic BIB002   ) and Nelson's paraconsistent four-valued logic (Almukdad and Nelson, 1984;  . Combining these logics with CTL * , CTL, and LTL has led to the introduction of various inconsistency-tolerant temporal logics, and inconsistency-tolerant versions (extensions) of CTL, CTL * , and LTL have been developed by many researchers. The multi-valued computation tree logic (χCTL) was introduced by Easterbrook and Chechik (Easterbrook and Chechik, 2001) as the base logic for multi-valued model checking, the first framework for inconsistency-tolerant model checking. The quasiclassical temporal logic (QCTL) was introduced by Chen and Wu BIB004 to verify inconsistent concurrent systems using inconsistencytolerant model checking. The paraconsistent full computation tree logic (4CTL * ) was proposed by Kamide  to obtain a logical foundation for inconsistency-tolerant model checking. The paraconsistent linear-time temporal logic (PLTL) was introduced by Kamide and Wansing BIB005 to obtain a cut-free and complete Gentzen-type sequent calculus. The alternative paraconsistent computation tree logic (PCTL) was introduced by Kamide and Kaneiwa  and offered an alternative inconsistency-tolerant model checking framework. Kamide BIB006 introduced the sequence-indexed paraconsistent computation tree logic (SPCTL), which can be obtained from the CTL by adding the paraconsistent negation connective, ∼, and a sequence modal operator, [b] . This logic was used to verify clinical reasoning through inconsistency-tolerant hierarchical model checking.  recently developed pCTL and pLTL, which are alternative refined versions of the paraconsistent temporal logics PCTL and PLTL, respectively, to obtain various simple and efficient translation methods for inconsistency-tolerant model checking. These alternative refined logics adopt a simple single-satisfaction relation. The alternative version of PCTL is pCTL, which has the same name as the probabilistic computation tree logic. Whereas PLTL BIB005 , PCTL  , 4CTL *  , and SPCTL BIB006 have two types of dual-satisfaction relations, |= + (verification or justification) and |= − (refutation or falsification), pCTL and pLTL  have a simple single-satisfaction relation, |= * , which is highly compatible with the standard single-satisfaction relations of LTL, CTL, and CTL * . The single-satisfaction relation can provide simple proofs for embedding theorems, and the connective ∼ can be formalized simply and handled uniformly. To deal with open, large, and complex concurrent systems, such as cloud-based systems and web application systems, it is necessary to have extended logics with model checking frameworks that can also simultaneously handle both inconsistency-tolerant and probabilistic reasoning. To this end, in BIB007  , a partial solution was obtained (i.e., an inconsistencytolerant extension of the probabilistic computation tree logic, pCTL, was developed). The paraconsistent probabilistic computation tree logic (PpCTL), which can be obtained from the probabilistic computation tree logic, pCTL, by adding a paraconsistent negation connective ∼, was constructed in BIB007  based on a probability-measure-independent translation of PpCTL into pCTL. The theorem for embedding PpCTL into pCTL was proven using this trans-lation and entails the relative decidability of PpCTL with respect to pCTL (i.e., the decidability of pCTL implies the decidability of PpCTL). This result indicates that we can reuse the existing pCTL-based model-checking algorithms by Aziz et al. BIB003 and Bianco and de Alfaro (Bianco and de Alfaro, 1995) for the PpCTL-based model-checking algorithms.