Decentralized Planning Using Probabilistic Hyperproperties
This work addresses the problem of specifying complex temporal objectives in decentralized multi-agent systems for researchers in formal methods and AI planning, though it is incremental in extending existing model checking techniques.
The paper tackles multi-agent planning under stochastic dynamics by proposing a new approach using probabilistic hyperproperties to capture temporal objectives for decentralized agents, demonstrating its flexibility and expressiveness through case studies and establishing undecidability results for a subclass.
Multi-agent planning under stochastic dynamics is usually formalised using decentralized (partially observable) Markov decision processes ( MDPs) and reachability or expected reward specifications. In this paper, we propose a different approach: we use an MDP describing how a single agent operates in an environment and probabilistic hyperproperties to capture desired temporal objectives for a set of decentralized agents operating in the environment. We extend existing approaches for model checking probabilistic hyperproperties to handle temporal formulae relating paths of different agents, thus requiring the self-composition between multiple MDPs. Using several case studies, we demonstrate that our approach provides a flexible and expressive framework to broaden the specification capabilities with respect to existing planning techniques. Additionally, we establish a close connection between a subclass of probabilistic hyperproperties and planning for a particular type of Dec-MDPs, for both of which we show undecidability. This lays the ground for the use of existing decentralized planning tools in the field of probabilistic hyperproperty verification.