💻 computer science

Disintegration Temporal Logic for Probabilistic Hyperproperties

This paper introduces Disintegration Temporal Logic (DTL), a new probabilistic temporal logic based on measure disintegration that expresses complex hyperproperties like probabilistic non-interference, and identifies two decidable fragments with efficient model-checking procedures despite the undecidability of the full logic.

Original authors: Mishel Carelli, Bernd Finkbeiner

Published 2026-07-17

📖 6 min read🧠 Deep dive

CC BY 4.0

Original authors: Mishel Carelli, Bernd Finkbeiner

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

The Detective's Dilemma: Tracing Secrets in a Chaotic World

Imagine you are a detective trying to solve a mystery in a bustling, noisy city. In the world of computer science, this city is a "system"—a piece of software or hardware that does things like send messages, control robots, or encrypt your bank data. Usually, we check if a system works by watching a single movie of its life: does it crash? Does it give the right answer? But some mysteries are trickier. They aren't about what happens in one movie, but about how two different movies relate to each other. This is the realm of hyperproperties. It's like asking, "If I change the secret code in the first movie, does the ending of the second movie change?" This is crucial for security; we want to make sure that a hacker's secret actions (the high-level inputs) never leak out into the public view (the low-level outputs).

Now, add a twist: the city isn't just noisy; it's chaotic. The system makes random choices, like rolling dice at every step. This is a probabilistic system. In the past, checking these systems was like trying to predict the weather with a crystal ball that only worked for sunny days. We could check if something happened usually, but we struggled to ask, "If I know exactly what happened in the first half of the story, how does that change the odds of the ending?" This is called conditioning. It's the difference between asking "What are the odds of rain?" and "What are the odds of rain if I see dark clouds right now?" The math behind this gets incredibly messy, especially when the "now" stretches into an infinite future. For a long time, computer scientists hit a wall: they couldn't write a set of rules to check these complex, conditional secrets in systems that make random choices. They needed a new kind of magnifying glass.

The Magic Lens: Disintegration Temporal Logic

Enter Disintegration Temporal Logic (DTL), a new tool introduced by researchers Mishel Carelli and Bernd Finkbeiner. Think of DTL as a super-powered detective's lens that can look at a system's history and instantly re-calculate the odds of the future, no matter how chaotic the past was. The secret sauce behind this lens is a mathematical concept called measure disintegration. In plain English, imagine you have a giant jar of mixed-up colored marbles representing all possible futures of a system. Usually, if you pick a specific, tiny handful of marbles (a specific sequence of events), the odds of picking a red one might be zero because that handful is so small. But DTL uses disintegration to say, "Okay, let's pretend we did pick that specific handful. Given that we are holding these exact marbles, what is the new probability of the next one being red?" It allows the logic to condition probabilities on events that are technically "impossible" to pin down in standard math, like a specific infinite sequence of random choices.

With this new lens, the authors show that we can finally write down rules for some of the most important security secrets. For example, they can express probabilistic non-interference. Imagine a spy (the high-level input) and a civilian (the low-level output). The rule is: "No matter what secret code the spy sends, the civilian's view of the world should look exactly the same." DTL can write this rule down precisely, even if the system is making random choices at every step. They also tackle perfect indistinguishability, which is the gold standard for encryption: "If I encrypt two different messages, the resulting codes should be so similar that you can't tell which message was used, even if you know the history of the encryption process."

However, the authors are honest about the limits of their new tool. They prove that if you try to use the full power of DTL to check every possible question about a system, the computer will get stuck forever; the problem is undecidable. It's like trying to solve a puzzle that has no solution. But, they didn't throw up their hands. Instead, they found two special "fragments" or simplified versions of the logic that do work and can be checked by computers.

The first is the Linear Fragment. This version is great for checking if two things are independent, like our spy and civilian example. The authors show that computers can check these rules very quickly (in polynomial time), making it practical for real-world security checks. The second is the Qualitative Fragment. This version is a bit more relaxed; instead of asking "Is the probability exactly 0.43?", it asks "Is the probability definitely 0 or definitely 1?" This is like asking, "Is it impossible for the spy to leak the secret?" or "Is it guaranteed that the system will crash?" The authors found a way to check these "soft" questions using a method that combines standard logic checking with a clever analysis of the system's loops. While this method is complex (growing very fast as the questions get harder), it is still solvable, unlike the full version.

The paper doesn't just stop at theory; it shows how DTL can be used to model systems interacting with unpredictable environments, like a robot navigating a stormy sea or a network dealing with bursty internet errors. By conditioning on the "weather" (the environment's infinite history), DTL can tell us if the robot is safe specifically when the storm is bad, rather than just on average. This reveals hidden dangers that older methods would miss, like a system that works 99% of the time but fails catastrophically in a specific, rare scenario.

In short, Carelli and Finkbeiner haven't solved every mystery in the chaotic city, but they've handed us a new, powerful flashlight. They've shown us how to mathematically define and check for "perfect secrecy" and "no information leaks" in systems that roll the dice, proving that while the full problem is too hard to solve completely, the most important parts of it are now within our reach.

Technical Summary: Disintegration Temporal Logic for Probabilistic Hyperproperties

1. Problem Statement

Hyperproperties relate multiple execution traces and are essential for specifying security properties like non-interference, robustness, and counterfactual causality. While logics such as HyperLTL successfully handle hyperproperties for non-probabilistic systems, extending these capabilities to probabilistic systems has proven difficult. Existing probabilistic logics, such as HyperPCTL, combine probabilistic reasoning with state quantification but fail to express conditional probabilities conditioned on sequences of events (traces).

This limitation prevents the specification of general probabilistic non-interference, which requires that the probability of a low-level output, conditioned on the low-level history, remains independent of the high-level history. Furthermore, standard probabilistic logics struggle with systems interacting with stochastic environments where one component's execution induces a conditional probability distribution over another. A fundamental mathematical challenge arises here: individual infinite traces typically have probability zero, making standard conditional probability definitions ( $P(A|B) = P(A \cap B)/P(B)$ ) undefined.

2. Methodology

The authors introduce Disintegration Temporal Logic (DTL), a new probabilistic temporal logic grounded in the measure-theoretic concept of measure disintegration.

Core Mathematical Foundation

DTL utilizes measure disintegration (Rokhlin's theorem) to define conditional probabilities even when conditioning on events of probability zero (such as specific infinite traces).

Disintegration Kernel: Given a probability measure $\mu$ on a product space $X \times Y$ , disintegration provides a kernel $\nu$ such that $\mu = \hat{\mu}_X \otimes \nu$ . Intuitively, $\nu(x, \cdot)$ represents the conditional distribution of $Y$ given $X=x$ .
Cuts: To apply this to infinite traces, the authors introduce the notion of a cut, a function $C: AP \to \mathbb{N}_\omega$ that specifies how much of the history of each atomic proposition is "revealed" (conditioned on). A cut partitions the trace space into a prefix (conditioned part) and a suffix (future behavior).
Constructive Disintegration: The paper establishes that disintegration with respect to a cut involving infinite values ( $\omega$ ) can be obtained as the limit of disintegrations with respect to finite prefixes, allowing for constructive computation.

Logic Syntax and Semantics

DTL extends temporal logic with a conditional probability operator $P(\phi \mid [A], B)$ .

Syntax: Formulas include standard temporal operators ( $\mathbf{X}, \mathbf{U}$ ), boolean connectives, and quantitative formulas involving linear combinations of probabilities. The core operator $P(\phi \mid [A], B)$ conditions the satisfaction of $\phi$ on the history of propositions in $A$ up to the current timestamp and the entire infinite history of propositions in $B$ .
Semantics: Satisfaction is defined relative to a trace, a timestamp, a cut, and a measure. The operator updates the cut to reflect the conditioning requirements and evaluates the probability of the subformula using the disintegration measure associated with the updated cut.

3. Key Contributions and Results

Decidability and Complexity

The authors prove that the general model-checking problem for DTL against Markov chains is undecidable (via reduction from the strict cutpoint emptiness problem for Probabilistic Finite Automata). However, they identify two decidable fragments:

The Linear Fragment:
- Capabilities: Expresses conditional independence properties, including general probabilistic non-interference and perfect indistinguishability. It allows comparing probabilities to 1 and checking equality between probabilities.
- Algorithm: Admits a polynomial-time model-checking procedure (PTIME in the size of the Markov chain, EXPTIME in the formula size).
- Technique: The algorithm relies on linear-algebraic techniques and a new construction called Multidynamic Automata, which checks the equivalence of two dynamics on a graph with respect to a quadratic form.
The Qualitative Fragment:
- Capabilities: A probabilistic counterpart to HyperCTL*. Probabilities are compared only to 0 or 1 (soft existential and universal quantification). This fragment captures properties of systems interacting with stochastic environments and distributional properties of Markov Decision Processes (MDPs).
- Algorithm: Admits an automata-theoretic model-checking procedure. The complexity is NSPACE bounded by a tower of exponentials, where the height is linear in the alternation depth of the formula.
- Technique: The algorithm constructs Alternating Büchi Automata (ABA) recursively. It combines standard HyperCTL* reasoning with analysis of Bottom Strongly Connected Components (BSCCs) to handle qualitative probabilistic constraints. It utilizes the cascade property (a conditional independence assumption satisfied by cascade products of systems) to ensure the limit of conditional probabilities is reached in finite steps.

Expressiveness and Applications

The paper demonstrates DTL's ability to express properties previously difficult or impossible to capture:

Probabilistic Non-Interference: Formulated as the independence of the next output from high-level inputs, conditioned on the low-level history.
Perfect Indistinguishability: Expressed as the independence of ciphertext traces from message traces.
Stochastic Environments: DTL can express properties where the probability of a system failure depends on specific infinite executions of an external environment (e.g., "With probability > 0.1, the environment produces a trace such that the conditional probability of failure is > 0.4").
Distributional Properties: DTL replaces strict existential quantification over schedulers with probabilistic quantification over a distribution of schedulers. This allows for decidable verification of properties for probabilistic automata on infinite words, which are undecidable under strict existential quantification.

4. Significance

The paper claims that DTL provides a principled framework for reasoning about interacting stochastic systems where the execution of one component induces conditional probability distributions over another. By leveraging measure disintegration, DTL resolves the mathematical subtleties of conditioning on null events (infinite traces), a problem dating back to the Borel-Kolmogorov paradox.

The significance lies in:

Unification: It unifies the specification of hyperproperties (like non-interference) with probabilistic reasoning in a single logic.
Decidability: It identifies specific, practically relevant fragments (linear and qualitative) that are decidable, offering polynomial-time and automata-theoretic solutions where general probabilistic hyperproperty verification is often undecidable.
Soft Quantification: It introduces a "softer" form of quantification (probabilistic mass of schedulers) that enables decidability for problems (like probabilistic automata on infinite words) that are undecidable under strict existential quantification.

The work establishes a theoretical bridge between measure theory and formal verification, enabling the rigorous analysis of information flow and reliability in complex, interacting probabilistic systems.