### 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.