Model checking recursive game graphs using dataflow equations

Recursive state machines (RSMs) offer a visual model of the control flow in sequential imperative programs with potentially recursive procedures. A natural way to extend RSMs to model adversarial inputs from the environment is to use Recursive Game Automata (RGAs). These models are closely related to pushdown systems which have been studied
extensively in the model checking and program analysis literature.

In this talk I will describe recursive game automata, and I will describe how old tools from dataflow analysis can provide algorithms for model checking recursive game automata. These algorithms suffer from the same worst-case complexity as known algorithms for pushdown games ([Walukiewicz'96,..]), but offer some  practical advantages, and are intuitively clean and easy to implement and extend.

(describes in part joint work with R. Alur and M. Yannakakis)
 

Home : News : Jamboree : 2003