Session 1.8c Update: Model Checking Knowledge in Multi-agent Systems with MCK
Tracks
ㅤ
| Tuesday, November 17, 2026 |
| 4:00 PM - 5:00 PM |
| Menzies Theatre |
Presentation Outline
Model Checking is an automated analysis technique for assurance of computer software and hardware, used to verify that a system satisfies a specification stated in a formal logic. Compared to testing, which provides assurance only about the specific scenarios tested, model checking provides exhaustive coverage of all the possible behaviours of the system.
The presentation will describe MCK, a model checker developed at UNSW, which checks specifications stated in a logic that covers knowledge, probability and time in multi-agent systems in which agents have uncertainty about each others' actions and about the state of their environment. In addition to model checking, MCK is also able to automatically synthesize implementations for programs that describe agent behaviour in terms of how an agent acts as a function of its state of knowledge. These "knowledge-based programs'' are able to describe behaviours abstractly, independently of details of how knowledge is acquired in a specific operational environment.
Publications concerning MCK and demonstrator apps are available at http://www.cse.unsw.edu.au/~mck. Examples of the application of MCK will be described, including analysis of pursuit evasion games, computer security and hardware protocol analysis, and the development of optimal algorithms for fault-tolerant distributed systems.
Speaker
Prof Ron Van Der Meyden
UNSW Sydney
ㅤ
Biography
Ron van der Meyden is a Professor in the School of Computer Science and Engineering at UNSW Sydney. His research interests include the foundations of distributed and multi-agent systems and computer security, and his contributions have included work on deontic logic, deductive databases, foundations of public key infrastructure, model checking and synthesis for epistemic logic, and information flow security. He received the ACM Distinguished Scientist Award in 2009.
Ron previously held positions at the University of Technology, Sydney, the Weizmann Institute of Science, and NTT Basic Research Laboratories, Tokyo, and has held visiting positions at NYU and Stanford. He was a member of the teams that constructed successful bids for and established the Cooperative Research Centre for Smart Internet Technology and National ICT Australia (now part of Data61). He served in 2001 as a research program leader in the Cooperative Research Centre for Smart Internet Technology, before establishing the Formal Methods program of National ICT Australia, which he led from 2002 to 2006. Outcomes from this program include the verification of the SeL4 micro-kernel, and Red Lizard Software, a static analysis spinout which was acquired by Synopsys.
Ron previously held positions at the University of Technology, Sydney, the Weizmann Institute of Science, and NTT Basic Research Laboratories, Tokyo, and has held visiting positions at NYU and Stanford. He was a member of the teams that constructed successful bids for and established the Cooperative Research Centre for Smart Internet Technology and National ICT Australia (now part of Data61). He served in 2001 as a research program leader in the Cooperative Research Centre for Smart Internet Technology, before establishing the Formal Methods program of National ICT Australia, which he led from 2002 to 2006. Outcomes from this program include the verification of the SeL4 micro-kernel, and Red Lizard Software, a static analysis spinout which was acquired by Synopsys.
