The Dynamic Turn in Strategy Logics

Abstract

Strategy Logics are well-studied frameworks for the specification and verification of strategic abilities in multi-agent systems (MAS). However, the current generation of Strategy Logics is limited to static reasoning about fixed models of MAS. This limitation excludes a plethora of applications that require addressing dynamic changes and updates. Examples include verifying that a computer program executes correctly after an upgrade, automatically repairing MAS to meet safety requirements, and reasoning about robots operating in a dynamic environment. To address this limitation, we propose a new research agenda centered on enriching Strategy Logics with concepts and intuitions from Dynamic Epistemic Logic, aiming to develop a holistic and general framework that captures dynamic phenomena in MAS and facilitates their verification.