CTL/ACTL Model Update: The Model Explosion Problem and Counterexample Guided Update

Title: CTL/ACTL Model Update: The Model Explosion Problem and Counterexample Guided Update
Speaker: Professor Yan Zhang, Intelligent Systems Laboratory, School of Computing and Mathematics University of Western Sydney, Australia
Time: 10:00am, Tuesday June 12
Venue: Lecture room, Lab for Computer Science, Level 3 Building #5, Institute of Software, CAS

Abstract:Model checking is a promising technology, which has been applied for verification of many hardware and software systems. In this talk, we introduce the concept of model update towards the development of automatic system modification tool that extends model checking functions. We first define primitive model operations on Computational Tree Logic (CTL) models and formalize the principle of minimal change for CTL model update. We address the model explosion problem that is embedded in our CTL model update approach, and propose an optimization method to improve our model update approach. Based on this discussion, we then focus on counterexample guided ACTL model update, and demonstrate how a combined structure based minimal change principle can be developed for the tree-like ACTL counterexample updates.

About the speaker:
Prof Yan Zhang obtained his PhD degree in Computer Science from University of Sydney in 1994. He joined University of Western Sydney in 1995, and established the Intelligent Systems Laboratory in the School of Computing and Mathematics. Prof Yan Zhang’s research interests include knowledge representation and reasoning, nonmonotonic logic programming, epistemic reasoning for intelligent systems, information security, model checking and modification, and computational complexity for dynamic system modeling.
In recent years, he has published significant results in these areas in top international journals and conferences such as journals Artificial Intelligence, ACM Transactions on Computational Logic, and IJCAI, AAAI, ECAI and KR conferences.