Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Hierarchical 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> Hierarchical Temporal Logics <s> An extended full computation-tree logic, CTLS*, is introduced as a Kripke semantics with a sequence modal operator. This logic can appropriately represent hierarchical tree structures where sequence modal operators in CTLS* are applied to tree structures. An embedding theorem of CTLS* into CTL* is proved. The validity, satisfiability and model-checking problems of CTLS* are shown to be decidable. An illustrative example of biological taxonomy is presented using CTLS* formulas. <s> BIB002 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Hierarchical Temporal Logics <s> We propose a proof system for reasoning on certain specifications of secure authentication systems. For this purpose, a new logic, sequence-indexed linear-time temporal logic (SLTL), is obtained semantically from standard linear-time temporal logic (LTL) by adding a sequence modal operator that represents a sequence of symbols. By this sequence modal operator, we can appropriately express message flows between clients and servers and states of servers in temporal reasoning. A Gentzen-type sequent calculus for SLTL is introduced, and the completeness and cut-elimination theorems for it are proved. SLTL is also shown to be PSPACE-complete and embeddable into LTL. <s> BIB003 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Hierarchical Temporal Logics <s> In this paper, we propose a method for modeling concepts in full computation-tree logic with sequence modal operators. An extended full computation-tree logic, CTLS*, is introduced as a Kripke semantics with a sequence modal operator. This logic can appropriately represent hierarchical tree structures in cases where sequence modal operators in CTLS* are applied to tree structures. We prove a theorem for embedding CTLS* into CTL*. The validity, satisfiability, and model-checking problems of CTLS* are shown to be decidable. An illustrative example of biological taxonomy is presented using CTLS* formulas. © 2011 Wiley Periodicals, Inc. ::: ::: (This paper is an extended version of Kamide and Kaneiwa.) <s> BIB004 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Hierarchical 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> BIB005 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Hierarchical Temporal Logics <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> BIB006 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Hierarchical Temporal Logics <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> BIB007
In what follows, we present a survey of various hierarchical (sequential) temporal logics and their applications. Various extended temporal logics employing the sequence (hierarchical) modal operator [b] , where b represents a sequence of symbols, have been investigated to handle hierarchical information BIB002 BIB003 BIB004 BIB005 BIB006 BIB007 . The sequence modal operator [b] can be used to represent the concepts of hierarchical information in the following manner: a sequence structure produces a monoid M, ;, / 0 with the following informational interpretation BIB001 : (1) M is a set of pieces of ordered information (i.e., a set of sequences); (2) ';' is a binary operator (on M) that combines two pieces of information (i.e., it is a concatenation operator on sequences); (3) / 0 is an empty piece of information (i.e., an empty sequence). Then, formulas with the form [b 1 ; b 2 ; · · · ; b n ]α imply that α is true with the sequence b 1 ; b 2 ; · · · ; b n of ordered pieces of information. In addition, formulas with the form [ / 0]α, which coincide with α, imply that α is true without any information (i.e., it is an eternal truth in the sense of classical logic). BIB002 BIB004 introduced CTLS * , which is an extension of CTL * , by adding [b] to CTL * . Similarly, the sequence-indexed lineartime temporal logic (SLTL), which is an extension of LTL, was introduced in by adding [b] to LTL. A proof system for SLTL was developed to verify certain specifications of secure authentication systems. The sequence-indexed paraconsistent computation-tree logic (SPCTL), which is an extension of CTL, was introduced by Kamide in BIB005 by adding [b] and ∼ to CTL. As explained above, SPCTL was used to verify clinical reasoning through inconsistency-tolerant hierarchical model checking. In BIB006 BIB007 , thesequential linear-time temporal logic (sLTL) and sequential computation-tree logic (sCTL) were developed by extending LTL and CTL, respectively, to obtain the logical foundation of hierarchical model checking. The hierarchical (sequential) temporal logics sCTL and sLTL proposed by BIB006 BIB007 adopted a simple single-satisfaction relation to obtain various simple and efficient translation methods for hierarchical model checking. Although the previously proposed logics, CTLS * BIB002 BIB004 , SLTL , and SPCTL BIB005 , have complex multiple sequence-indexed satisfaction relations, |=d, sLTL and sCTL BIB006 BIB007 have a simple single-satisfaction relation, |= , which is highly compatible with the standard single-satisfaction relations of LTL, CTL, and CTL * . Using this simple satisfaction relation, embedding theorems can be easily proven, and the operator [b] can be formalized simply and handled uniformly.