AI summaryⓘ
The authors present Disintegration Temporal Logic (DTL), a new type of probabilistic logic that helps describe complex properties about how systems behave over time, especially when randomness and interaction are involved. DTL uses a probability concept called measure disintegration to better understand how one part of a system influences the probabilities in another during execution. They show how DTL can be applied to various systems like Markov decision processes and probabilistic automata, and identify parts of the logic where checking if a system meets a property is computationally manageable. This includes a linear fragment suited for certain information security properties and a qualitative fragment that builds on existing logical frameworks.
probabilistic temporal logicmeasure disintegrationprobabilistic hyperpropertiesnon-interferenceMarkov decision processesprobabilistic automatamodel checkinglinear fragmentqualitative fragmentHyperCTL*
Authors
Mishel Carelli, Bernd Finkbeiner
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.