Robust Alternating-Time Temporal Logic
Abstract
In multi-agent system design, a crucial aspect is to ensure robustness, meaning that for a coalition of agents A, small violations of adversarial assumptions only lead to small violations of A's goals. In this paper we introduce a logical framework for robust strategic reasoning about multi-agent systems. Specifically, inspired by recent works on robust temporal logics, we introduce and study rATL and rATL*, logics that extend the well-known Alternating-time Temporal Logic ATL and ATL* by means of an opportune multi-valued semantics for the strategy quantifiers and temporal operators. We study the model-checking and satisfiability problems for rATL and rATL* and show that dealing with robustness comes at no additional computational cost. Indeed, we show that these problems are PTime-complete and ExpTime-complete for rATL, respectively, while both are 2ExpTime-complete for rATL*.
Cite
@article{arxiv.2307.10885,
title = {Robust Alternating-Time Temporal Logic},
author = {Aniello Murano and Daniel Neider and Martin Zimmermann},
journal= {arXiv preprint arXiv:2307.10885},
year = {2023}
}