An Isaac Newton Institute Programme

Logic and Algorithms

Infinite state model checking in modal logic

17th March 2006

Author: Valentin Goranko (Witwatersrand)

Abstract

In this talk will discuss why model checking of basic modal logic and extensions of it on infinite state systems is interesting and important. In particular, I will present the case of model checking on `rational Kripke models' and its possible applications to regular model checking. Time permitting, I will also discuss how minimal extensions of basic modal logic can be used to specify and verify reachability problems in infinite state transition systems.