Invited Speaker---Assoc. Prof. Norihiro Kamide


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: Foundations of Hierarchical Model Checking: Logics, Translations, and Examples
Abstract: Hierarchical model checking is a model-checking paradigm that can appropriately verify systems with hierarchical information and structures. In this study, logics and translations for hierarchical model checking are developed on the basis of 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 struc- tures, 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. 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*. Some illustrative examples of hierarchical model checking are also pre- sented on the basis of the proposed logics and translations.