Disintegration Temporal Logic for Probabilistic Hyperproperties

Abstract

We introduce Disintegration Temporal Logic (DTL), a new probabilistic temporal logic that can express a wide range of probabilistic hyperproperties, including probabilistic non-interference and perfect indistinguishability. DTL is based on the notion of measure disintegration from probability theory, which allows for conditioning probabilities on a finite or infinite sequence of events occurring during a program execution. This naturally supports reasoning about interacting stochastic systems, where complete executions of one component induce conditional probability distributions over another. We illustrate applications of DTL to systems interacting with stochastic environments, distributional properties of Markov decision processes, and probabilistic automata on infinite words, and discuss its relationship to existing probabilistic logics. While model checking Markov chains against full DTL is undecidable, we identify two decidable fragments that capture many hyperproperties of interest. The linear fragment admits a polynomial-time model-checking procedure based on linear-algebraic techniques and captures probabilistic information-flow properties such as perfect indistinguishability and history-based probabilistic non-interference. The qualitative fragment admits an automata-theoretic model-checking procedure that extends the standard algorithm for $\mathit{HyperCTL}^*$ with reasoning about bottom strongly connected components.