Decentralized Planning Using Probabilistic Hyperproperties

TL;DR

This paper introduces a novel framework for multi-agent decentralized planning using probabilistic hyperproperties, extending model checking techniques to handle complex temporal objectives across multiple agents.

Contribution

It proposes a new approach that models multi-agent planning with a single-agent MDP and probabilistic hyperproperties, expanding the expressiveness of specifications in decentralized planning.

Findings

Extended model checking for probabilistic hyperproperties to multi-agent path relations

Demonstrated flexibility and expressiveness through case studies

Established undecidability results linking hyperproperties and Dec-MDPs

Abstract

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.