Abstract
We study a class of synchronous, perfect-recall multi-agent systemswith imperfect information and broadcasting (i.e., fully observableactions). We define an epistemic extension of strategy logic withincomplete information and the assumption of uniform and coherentstrategies. In this setting, we prove that the model checking problem,and thus rational synthesis, is decidable with non-elementarycomplexity. We exemplify the applicability of the framework on arational secret-sharing scenario.
Keywords
- Agent-based and Multi-agent Systems: Formal verification, validation and synthesis
- Multidisciplinary Topics and Applications: Validation and Verification
