Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> INTRODUCTION <s> A unified approach to program verification is suggested, which applies to both sequential and parallel programs. The main proof method suggested is that of temporal reasoning in which the time dependence of events is the basic concept. Two formal systems are presented for providing a basis for temporal reasoning. One forms a formalization of the method of intermittent assertions, while the other is an adaptation of the tense logic system Kb, and is particularly suitable for reasoning about concurrent programs. <s> BIB001 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> INTRODUCTION <s> In this paper the full branching time logic (CTL*) is studied. It has basic modalities consisting of a path quantifier, either A (“for all paths”) of E (“for some path”), followed by an arbitrary linear time assertion composed of unrestricted combinations of the usual linear temporal operators F (“sometime”), G (“always”), X (“nexttime”), and U (“until”). It is shown that the problem of determining if a CTL* formula is satisfiable in a structure generated by a binary relation is decidable in triple exponential time. The decision procedure exploits the special structure of the finite state ω -automata for linear temporal formulae which allows them to be determinized with only a single exponential blowup in size. Also the expressive power of tree automata is compared with that of CTL* augmented by quantified auxillary propositions. <s> BIB002 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> INTRODUCTION <s> The differences between and appropriateness of branching versus linear time temporal logic for reasoning about concurrent programs are studied. These issues have been previously considered by Lamport. To facilitate a careful examination of these issues, a language, CTL * , in which a universal or existential path quantifier can prefix an arbitrary linear time assertion, is defined. The expressive power of a number of sublanguages is then compared. CTL* is also related to the logics MPL of Abrahamson and PL of Harel, Kozen, and Parikh. The paper concludes with a comparison of the utility of branching and linear time temporal logics. <s> BIB003 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> INTRODUCTION <s> We Propose a method of constructing concurrent programs in which the synchronization skeletonof the program is automatically synthesized from a high-level (branching time) Temporal Logic specification. The synchronization skeleton is an abstraction of the actual program where detail irrelevant to synchronization is suppressed. For example, in the synchronization skeleton for a solution to the critical section problem each process's critical section may be viewed as a single node since the internal structure of the critical section is unimportant. Most solutions to synchronization problems in the literature are in fact given as synchronization skeletons. Because synchronization skeletons are in general finite state, the propositional version of Temporal Logic can be used to specify their properties. <s> BIB004 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> INTRODUCTION <s> Introductory overview.- Splicing logics: Syntactic fibring.- Splicing logics: Semantic fibring.- Heterogeneous fibring.- Fibring non-truth functional logics.- Fibring first-order logics.- Fibring higher-order logics.- Modulated fibring.- Splitting logics.- New trends: Network fibring.- Summing-up and outlook. <s> BIB005
In this paper, we introduce a locative inconsistencytolerant hierarchical probabilistic computation tree logic (LIHpCTL), which is designed to form the logical foundation of a new model checking paradigm. This paradigm is intended to appropriately verify locative (spatial), inconsistent, hierarchical, probabilistic (randomized), and time-dependent concurrent systems. LIHpCTL is an extension of several previously proposed locative, inconsistency-tolerant, hierarchical, and probabilistic extensions of the standard temporal logic known as CTL BIB004 , which is widely used for model checking BIB004    . Model checking is a well-known formal and automated technique for verifying concurrent systems. Although the decidability of model checking based on LIHpCTL has not been determined yet, we present an illustrative example of the novel LIHpCTL-based model checking paradigm. In what follows, we present a brief explanation of several standard and extended temporal logics and their applications to model checking. The following are well-known standard temporal logics typically used in model checking: computation tree logic (CTL) BIB004 , linear-time tem-poral logic (LTL) BIB001 , and full computation tree logic (CTL * ) BIB002 BIB003 . The logic CTL BIB004 is one of the most useful temporal logics for model checking; it is based on the branching-time paradigm, which uses computation trees to represent the passage of time. The logic LTL BIB001 is another form of temporal logic widely used for model checking; it is based on the linear-time paradigm, which uses linear order to represent the passage of time. The logic CTL * BIB002 BIB003 ) is more expressive than LTL and CTL; it is based on the branching-time paradigm with path quantifiers to represent the passage of time. To extend the above-mentioned temporal logics, other useful non-classical logics must be combined and integrated in a natural way. This is also an important issue in mathematical logic BIB005 . The following logics can be utilized for this purpose: probabilistic (probability) logics, inconsistency-tolerant (paraconsistent) logics, hierarchical (sequential) logics, and spatial (locative) logics. By combining and integrating these logics, we can extend and refine the existing standard model-checking framework. Model checking has been extended to probabilistic model checking (Aziz