Alternating-time Temporal Logic on Finite Traces

Alternating-time Temporal Logic on Finite Traces

Francesco Belardinelli, Alessio Lomuscio, Aniello Murano, Sasha Rubin

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence

We develop a logic-based technique to analyse finite interactions in multi-agent systems. We introduce a semantics for Alternating-time Temporal Logic (for both perfect and imperfect recall) and its branching-time fragments in which paths are finite instead of infinite.  We study validities of these logics and present optimal algorithms for their model-checking problems in the perfect recall case.
Keywords:
Agent-based and Multi-agent Systems: Agent Theories and Models
Agent-based and Multi-agent Systems: Formal Verification, Validation and Synthesis