Norihiro Kamide received his Ph.D. in Information Science from Japan Advanced Institute of Science and Technology in 2000. He is now an associate professor of Teikyo University. His main research areas are Logic in Computer Science, Mathematical Logic and Philosophical Logic. He is interested in non-classical logics and their applications to Software Science and Artificial Intelligence. He is now especially interested in model checking, logic programming and knowledge representation.
Speech Title: Extending Probabilistic Model Checking
Abstract: Model checking is well-known to be a formal and automated technique for verifying concurrent systems, and probabilistic model checking is an extended model checking paradigm that can appropriately verify probabilistic or stochastic concurrent systems. In this study, a locative inconsistency-tolerant hierarchical probabilistic computation tree logic and its subsystems and variants are introduced to establish the logical foundation of our proposed extended probabilistic model checking paradigm. These logics are extensions or modifications of several previously proposed extensions of the standard computation tree logic that has been widely used in model checking. Our proposed extended probabilistic model checking paradigm aims to appropriately verify spatial, inconsistent, hierarchical, and probabilistic concurrent systems. A theorem for embedding a subsystem of the locative inconsistency-tolerant hierarchical probabilistic computation tree logic into a standard probabilistic computation tree logic is proved using a probability-measure-independent translation. The relative decidability theorem 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 existing standard model checking algorithms to verify the systems that can be described using this subsystem. Moreover, in this study, some illustrative examples of our extended probabilistic model checking paradigm, including a verification of the reasoning process behind diagnosing multiple sclerosis, a relatively rare disease, are presented based on the locative inconsistency-tolerant hierarchical probabilistic computation tree logic.
Assoc. Prof. WONG Seng Fat, Alfred, University of Macau, China
Prof. WONG Seng Fat, Alfred is Associate Professor of Electromechanical Engineering of University of Macau, Fellow of Institute of Measurement and Control (InstMC), and Chartered Fellow of Charted Association of Building Engineers (CABE). His research interests are included Human Factors Engineering, Smart City, Medical Engineering, Applied RFID Technology in Industrial Solutions, Industrial Engineering and Engineering Management, Innovative Product Design, and Knowledge Engineering Management. He is enthusiastic in society works. Therefore, he is the president in different societies or engineering associations such as Executive Director of Smart City Alliance Association of Macau (SCAAM), President-Elect of American Society of Heating, Refrigerating and Air-Conditioning Engineers (ASHRAE) Macao Chapter, Former Council President of The Macau Institution of Engineers (MIE), Expert of Shenzhen Association of Ergonomics Application (SAEA), Invited Committee Member of The 8th Committee of Guangdong Provincial Association for Science and Technology, Secretary-general of The 4th Information Technology Committee of Guangdong of Guangdong-Hong Kong-Macau Cooperation Promotion Association, and Committee Member of The 1st Autopilot Working Committee of China Highway and Transportation Society. Moreover, he is Vice President of Macao SAR Government Traffic Services Committee.