Careful Autonomous Agents in Environments With Multiple Common Resources

TL;DR

This paper extends the concept of careful rational synthesis from a single resource to multiple resources, showing undecidability in general but decidability under bounded resource constraints, aligning with controller synthesis complexity.

Contribution

It introduces a multi-resource careful rational synthesis framework, proves undecidability in the general case, and demonstrates decidability when resources are bounded, connecting to LTL controller synthesis.

Findings

Decidability is lost with multiple resources in general.

Bounded resources restore decidability.

Complexity matches that of LTL controller synthesis.

Abstract

Careful rational synthesis was defined in (Condurache et al. 2021) as a quantitative extension of Fisman et al.'s rational synthesis (Fisman et al. 2010), as a model of multi-agent systems in which agents are interacting in a graph arena in a turn-based fashion. There is one common resource, and each action may decrease or increase the resource. Each agent has a temporal qualitative objective and wants to maintain the value of the resource positive. One must find a Nash equilibrium. This problem is decidable. In more practical settings, the verification of the critical properties of multi-agent systems calls for models with many resources. Indeed, agents and robots consume and produce more than one type of resource: electric energy, fuel, raw material, manufactured goods, etc. We thus explore the problem of careful rational synthesis with several resources. We show that the problem is undecidable. We then propose a variant with bounded resources, motivated by the observation that in practical settings, the storage of resources is limited. We show that the problem becomes decidable, and is no harder than controller synthesis with Linear-time Temporal Logic objectives.