Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Decentralized Planning Using Probabilistic Hyperproperties

Francesco Pontiggia, Filip Macák, Roman Andriushchenko, Michele Chiari, Milan Češka

TL;DR

This paper introduces PHyperLTL (PHLTL), a novel specification language for decentralized planning under uncertainty by coupling probabilistic hyperproperties with an MDP-based representation of a single agent’s environment. It develops a synchronised-product abstraction and an abstraction-refinement loop to search for joint policies that satisfy temporal hyperproperties across multiple agents, and it identifies a tractable fragment, PHLTLDEC, that reduces to Dec-MDP planning while highlighting undecidability in the general setting. The authors provide theoretical results (undecidability proofs and complexity bounds) and demonstrate empirical performance on grid-based benchmarks, often outperforming the state-of-the-art Dec-POMDP solver Inf-JESP. The work bridges probabilistic hyperproperty verification and decentralized planning, enabling richer coordination specs at the cost of exponential state-space growth, and lays groundwork for applying existing decentralized planning tools to PH hyperproperty verification.

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.

Decentralized Planning Using Probabilistic Hyperproperties

TL;DR

This paper introduces PHyperLTL (PHLTL), a novel specification language for decentralized planning under uncertainty by coupling probabilistic hyperproperties with an MDP-based representation of a single agent’s environment. It develops a synchronised-product abstraction and an abstraction-refinement loop to search for joint policies that satisfy temporal hyperproperties across multiple agents, and it identifies a tractable fragment, PHLTLDEC, that reduces to Dec-MDP planning while highlighting undecidability in the general setting. The authors provide theoretical results (undecidability proofs and complexity bounds) and demonstrate empirical performance on grid-based benchmarks, often outperforming the state-of-the-art Dec-POMDP solver Inf-JESP. The work bridges probabilistic hyperproperty verification and decentralized planning, enabling richer coordination specs at the cost of exponential state-space growth, and lays groundwork for applying existing decentralized planning tools to PH hyperproperty verification.

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.

Paper Structure

This paper contains 36 sections, 4 theorems, 10 equations, 1 figure, 2 tables.

Table of Contents

  1. Introduction
  2. Decentralized planning under uncertainty
  3. Planning of multi-agent systems using temporal logics
  4. Probabilistic hyperproperties
  5. Motivating example.
  6. Contributions
  7. Decentralized planning with complex shared objectives
  8. Verification of Hyperproperties
  9. Background
  10. Temporal Logic
  11. PHLTL
  12. PHLTL Syntax
  13. Formal Semantics
  14. Related Logics
  15. Undecidability
  16. ...and 21 more sections

Key Result

theorem 1

PHLTL model checking is undecidable.

Figures (1)

  • Figure 1: Running example on a 4x4 grid with 2 agents and a target cell $T$. The goal is to ensure that the red agent reaches $T$ first. (a) An illustration of the optimal memoryless policies. (b) The considered slipping factor. (c) A 2-node controller representing the optimal policy for the blue agent (the labels describes the transitions between the nodes). (d) An illustration including the optimal policy for the blue agent.

Theorems & Definitions (10)

  • definition 1: MDP
  • definition 2: MDP self-composition
  • definition 3
  • definition 4: DRA
  • theorem 1
  • definition 5: Synchronised product
  • theorem 2
  • definition 6: Policy consistency
  • theorem 3
  • corollary 1