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 \(^*\).

Authors

• Aniello Murano
• Daniel Neider
• Martin Zimmermann 0002

Keywords

No keywords are indexed for this paper.