Invited speaker

Wojtek Jamroga (Polish Academy of Sciences)

On Module Checking and Strategies (joint work with Aniello Murano)

Two verification problems are very close in spirit: _model_ checking and _module_ checking. Model checking typically assumes a "closed" system, in the sense that all the possible events are included in the model of the system. In contrast, module checking was designed for verification of "open" systems, i.e., ones that are coupled with an external environment whose behavior cannot be fully predicted.
When reasoning about multi-agent strategic interaction is allowed, the difference seems to be mostly a matter of presentation. In particular, model checking of the strategic logic ATL appears to be a natural extension of module checking for the temporal logic CTL. In fact, it was commonly believed that the former subsumes the latter in a straightforward way.
We show that, on the contrary, the two problems are fundamentally different. The way in which behavior of the environment is understood in module checking cannot be equivalently characterized in ATL. Moreover, if one wants to embed module checking in ATL then its semantics must be extended with two essential features, namely nondeterministic strategies and long-term commitment to strategies.
Finally, we study a variant of module checking where the specification of objectives is given in the richer language of ATL. We prove that the resulting "reactive" semantics of ATL increases the expressive power of the logic. On the other hand, it admits so called non-behavioral strategies, which is usually considered counterintuitive.