Parity-energy ATL for Qualitative and Quantitative Reasoning in MAS

In this paper, we introduce a new logic suitable to reason about strategic abilities of multi-agent systems where (teams of) agents are subject to qualitative (parity) and quantitative (energy) constraints and where goals are represented, as usual, by means of temporal properties. We formally define such a logic, named parityenergy-ATL (pe-ATL, for short), and we study its model checking problem, which we prove to be decidable with different complexity upper bounds, depending on different choices for the energy range.