Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Locative Temporal Logics <s> We propose a framework of distributed concurrent linear logic programming, which can elegantly capture the essential features of distributed computation: location-dependence/independence of names and movement of computation. We first define the syntax and semantics of a modal linear logic that is suitable for expressing distributed computation, and then show that there is a close relationship between formulas of a fragment of the modal linear logic and distributed processes. <s> BIB001 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Locative Temporal Logics <s> A spatial modal logic (SML) is introduced as an extension of the modal logic S4 with the addition of certain spatial operators. A sound and complete Kripke semantics with a natural space (or location) interpretation is obtained for SML. The finite model property with respect to the semantics for SML and the cut-elimination theorem for a modified subsystem of SML are also presented. (© 2005 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim) <s> BIB002 </s> Towards Locative Inconsistency-tolerant Hierarchical Probabilistic CTL Model Checking: Survey and Future Work <s> Locative Temporal Logics <s> A temporal spatial epistemic intuitionistic linear logic (TSEILL) is introduced, and the completeness theorem for this logic is proved with respect to Kripke semantics. TSEILL has three temporal modal operators: [F] (any time in the future), [N] (next time) and [P] (past), some spatial modal operators [li] (locations), two epistemic modal operators; [K] (know) and (K), and a linear modal operator ! (exponential). A basic normal modal intuitionistic affine logic (BIAL) and its normal extensions are also defined, and the completeness theorems for these logics are proved with respect to Kripke semantics. In the proposed semantic framework of these normal extensions, a simple correspondence can be given between frame conditions and Lemmon-Scott axioms. A dynamic intuitionistic affine logic (DIAL) is proposed as an affine version of (test-free) dynamic logic, and the completeness theorem for this logic is shown with respect to Kripke semantics. Finally, some intuitive interpretations, such as resource and informational interpretations, are given for the proposed logics and semantics. By using these logics, semantics and interpretations, various kinds of fine-grained resource-sensitive reasoning can be expressed. <s> BIB003
Future studies should aim to extend the previously proposed standard and extended temporal logics by adding a location (locative) operator, [l i ]. By adding this operator to previously proposed logics, locative (spatial) properties within the model checking framework can be appropriately handled. The location operator was originally introduced by BIB001 ) using a structural congruence relation in the formalization of a distributed concurrent linear logic programming language. The location operator was also reformulated by Kamide in BIB002 BIB003 and the reformulated operator was a variant of the original setting by BIB001 . In fact, the framework of the original operator was improved in BIB002 BIB003 ) as a purely logical formulation without any structural congruence relations. Formulas with the form [l i ]α can be interpreted as follows: proposition α holds at location l i . Various locative (spatial) temporal logics employing the location operator [l i ] have been investigated to handle distributed concurrent systems. For example, the locative paraconsistent probabilistic computation tree logic (LPpCTL) was introduced by Kamide and Koizumi in  by adding [l i ] to the inconsistency-tolerant (paraconsistent) probabilistic computation tree logic, PpCTL. By integrating the findings of the above-mentioned studies with the findings in  , we intend to establish a logical foundation for the proposed framework of locative inconsistency-tolerant hierarchical probabilistic model checking based on LIHpCTL employing [l i ]. Assuming a space domain Loc and operator [l] with l ∈ Loc, the satisfaction relation (s, l) |= α of LPpCTL can be interpreted as follows: proposition α holds at time state s and location l. Then, various properties and situations with space and time can be expressed using LPpCTL formulas. The following liveness property is an example: "If we input the login password of host computer Comp3 at one of the mobile computers Comp1 and Comp2, then we will eventually be able to log in to Comp3." This can be formally expressed as AG ([comp1] 