Strategic Reasoning in Formal Verification (invited talk)

Abstract: In open system verification, to formally check for reliability, one needs an appropriate formalism to model the interaction between agents and express the correctness of the system no matter how the environment behaves. Important contributions in this context are given by module checking (a.k.a., module checking of open systems) and modal logics for strategic ability, in the setting of multi-agent games, such as ATL, ATL*, and the like. In this talk, I will first recall and compare these two different approaches. Then, I will introduce Strategy Logic (SL) as a powerful logic framework for reasoning explicitly about strategies in multi-agent concurrent games, which includes both. In particular, I will mainly discuss about the model checking and the satisfiability questions for SL. As a key aspect, SL uses first-order quantifications over strategies, where strategies are not glued to a specific agent, but an explicit binding operator allows to bind an agent to a strategy variable. Notably, this allows agents to share strategies or reuse one previously adopted.