HyperPCTL: A Temporal Logic for Probabilistic Hyperproperties

TL;DR

HyperPCTL is a new temporal logic that enables expressing and verifying probabilistic hyperproperties involving multiple system executions, extending traditional probabilistic logics like PCTL to handle complex quantitative relationships.

Contribution

The paper introduces HyperPCTL, a logic that adds explicit quantification over multiple traces to PCTL, allowing for the expression of probabilistic hyperproperties.

Findings

Provides a model checking algorithm for discrete-time Markov chains.

Enables formal reasoning about complex probabilistic dependencies.

Extends the expressiveness of existing probabilistic temporal logics.

Abstract

In this paper, we propose a new logic for expressing and reasoning about probabilistic hyperproperties. Hyperproperties characterize the relation between different independent executions of a system. Probabilistic hyperproperties express quantitative dependencies between such executions. The standard temporal logics for probabilistic systems, i.e., PCTL and PCTL* can refer only to a single path at a time and, hence, cannot express many probabilistic hyperproperties of interest. The logic proposed in this paper, \HyperPCTL, adds explicit and simultaneous quantification over multiple traces to PCTL. Such quantification allows expressing probabilistic hyperproperties. A model checking algorithm for the proposed logic is also given for discrete-time Markov chains.