Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> The expression [d] <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> BIB001 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> The expression [d] <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> The expression [d] <s> We investigate the notion of classical negation from a non-classical perspective. In particular, one aim is to determine what classical negation amounts to in a paracomplete and paraconsistent four-valued setting. We first give a general semantic characterization of classical negation and then consider an axiomatic expansion BD+ of four-valued Belnap---Dunn logic by classical negation. We show the expansion complete and maximal. Finally, we compare BD+ to some related systems found in the literature, specifically a four-valued modal logic of Beziau and the logic of classical implication and a paraconsistent de Morgan negation of Zaitsev. <s> BIB003 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> The expression [d] <s> Abstract In this study, logics and translations for hierarchical model checking are developed based on linear-time temporal logic (LTL) and computation-tree logic (CTL). Hierarchical model checking is a model checking paradigm that can appropriately verify systems with hierarchical information and structures. A sequential linear-time temporal logic (sLTL) and a sequential computation-tree logic (sCTL), which can suitably represent hierarchical information and structures, are developed by extending LTL and CTL, respectively. Translations from sLTL and sCTL into LTL and CTL, respectively, are defined, and theorems for embedding sLTL and sCTL into LTL and CTL, respectively, are proved using these translations. These embedding theorems allow us to reuse the standard LTL- and CTL-based model checking algorithms to verify hierarchical systems that are modeled and specified by sLTL and sCTL. <s> BIB004 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> The expression [d] <s> Purpose ::: ::: ::: ::: ::: The purpose of this paper is to develop new simple logics and translations for hierarchical model checking. Hierarchical model checking is a model-checking paradigm that can appropriately verify systems with hierarchical information and structures. ::: ::: ::: ::: ::: Design/methodology/approach ::: ::: ::: ::: ::: In this study, logics and translations for hierarchical model checking are developed based on linear-time temporal logic (LTL), computation-tree logic (CTL) and full computation-tree logic (CTL*). A sequential linear-time temporal logic (sLTL), a sequential computation-tree logic (sCTL), and a sequential full computation-tree logic (sCTL*), which can suitably represent hierarchical information and structures, are developed by extending LTL, CTL and CTL*, respectively. Translations from sLTL, sCTL and sCTL* into LTL, CTL and CTL*, respectively, are defined, and theorems for embedding sLTL, sCTL and sCTL* into LTL, CTL and CTL*, respectively, are proved using these translations. ::: ::: ::: ::: ::: Findings ::: ::: ::: ::: ::: These embedding theorems allow us to reuse the standard LTL-, CTL-, and CTL*-based model-checking algorithms to verify hierarchical systems that are modeled and specified by sLTL, sCTL and sCTL*. ::: ::: ::: ::: ::: Originality/value ::: ::: ::: ::: ::: The new logics sLTL, sCTL and sCTL* and their translations are developed, and some illustrative examples of hierarchical model checking are presented based on these logics and translations. <s> BIB005
can be the empty sequence and is not uniquely determined. Definition 3.2. A structure (Loc, S, S 0 , R, µ s , L ) is a locative inconsistency-tolerant hierarchical probabilistic model iff 1. Loc is a finite non-empty set of locations, 2. S is the set of states, 3. S 0 is a set of initial states and S 0 ⊆ S, 4. R is a binary relation on S which satisfies the condition: ∀s ∈ S ∃s ∈ S [(s, s ) ∈ R], 5. µ s is a certain probability measure concerning s ∈ S: a set of paths beginning at s is mapped into a real number in [0, 1], 6. L is a mapping from S to the power set of d∈SE Φ ∼[d] . A path in a hierarchical probabilistic model is an infinite sequence of states, π = s 0 , s 1 , s 2 , ... such that 1. LIHpCTL is regarded as an extension of the following temporal logics: probabilistic CTL (called pCTL) studied in BIB001 BIB002 , inconsistencytolerant CTL (also called pCTL, but different from the above-mentioned probabilistic one) proposed in  , and hierarchical CTL (called sCTL) proposed in BIB004 BIB005 . 2. There are some possibilities of defining a probability measure µ s . For example, two probability measures µ + s and µ − s , which were defined on a Borel σ-algebra B s , were proposed in (Bianco and de BIB002 . A probability measure µ s , which is concerned with some discrete Markov processes, was proposed in BIB001 . 3. The model checking problem for the probabilistic CTL with the probability measures µ + s and µ − s was shown to be decidable in BIB002 . The model checking problem for the probabilistic CTL with the probability measure µ s was shown to be decidable in BIB001 . 4. The setting of the conditions concerning the negated implication and negated negation in LIH-pCTL is based on the axiom schemes ∼(α→β) ↔ ¬∼α ∧ ∼β and ∼¬α ↔ ¬∼α. These axiom schemes were originally introduced by De and Omori in BIB003 wherein these are shown to be natural and plausible from the point of view of many-valued semantics. 5. The setting of the location operator is the same as that of the locative paraconsistent probabilistic computation tree logic (called LPpCTL) introduced in  . The decidability of the model checking problem for LP-pCTL has not yet been proved. 6. The single-satisfaction relation |= of LIHpCTL is highly compatible with the standard singlesatisfaction relations of CTL. By using this satisfaction relation, we can simply formalize and uniformly handle ∼ and [b] . We then have the following conjecture. Conjecture 3.5 (Decidability).