Robust Alternating-Time Temporal Logic

TL;DR

This paper introduces rATL and rATL* logics for robust strategic reasoning in multi-agent systems, extending ATL and ATL* with multi-valued semantics to handle small violations without increasing computational complexity.

Contribution

It presents new robust temporal logics rATL and rATL* with multi-valued semantics, and analyzes their model-checking and satisfiability complexities, showing no additional computational cost.

Findings

Model-checking for rATL is PTime-complete.

Model-checking for rATL* is ExpTime-complete.

Satisfiability for both logics is 2ExpTime-complete.

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*.