July 1, 2019
Wojtek Jamroga (Polish Academy of Sciences)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.