Invited Speaker---Dr. Norihiro Kamide, Associate Professor

Department of Information and Electronic Engineering, Teikyo University, Japan

Biography: Norihiro Kamide is an associate professor of Teikyo University, Faculty of Science and Engineering, Department of Information and Electronic Engineering. He received his Ph.D. in Information Science from Japan Advanced Institute of Science and Technology in 2000. His main research areas are Logic in Computer Science, Mathematical Logic and Philosophical Logic. He is interested in non-classical logics, including paraconsistent, temporal, description, and substructural logics, and their applications to Software Science and Artificial Intelligence. He is now especially interested in paraconsistent logics and their applications to model checking, logic programming, and knowledge representation.

Speech Title: Logical Foundation of Locative Inconsistency-tolerant Hierarchical Probabilistic Model Checking

Abstract: A locative inconsistency-tolerant hierarchical probabilistic computation tree logic and its subsystems and variants are introduced to establish the logical foundation of our proposed new model checking paradigm. These logics are extensions or modifications of several previously proposed extensions of the standard computation tree logic that is widely used in model checking, which is a well-known formal and automated technique for verifying concurrent systems. Our proposed paradigm, which is called the locative inconsistency-tolerant hierarchical probabilistic model checking, aims to appropriately verify locative (spatial), inconsistent, hierarchical, probabilistic (randomized), and time-dependent concurrent systems. Further, it is expected to be useful in a new application of model checking—to verify mission-critical clinical reasoning regarding disease ontologies. A probability-measure-independent translation from a subsystem of the locative inconsistency-tolerant hierarchical probabilistic computation tree logic into a standard probabilistic computation tree logic is defined, and a theorem for embedding this subsystem into the standard logic is proved using this translation. The relative decidability of this subsystem with respect to the standard logic is proved using this embedding theorem. These embedding and relative decidability results allow us to reuse the standard probabilistic model checking algorithms to verify the systems that can be described using this subsystem. Given that the embeddability and relative decidability problems of the locative inconsistency-tolerant hierarchical probabilistic computation tree logic have not yet been solved, these theorems are considered to be conjectural. Some illustrative examples of our paradigm, including a verification of the reasoning process behind diagnosing multiple sclerosis, a relatively rare disease, are presented. Additionally, a survey of various prior studies on fuzzy, probabilistic, inconsistency-tolerant, and hierarchical temporal logics and their applications in model checking is presented. The results presented in this talk include those in the previously published papers.