1 Introduction↩︎

Hyperproperties are system properties that relate multiple execution traces [1]. They arise naturally in areas such as information-flow security, multi-agent systems, and counterfactual reasoning. There is substantial interest in finding expressive specification logics that capture a large set of relevant hyperproperties and yet have verification problems with acceptable computational cost (cf. [2]).

For circuits and other non-probabilistic systems, simple variations of the standard temporal logics, such as HyperLTL [3], the extension of linear-time temporal logic (LTL) with quantification over multiple traces, have proven to be powerful unifying frameworks. Such logics cover a large class of hyperproperties, including notions like non-interference, robustness, and counterfactual causality, that were previously studied in isolation. For probabilistic systems, the quest for general specification logics has turned out to be more difficult. A typical example of a probabilistic temporal logic is HyperPCTL [4], which combines standard probabilistic reasoning from logics like PCTL [5] with quantification over states. This allows for the specification of restricted versions of probabilistic non-interference, such as that an output distribution must not depend on the initial state. However, logics like HyperPCTL cannot refer to conditional probabilities. As a result, such logics cannot express notions like probabilistic non-interference in full generality, which is needed for systems that communicate reactively through low-security and high-security channels [6].

Consider a system that, at every step, receives a low-security input and a high-security input in variables \(l\) and \(h\) and, based on the previous trace and the current inputs, probabilistically determines the value of a binary output variable \(o\). Probabilistic non-interference requires that for any low-level input trace \(L\) of length \(n\), any high-level input trace \(H\) of length \(n\), and any low-level output trace \(O\) of length \(n\), such that the joint probability \(\mathbb{P}(H,L,O) > 0\), the probability of \(o\) being true at step \(n\) conditioned on \((H,L,O)\), is the same as the probability conditioned only on \((L,O)\). Intuitively, this property expresses that the high-level input trace does not provide additional information about the next output, once the low-level input and output history is fixed.

To express properties like general probabilistic non-interference in a temporal logic, the logic must support both temporal reasoning and probabilistic reasoning with conditioning on sequences of events. In this paper, we introduce Disintegration Temporal Logic (DTL), which provides such a combination. DTL expresses general probabilistic non-interference as the following formula: \[\label{nonint} \mathbb{P}\!\Bigl( \LTLglobally \bigl( \mathbb{P}(\LTLnext o \mid [h,l,o]) = \mathbb{P}(\LTLnext o \mid [l,o]) \bigr) \Bigr) = 1.\tag{1}\] Here, \(\mathbb{P}(\LTLnext o \mid [h,l,o])\) denotes the probability that \(o\) is true at the next step, conditioned on the history of \(h\), \(l\), and \(o\). Analogously, \(\mathbb{P}(\LTLnext o \mid [l,o])\) conditions only on the history of \(l\) and \(o\). The globally operator \(\LTLglobally\) has the usual meaning, that the subformula must hold at every point in time, and \(\mathbb{P}(\cdot)=1\) requires that the property holds for almost every trace (up to a set of measure zero). Combining these components, we obtain that the formula (1 ) holds for a system \(M\) if the system satisfies probabilistic non-interference.

In addition to conditioning on finite sequences of events, DTL also allows for conditioning on infinite sequences. This naturally arises in systems consisting of several interacting stochastic components. Consider a system interacting with an external stochastic environment modeled by a Markov chain. DTL can express properties such as With probability at least \(0.1\), the environment produces an execution such that, conditioned on this execution, the probability that the system exhibits the undesirable behavior is greater than \(0.4\). This is expressed by the formula \[M\vDash\mathbb{P}\Bigl( \mathbb{P}\bigl( \phi_{bad} \mid AP_{env}\bigr) > 0.4 \Bigr) > 0.1.\]

Here, \(AP_{env}\) denotes the set of actions produced by the environment. Note that we write \(AP_{env}\) rather than \([AP_{env}]\), corresponding to conditioning on the full infinite trace rather than on a finite prefix as in formula (1 ).

Beyond these motivating examples, DTL also naturally expresses distributional properties of Markov decision processes and properties of probabilistic automata on infinite words, establishing connections to existing probabilistic verification frameworks.

The mathematical foundation of DTL is the notion of measure disintegration. Disintegration allows us to define conditional probabilities even when conditioning on events of probability zero. This is essential in our setting, since individual infinite traces typically have probability zero, yet we still want to condition on them. The problem of defining conditional probabilities in such cases dates back to Kolmogorov [7] and the Borel–Kolmogorov paradox, which illustrates the subtlety of conditioning on null events. Measure-theoretic disintegration, established by Rokhlin [8], provides a principled resolution of this issue [9], [10].

For full DTL, the model checking problem (determining whether a formula is satisfied by a given Markov chain) is undecidable. However, we identify two decidable fragments that capture many hyperproperties of interest.

The linear fragment allows comparing probabilities to \(1\) as well as checking the equality between probabilities. This fragment can express conditional independence properties, including probabilistic non-interference and perfect indistinguishability. The linear fragment admits polynomial-time model checking based on linear-algebraic reasoning, similar in spirit to algorithms for checking equivalence of labeled Markov chains [11].

The qualitative fragment can be viewed as a probabilistic counterpart of the widely used hyperproperty logic HyperCTL\(^*\) [3]. In this fragment, probabilities may only be compared to \(0\) or \(1\), yielding “soft” versions of existential and universal quantification. The qualitative fragment can express, among others, properties of systems interacting with stochastic environments that compare probabilities only to \(0\) and \(1\). We present a model-checking algorithm for this fragment that combines reasoning about bottom strongly-connected components with the standard HyperCTL\(^*\) model-checking procedure. The resulting complexity is a tower of exponentials whose height is linear in the alternation depth of the formula.

The remainder of the paper is organised as follows:

• Section 2 presents preliminaries, introduces measure disintegration, and establishes key properties of disintegration on spaces of infinite traces.

• Section 3 defines the syntax and semantics of DTL and justifies the semantics using measure-theoretic arguments.

• Section 4 demonstrates how to express different properties in DTL and relates it to existing logics.

• Sections 5 and 6 introduce the linear and qualitative fragments and provide corresponding model-checking algorithms.

• Section 7 concludes.

2 Preliminaries↩︎

In this section, we introduce both well-known concepts and new notions that are used throughout the paper.

We begin with notations, followed by basic definitions from probability theory on the space of infinite words. We then introduce the fundamental concept of conditioning via measure disintegration, which forms the basis of our logic. Next, we describe our approach to conditioning on the space of infinite words through the notion of a cut, and present several technical results that provide a constructive interpretation of the abstract concept of disintegration in the space of infinite words. Finally, we define Markov chains, Markov decision processes, and various types of automata.

2.1 Notations↩︎

Let \(\mathbb{N}\), \(\mathbb{R}\), and \(\mathbb{R}_+\) denote the sets of natural numbers, real numbers, and non-negative real numbers, respectively. \(\mathbb{N}_{\omega}\), denotes the set \(\mathbb{N}\cup \{\omega \}\), with a linear order, extended from \(\mathbb{N}\), with \(\omega>n\), for every \(n\in \mathbb{N}\).

Given an element \(s\in X\times Y\), \(s_X\) denotes the projection of \(s\) on \(Y\).

Given a set \(X\) and \(n \in \mathbb{N}\), we write \(2^X\) for the set of all subsets of \(X\), \(X^n\) for the set of sequences of elements of \(X\) of length \(n\), \(X^* = \bigcup_{n \in \mathbb{N}} X^n\), and \(X^\omega\) for the set of all infinite sequences of elements of \(X\), called traces. Given a subset \(Y\subseteq X\), \(\overline{Y}\) denotes the complement of \(Y\).

Given a trace \(\pi \in X^\omega \cup X^*\) and \(n \in \mathbb{N}\), let \(\pi(n)\) denote the \(n\)-th element of \(\pi\) if it exists, and let \(\pi[n]\) denote the prefix of \(\pi\) of length \(\min\{n, |\pi|\}\).

Given \(\pi \in X^*\) and \(\rho \in X^\omega \cup X^*\), their concatenation is denoted by \(\pi \rho\). For \(Y \subseteq X^*\) and \(Z \subseteq X^\omega \cup X^*\), we define their concatenation element-wise by \(YZ = \{ \pi \rho \mid \pi \in Y \text{ and } \rho \in Z \}.\) For \(\pi \in X^*\) and \(Z\subseteq X^\omega \cup X^*\), denote \(\pi Z = \{ \pi\} Z\).

2.2 Probability measure on infinite words↩︎

Given a set \(X\), a \(\sigma\)-algebra on \(X\) is a non-empty collection \(\mathcal{X} \subseteq 2^X\) that is closed under complementation and countable unions and intersections. A measurable space is a pair \((X,\mathcal{X})\), where \(X\) is a set and \(\mathcal{X}\) is a \(\sigma\)-algebra on \(X\).

Given a countable set \(X\), the Cantor \(\sigma\)-algebra on \(X^\omega\) is the minimal \(\sigma\)-algebra containing the cylinder sets of the form \(\mathsf{Cyl}(\pi) := \{ \pi \rho \mid \rho \in X^\omega \}\), where \(\pi \in X^*.\) We always assume the Cantor \(\sigma\)-algebra on \(X^\omega\) and omit mentioning it.

Let \((X,\mathcal{X})\) and \((Y,\mathcal{Y})\) be measurable spaces. A function \(f \colon X \to Y\) is measurable if \(f^{-1}(B) \in \mathcal{X}\) for every \(B \in \mathcal{Y}\). The product \(\sigma\)-algebra on \(X \times Y\) is the smallest \(\sigma\)-algebra containing all rectangles of the form \(A \times B\) with \(A \in \mathcal{X}\) and \(B \in \mathcal{Y}\). We denote it by \(\mathcal{X} \otimes \mathcal{Y}\).

A finite measure on \((X,\mathcal{X})\) is a function \(\mu \colon \mathcal{X} \to \mathbb{R}_+\) such that \(\mu(\emptyset) = 0\) and \(\mu\) is countably additive, i.e. \(\mu (\bigcup_{n \in \mathbb{N}} A_n) = \sum_{n \in \mathbb{N}} \mu(A_n)\) for every sequence of pairwise disjoint sets \(A_1, A_2, \dots \in \mathcal{X}\). A measure \(\mu\) is called a probability measure if \(\mu(X) = 1\).

We denote by \(\mathcal{M}(X,\mathcal{X})\) and \(\mathcal{P}(X,\mathcal{X})\) the sets of finite measures and probability measures on \((X,\mathcal{X})\), respectively.

Any countably additive function from the set of cylinder sets of \(X^\omega\) to \([0;1]\), that maps \(\emptyset\) to \(0\), extends uniquely to a probability measure on \(X^\omega\) [5].

Given a measure \(\mu\) on \((X\times Y , \mathcal{X}\otimes\mathcal{Y})\), define a marginal measure \(\hat{\mu}_X\) on \((X,\mathcal{X})\) for any \(B\in \mathcal{X}\) as \(\hat{\mu}_X(B) = \mu(B\times Y)\).

A property on \(X\) (for example, the equivalence of two functions or of two sets) is said to hold almost everywhere with respect to a measure \(\mu\) (written \(\mu\)-a.e.), if the set of points where the property fails has \(\mu\)-measure zero.

For the real-valued measurable function \(f:X\to \mathbb{R}\), measure \(\mu\) and a measurable subset \(A\subseteq X\) we denote an integral of \(f\) with respect to \(\mu\) over \(A\) as \(\int_A f(x) \mu(dx).\) For the definition of the integral and a more comprehensive introduction to measure theory, we refer to [9], [12].

2.3 Conditioning and Disintegration↩︎

The standard definition of the probability of an event \(A\) conditioned on an event \(B\) is given by \[\mathbb{P}(A\mid B) = \frac{\mathbb{P}(A\cap B)}{\mathbb{P}(B)}.\] This formula is well-defined only when \(\mathbb{P}(B)\neq 0\). However, in many situations, we would like to condition on events of probability \(0\).

Consider, for example, the uniform distribution on the unit square \([0,1]\times [0,1]\). Intuitively, if we condition on the first coordinate being equal to \(0.3\), the second coordinate should remain uniformly distributed on \([0,1]\). However, the event that the first coordinate is exactly \(0.3\) has probability \(0\), so such a conditional distribution is not defined by the standard formula above. To address this issue, probability theory uses the notion of measure disintegration.

Quoting [9]: "Modern probability theory can be said to begin with the notions of conditioning and disintegration."

Intuitively, if we have a measure on \(X\times Y\), the disintegration of this measure is a well-behaved choice of conditional measures \(\mu_x\) on \(Y\), indexed by points \(x\in X\), called kernel.

Let \((X,\mathcal{X})\) and \((Y,\mathcal{Y})\) be measurable spaces. Formally, a kernel from \(X\) to \(Y\) is a function \(\nu \colon X \to \mathcal{M}(Y,\mathcal{Y})\) such that for every \(B \in \mathcal{Y}\), the map \(x \mapsto \nu(x)(B)\) is measurable.

Given a measure \(\mu\in \mathcal{M}(X,\mathcal{X})\) and a kernel \(\nu: X \to \mathcal{M}(Y,\mathcal{Y})\) their composition measure \(\mu\otimes \nu \in \mathcal{M}(X\times Y, \mathcal{X}\otimes\mathcal{Y})\) is given by \[(\mu\otimes \nu) (A\times B) = \int_A \nu(x)(B) \mu(dx).\]

Intuitively, for each slice corresponding to a fixed value \(x\in X\), the measure on \(Y\) is given by \(\nu(x)\), and these slice measures are then averaged according to \(\mu\).

A measurable space \((X,\mathcal{X})\) is called standard Borel if there exists a metric on \(X\) that makes a complete, separable space, such that \(\mathcal{X}\) is the associated Borel \(\sigma\)-algebra.

We use the fact that \(X^\omega\) with Cantor \(\sigma\)-algebra is standard Borel when \(X\) is finite or countable [13], which suffices to apply the following result from [9].

We call such \(\nu\) a disintegration kernel of \(\mu\) with respect to \(X\) and denote \(\nu(x,\cdot)\) as \(\mu_x\). Intuitively, \(\mu_x\) represents the conditional distribution of \(Y\) given \(X = x\).

Returning to the example above, let \(\mu\) be the uniform distribution on \([0,1]\times [0,1]\). Disintegrating \(\mu\) with respect to the first coordinate yields that, for almost every \(x\in [0,1]\), the measure \(\mu_x\) is the uniform distribution on \([0,1]\). The qualification “almost every” is necessary because the disintegration kernel is unique only up to a set of measure zero.

2.4 Cut and Disintegration in Infinite Words↩︎

Fix a finite set of atomic propositions \(AP\). We work with the space \((2^{AP})^\omega\) of infinite words over \(2^{AP}\), where at each step every atomic proposition is either true or false.

Observe that there is a natural bijection \((2^{AP})^\omega \cong \prod_{a\in AP} 2^\omega,\). We will repeatedly use this correspondence. We also use the natural identification \(2^n \times 2^\omega \cong 2^\omega,\) given by concatenation.

In this subsection, we consider disintegration in the space of infinite words. To disintegrate, we need to represent \((2^{AP})^\omega\) as a product of two spaces. For that purpose, we introduce a notion of a cut.

Informally, a cut can be viewed as a generalized notion of a timestamp. It specifies which part of a trace is conditioned on. Intuitively, a cut separates a trace into a prefix, representing the past, and a suffix, representing the future; disintegration then yields a distribution over future behavior conditioned on the past.

Formally, a cut is a function \(C \colon AP \to \mathbb{N}_\omega.\) Given a cut \(C\), we define the sets \(L(C)\) and \(U(C)\) by \[L(C) = \prod_{a \in AP} 2^{C(a)}, \qquad U(C) = \prod_{a \in AP; \;C(a) \neq \omega} 2^{\omega }.\]

Intuitively, the value \(C(a)\) specifies how much of the history of the proposition \(a\) is revealed. The factor \(2^{C(a)}\) represents the portion of the trace over \(a\) that is conditioned on, while the corresponding factor \(2^\omega\) in \(U(C)\) represents the remaining unconstrained suffix. If \(C(a)=\omega\), then the entire history of \(a\) is fixed, and therefore no suffix component for \(a\) appears in \(U(C)\).

Hence, we can view a measure \(\mu \in \mathcal{P}((2^{AP})^\omega)\) as a probability measure on \(L(C) \times U(C)\). For each \(T' \in L(C)\), we may then consider a disintegration measure \(\mu_{T'}\) as given by 1.

2.5 Constructive disintegration↩︎

In this subsection, we give a constructive interpretation of the abstract notion of disintegration on the space of infinite words. This result allows us to compute disintegration measures in certain cases and is later used to develop model-checking algorithms.

We first observe that disintegration with respect to a finite prefix coincides with ordinary conditional probability. Since the set of prefixes of a fixed finite length is finite, conditioning on a specific prefix amounts to conditioning on an event of positive probability. In this case, the disintegration measure is given by the classical formula \[\mathbb{P}(X \mid Y) = \frac{\mathbb{P}(X \cap Y)}{\mathbb{P}(Y)},\] whenever \(\mathbb{P}(Y) > 0\).

Next, we show that disintegration with respect to a cut that assigns the value \(\omega\) can be obtained as the limit of disintegrations with respect to its finite prefixes.

2.6 Modeling the system↩︎

We consider labeled Markov Decision Processes.

A Markov chain is an MDP \(M = (S, A, AP, l, R, i)\) whose action set is a singleton, i.e.\(A = \{\ast\}\). Since the single action is irrelevant, we write a Markov chain as \((S, AP, l, P, i)\), omitting \(A\), where \(P(s,s') := R(s,\ast)(s')\).

Given a Markov chain \(M = (S, AP, l, P, i)\), we call the sequence of states \(\pi \in S^*\cup S^\omega\) a path and its corresponding labeling trace \(l(\pi)\in {(2^{AP})}^*\cup (2^{AP})^\omega\) is given by \(l(\pi)(i) = l(\pi(i))\), for every \(i<|\pi|\). \(M\) induces a probability measure \(\nu \in \mathcal{P}(S^\omega)\) on the set of infinite paths. For \(n\in \mathbb{N}\) and a finite path \(p\in S^n\), the measure of the corresponding cylinder set is given by \[\nu(\pi \in S^\omega \mid \pi[n] = p) = i(p(0) ) \;\prod_{i=0}^{n-2} P(p(i),p(i+1)).\]

Moreover, \(M\) induces a probability measure \(\mu \in \mathcal{P} ((2^{AP})^\omega)\) on the set of infinite traces. For \(n\in \mathbb{N}\) and a finite trace \(t\in (2^{AP})^n\), the measure of the cylinder set is given by \[\mu(T\in (2^{AP})^\omega \mid T[n] = t) = \nu(\pi \in S^\omega \mid l(\pi[n]) =t) =\] \[= \sum_{p\in S^n;l(p) = t} i(p(0)) \;\prod_{i=0}^{n-2} P(p(i),p(i+1)).\]

We call a Markov chain \(M= (S, AP,l, R, i)\) precisely labeled, if for every \(s_1,s_2\in S\), if \(l(s_1) = l(s_2)\), then \(s_1 = s_2\), i.e., labeling function \(l: S \to 2^{AP}\) is injective.

Throughout the paper, we use a construction in which one component, \(M_1\), “blindly” schedules another component, \(M_2\). Intuitively, \(M_1\) probabilistically generates a blind scheduler for \(M_2\). By blind we mean that the scheduler does not depend on the states or transitions of \(M_2\), but only on the step index. The probability of generating a particular scheduler is determined solely by \(M_1\) and is independent of the behavior of \(M_2\). This construction allows us to reason about the behavior of \(M_2\) conditioned on the scheduling trace produced by \(M_1\). We formalize this intuition using the notion of a cascade product \(M_1 \otimes M_2\).

2.7 Automata↩︎

The algorithm in 6 uses several types of automata on infinite words.

We call an ABA existential (universal) if every formula \(\delta(q,\sigma)\) and the initial formula \(q_0\) use only disjunctions ( conjunctions). In this case we may write \(\delta(q,\sigma)=Q'\) or \(q_0=Q'\) for some \(Q'\subseteq Q\), meaning \(\bigvee_{q'\in Q'} q'\) ( \(\bigwedge_{q'\in Q'} q'\)).

A reachability (safety) alternating automaton is defined as ABA above, except that a run is accepting if every infinite branch that visits \(F\) at least once (if every infinite branch stays in \(F\) forever).

3 DTL↩︎

3.1 Syntax↩︎

Let \(AP\) be a finite set of atomic propositions. The formulas of Disintegration Temporal Logic are given by the following grammar, where \(\phi\) denotes state formulas and \(\psi\) denotes quantitative formulas: \[\begin{align} \phi &\mathrel{\vcenter{:}}= a \mid \neg \phi \mid \phi \land \phi \mid \psi \leq r \mid \LTLnext \phi \mid \phi \LTLuntil \phi, \\ \psi &\mathrel{\vcenter{:}}= r \cdot \psi \mid \psi + \psi \mid \mathbb{P}(\phi \mid [A], B). \end{align}\] Here \(a\in AP\) and \(A,B\subseteq AP\), and \(r\in \mathbb{R}\).

We use additional temporal operators \(\LTLglobally \phi = \neg \LTLeventually \neg \phi\); \(\LTLeventually \phi= true \LTLuntil \phi;\) \(\phi_1 \LTLr \phi_2 = \neg(\neg \phi_1 \LTLuntil \neg \phi_2)\). Moreover, \(\mathbb{P}(\phi) = \mathbb{P}(\phi \mid [\emptyset], \emptyset)\).

The scope of an occurrence of a probabilistic operator \(\mathbb{P}(\phi \mid [A], B)\) is the subformula \(\phi\). All occurrences of atomic propositions or temporal operators in the scope of a probabilistic operator are said to be bound. Note that the occurrences of atomic propositions from \(A \cup B\) in the conditional part \([A], B\) are not bound by this operator.

A formula \(\phi\) is called closed if every occurrence of an atomic proposition or a temporal operator is bound by some probabilistic operator.

3.2 Semantics↩︎

3.2.1 Informal explanation.↩︎

The main feature of the logic is the conditional probability operator. A formula is evaluated relative to a trace \(T\), a timestamp \(n\), a cut \(C\), and a probability measure \(\mu\).

The timestamp represents the current position in the trace; temporal operators update the timestamp. The cut specifies which part of the trace is conditioned on, namely the prefix component \(L(C)\).

The formula \(\mathbb{P}(\phi \mid [A], B)\) updates the cut from \(C\) to \(C'\) by assigning elements of \(A\) the current timestamp \(n\) and elements of \(B\) the value \(\omega\). Intuitively, this corresponds to conditioning on the behavior of atomic propositions in \(A\) up to the current step and on the entire behavior of atomic propositions in \(B\). The operator \(\mathbb{P}(\phi \mid [A], B)\) is interpreted quantitatively and denotes the probability of satisfying \(\phi\), conditioning on \(T_{L(C')}\).

3.2.2 Semantics↩︎

We now define the semantics formally. For every cut \(C\), we fix a disintegration kernel of \(\mu\) with respect to \(L(C)\). Later, we show that the semantics do not depend on the particular choice of this kernel.

Given a trace \(T \in (2^{AP})^\omega\), a timestamp \(n \in \mathbb{N}\), a cut \(C \colon AP \to \mathbb{N}_\omega\), and a measure \(\mu \in \mathcal{P}((2^{AP})^\omega)\), the satisfaction relation \(T,C,n \vDash_\mu \phi\) is defined inductively as follows: \[\begin{align} T,C,n &\vDash_\mu a\text{ iff } a\in T(n), \\ T,C,n &\vDash_\mu \neg \phi \text{ iff } T,C,n \not\vDash_\mu\phi, \\ T,C,n &\vDash_\mu \phi_1 \wedge \phi_2 \text{ iff } T,C,n \vDash_\mu\phi_1 \text{ and } T,C,n \vDash_\mu\phi_2, \\ T,C,n &\vDash_\mu \psi \leq r\text{ iff } \llbracket T,C,n,\psi \rrbracket_\mu \leq r, \\ T,C,n &\vDash_\mu \LTLnext \phi \text{ iff } T,C,n+1 \vDash_\mu \phi, \\ T,C,n &\vDash_\mu \phi_1 \LTLuntil \phi_2 \text{ iff } \exists i. \;T,C,n+i \vDash_\mu\phi_2 \text{ and } \forall j<i. \;T,C,n+j \vDash_\mu\phi_1. \end{align}\]

The formula \(\psi\) is interpreted quantitatively over a trace \(T\), a timestamp \(n\in \mathbb{N}\), a cut \(C\) and a measure \(\mu\), with its semantics taking values in \(\mathbb{R}\). \[\begin{align} \llbracket T,C,n, r\cdot \psi \rrbracket_\mu &= r \cdot \llbracket T,C,n,\psi \rrbracket_\mu, \\ \llbracket T,C,n, \psi_1 + \psi_2 \rrbracket_\mu &= \llbracket T,C,n, \psi_1 \rrbracket_\mu + \llbracket T,C,n, \psi_2 \rrbracket_\mu, \\ \llbracket T,C,n, \mathbb{P}(\phi \mid [A],B) \rrbracket_\mu &= \mu_{T_{L(C')}} ( t\in U(C') \mid (T_{L(C')},t),C',n \vDash_\mu\phi ). \end{align}\] In the last line, the cut \(C':AP\to \mathbb{N}_\omega\) is defined for \(p\in AP\) by \[C'(p) = \begin{cases} C(p), &\text{ for }p\notin A\cup B,\\ max(C(p),n), & \;\text{for } p\in A,\\ \omega, &\text{ for } p\in B. \end{cases} \label{eq95s39}\tag{4}\]

Here, \(T_{L(C')}\) denotes the projection of \(T \in (2^{AP})^\omega \cong L(C') \times U(C')\) onto \(L(C')\), and \(\mu_{T_{L(C')}}\) is the corresponding disintegration measure obtained from the fixed disintegration kernel.

Given a Markov chain \(M\) inducing a measure \(\mu\) and a closed DTL formula \(\phi\), we define \[M \vDash\phi \quad\text{iff}\quad T, C_0, 0 \vDash_\mu \phi,\] where \(C_0(p) = 0\) for all \(p \in AP\) and \(T\) is an arbitrary trace. Since \(\phi\) is closed, the evaluation does not depend on the choice of \(T\).

The DTL model-checking problem is to decide, given a Markov chain \(M\) and a closed DTL formula \(\phi\), whether \(M \vDash\phi\) holds.

3.2.3 Correctness and Undecidability↩︎

Recall that disintegration kernels are defined uniquely up to a.e. equivalence. The following theorem formalizes the correctness of the semantics and shows that the semantic evaluation is independent of the particular choice of disintegration kernels.

4 Expressing properties in DTL↩︎

4.1 Security properties and independence↩︎

We show how DTL can express well-known security properties formulated in terms of independence and conditional independence between different components of an execution trace. Typically, such properties require that conditioning on different high-level behaviors does not change the induced distribution over low-level behaviors.

These properties fall within the linear fragment of DTL, introduced in 5, for which we provide a polynomial-time model-checking algorithm.

4.1.1 Probabilistic Non-interference↩︎

To define probabilistic non-interference, originally formulated by Gray [15], [16], consider a probabilistic system that communicates with agents through high- and low-level channels. Informally, the property requires that the low-level trace does not give any information on the distribution of the high-level trace, or equivalently, there is no probabilistic information leakage from high-level data to low-level data. As defined in [15], probabilistic non-interference can be phrased as a conditional-independence requirement. For every \(n \in \mathbb{N}\), for any high-level input trace \(H\) of length \(n\), any low-level input and output traces \(L\) and \(O\) of length \(n\), and any low-level output event \(o\) at step \(n{+}1\), whenever the joint event \((H, L, O)\) has positive probability, the probability of observing \(o\) at step \(n{+}1\) conditioned on \((H, L, O)\) equals the probability conditioned on \((L, O)\).

We demonstrate how to express this property in DTL. Let \(M\) be a Markov chain that models our probabilistic system, and let the set of atomic propositions be \(AP = \{h, l, o\}\), where \(h\) and \(l\) represent the high- and low-level inputs and \(o\) the low-level output.

We say that \(M\) satisfies probabilistic non-interference if \[M \vDash\mathbb{P}\!\Bigl( \LTLglobally \bigl( \mathbb{P}(\LTLnext o \mid [h,l,o]) = \mathbb{P}(\LTLnext o \mid [l,o]) \bigr) \Bigr) = 1.\]

The informal quantification “for all input traces of length \(n\)” is captured by the outermost quantification with probability \(1\) and the globally operator \(\LTLglobally\). The innermost equality between probabilistic operators requires that \(\LTLnext o\) is independent from the history of \(h\), conditioning on the history of \(l\) and \(o\).

Relation to other version of probabilistic non-interference.

In the literature [1], [4], [17], another version of probabilistic non-interference is used. It requires that the distribution of the low-observable trace is the same for every pair of low-level equivalent initial states. This version is a weakening of the original probabilistic non-interference property: whereas the original requires independence from the high-level history at every step of the execution, this version only requires independence from the high-level information of the initial state, leaving open the possibility that high-level information leaks through the transition dynamics. For finite state systems, model checking of this weaker version can be reduced to a finite number of labeled Markov chain equivalence checks (or probabilistic bisimulation conditions).

In systems with ongoing interaction, the difference is significant. A system may conceal the high-level initial state and thus satisfy the weaker property, while still allowing future low-level observations to depend on the evolving high-level state. In such a system, information about high-level behavior may be leaked dynamically during execution even though the distribution of complete low-level traces is independent of the initial secret. The conditional-independence formulation rules out precisely this form of information flow. In that sense, the original notion of probabilistic non-interference is similar to the possibilistic trace-based version [3], [18], [19].

4.1.2 Perfect Indistinguishability↩︎

Perfect indistinguishability [19]–[21], also known as perfect secrecy, is commonly formulated as an indistinguishability requirement for ciphertext distributions, which in the perfect case reduces to (a form of) independence.

A probabilistic encryption system consists of two components: a key-generation procedure and an encryption procedure that, given a message and a key, produces a ciphertext (which can later be decrypted using the key). For simplicity, we model messages as finite traces over \(2^{\{m\}}\) and ciphertexts as finite traces over \(2^{\{c\}}\). We assume that \(MD\) receives a message trace and produces a ciphertext trace, with key generation happening internally.

\(MD\) satisfies perfect indistinguishability if for any two messages \(T_1,T_2\) and any ciphertext trace \(D\), the probability of outputting \(D\) on input \(T_1\) equals the probability of outputting \(D\) on input \(T_2\).

As above, we model universal quantification over messages by composing \(MD\) with a Markov chain \(M_{\mathit{msg}}\) that generates message letters uniformly. Let \(M := M_{\mathit{msg}} \otimes MD.\)

To express perfect indistinguishability in DTL, we need to require that the message and ciphertext projections are independent. We can do it as follows: \[M \vDash\mathbb{P}\Bigl( \LTLglobally \bigl( \mathbb{P}( \LTLnext ( \mathbb{P}( c \mid [m] ) = \mathbb{P}(c) ) \mid [c] )=1 \bigr) \Bigr) =1 \wedge\] \[\wedge \mathbb{P}\Bigl( \LTLglobally \bigl( \mathbb{P}( \LTLnext ( \mathbb{P}( m \mid [c] ) = \mathbb{P}(m) ) \mid [m] )=1 \bigr) \Bigr) =1.\]

Let us demonstrate that the conjunction above is equivalent to the independence of the projections of an execution trace onto \((2^{\{m\}})^\omega\) and \((2^{\{c\}})^\omega\). Let \(\mu\) be the probability measure induced by \(M\). Assume the projections are not independent. Then by Lemma 4.6 in [9] there exist \(n,k \in \mathbb{N}\) and finite traces \(T_m \in (2^{\{m\}})^n\) and \(T_c \in (2^{\{c\}})^k\) such that \[\mu((T_m (2^{\{ m\} })^\omega) \times (2^{\{ c\} })^\omega) \cdot \mu((2^{\{ m\} })^\omega \times (T_c(2^{\{ c\} })^\omega)) \neq\] \[\neq \mu( (T_m (2^{\{ m\} })^\omega) \times (T_c (2^{\{ c\} })^\omega) ).\] Without loss of generality, assume \(n\le k\), and assume that for the shorter prefix of \(T_c\), it does not hold; otherwise, we can shorten it. In that case, there is at least one \(T_{m}' \in (2^{ \{ m\} })^k\), such that \(T_m' [n] = T_m\), and \[\mu((2^{\{ m\} })^\omega \times (T_c(2^{\{ c\} })^\omega) \mid (2^{\{ m\} })^\omega \times (T_c[k-1](2^{\{ c\} })^\omega)) \neq\] \[\neq \mu((2^{\{ m\} })^\omega \times (T_c(2^{\{ c\} })^\omega) \mid ((T_m' (2^{\{ m\} })^\omega) \times (T_c[k-1](2^{\{ c\} })^\omega)),\] which fails the first conjunct. If \(n\ge k\), the second conjunct fails.

4.2 Stochastic environment↩︎

Many stochastic systems consist of several interacting components, one of which models an external stochastic environment. Temporal specifications concern infinite executions, and each complete environment execution (i.e., an infinite trace) naturally induces a conditional probability distribution over the executions of the remaining system. DTL captures these conditional distributions through conditioning on infinite traces, allowing one to express not only the overall probability of satisfying a temporal specification, but also how this probability varies across different environment executions.

This setting naturally occurs in a variety of applications.

Communication networks. A communication network interacting with a stochastic environment modeling the quality of the communication channel and the resulting burst errors [22]–[24]. The Gilbert–Elliott model is widely used to capture burst errors by representing the channel quality as a two-state Markov chain.

Hardware systems. A hardware component interacting with an external stochastic environment modeling radiation-induced transient faults (soft errors), which occur probabilistically [25], [26].

Embedded systems. The physical environment of an embedded system can be modeled by a finite-state Markov chain, as in Markov jump linear systems, where the Markov chain represents environmental changes [27].

Let the environment be modeled by a Markov chain \(M_{env}\) over the set of atomic propositions \(AP_{env}\). Let the system be modeled by an MDP \(MD\) whose actions are from \(2^{AP_{env}}\). Their cascade product \(M:= M_{env}\otimes MD\) models the joint behavior of the environment and the system. Let \(\mu\) denote the probability measure on infinite traces induced by \(M\).

Let the temporal formula \(\phi_{bad}\) specify an undesirable system behavior. DTL can express properties such as With probability at least \(0.1\), the environment produces an execution such that, conditioned on this execution, the probability that the system exhibits the undesirable behavior is greater than \(0.4\). This is expressed by the formula \[M\vDash\mathbb{P}\Bigl( \mathbb{P}\bigl( \phi_{bad} \mid AP_{env}\bigr) > 0.4 \Bigr) > 0.1.\]

In other words, although the system may perform reliably under most environment executions, there exists a substantial subset of environment executions under which its reliability is significantly lower. Such concentration of failures cannot be detected by considering only the overall probability of undesirable behavior. For example, the mean (overall) probability of undesirable behavior over all environment executions may be as low as 0.05, even though there exists a non-negligible subset of environment executions for which the conditional probability of failure exceeds 0.4. Consequently, two systems with the same overall probability of failure may exhibit fundamentally different behavior: one may exhibit a relatively uniform probability of failure across all environment executions, whereas the other may exhibit a high probability of failure concentrated on a significant subset of environment executions. Classical probabilistic temporal logics reason only about the overall probability of satisfying a temporal specification and therefore cannot distinguish between these situations. In contrast, by conditioning on complete environment executions (i.e., infinite traces), DTL enables reasoning not only about the overall probability of satisfying a temporal specification, but also about how this probability depends on environment execution, revealing whether failures are uniformly distributed or concentrated on particular classes of environment executions. In particular, replacing the threshold \(0.4\) by \(0\) or \(1\) yields a property in the qualitative fragment of DTL, for which we present a model-checking algorithm in 6.

4.3 Distribution transformers and probabilistic automata↩︎

We briefly discuss two verification frameworks for probabilistic systems whose specifications can be naturally expressed in DTL. The common theme is that, rather than quantifying existentially over schedulers, one can reason about a distribution over schedulers and ask for the probability mass of schedulers satisfying a given specification. This modification changes the original problem and yields a "more probabilistic" counterpart. For safety and reachability objectives, the two formulations coincide. For more general \(\omega\)-regular objectives, however, they may differ, and the new one may even become decidable in cases where the classical existential formulation is undecidable. Properties that compare probabilities only with 0 and 1 belong to the qualitative fragment of DTL, which we introduce in 6 and show to be decidable.

4.3.1 MDP as distribution transformers↩︎

Fix an MDP \(MD\) and a blind scheduler, i.e.an infinite sequence of actions. Under such a scheduler, the execution of \(MD\) induces a sequence of distributions over states. Properties that refer to this sequence are often called distributional properties. This view received significant attention over the last decade [28]–[30], with applications in a number of areas, e.g., multi-agent systems [31].

Distributional properties require some linear (specified by linear inequalities) labeling, i.e., functions \(\mathcal{P}(S) \to 2^\Sigma\), for the set of states of the MDP \(S\) and the set of labels \(\Sigma\). Distributional Model Checking Problem asks, given an MDP \(MD\), a regular set of blind schedulers \(\mathcal{A}\), a labeling function \(\lambda\), and a Büchi automaton \(\mathcal{B}\) over \(2^\Sigma\), whether there is a scheduler in \(\mathcal{A}\), such that it produces the sequence of labels under \(\lambda\) which is in \(\mathcal{L}(\mathcal{B})\).

Distributional properties can be modeled with DTL, replacing the existential quantification "there is a scheduler" by the probabilistic requirement "there is a set of schedulers of positive measure".

Formally, instead of a regular set of schedulers \(\mathcal{A}\), assume a probability distribution over blind schedulers given by a Markov chain \(M_{\mathit{sched}}\), and consider the cascade product \(M := M_{\mathit{sched}} \otimes MD\). Let \(AP_{\mathit{sched}}\) denote the atomic propositions encoding scheduler choices in \(M_{\mathit{sched}}\). Assume that \(M\) is precisely labeled. For a state \(s\) of \(MD\), let \(\phi_s\) be a (state) formula describing that the \(MD\)-coordinate of \(M\) on this state is \(s\). Then the conditional probability of being in state \(s\) given the scheduler trace is expressible as \(\mathbb{P}(\phi_s \mid [AP_{\mathit{sched}}])\). Since the logic admits linear combinations of such probabilities, we can encode any linear labeling \(\lambda\), and we can express the LTL property corresponding to \(\mathcal{L}(\mathcal{B})\) (when \(\mathcal{L}(\mathcal{B})\) is LTL-expressible). Let \(\phi\) denote the resulting formula.

We can then require that the set of schedulers satisfying \(\phi\) has positive measure. We define the property \[M \vDash\mathbb{P}( \phi) > 0\bigr.\] If \(\mathcal{L}(\mathcal{B})\) is a reachability property, this essentially coincides with pure existential quantification. In general, however, it is stronger, since it requires a set of schedulers of positive probability mass rather than a single scheduler.

4.3.2 Probabilistic Automata over Infinite Words↩︎

Probabilistic automata over infinite words [32], [33] can be viewed as an MDP in the sense of our modeling framework, together with a Büchi, Streett, or Rabin acceptance condition over \(2^{AP}\). A central question studied in this setting is whether there exists a blind scheduler such that the probability of producing an infinite trace satisfying a given acceptance condition meets a prescribed linear requirement. Typically, this is phrased by comparing the acceptance probability against thresholds such as \(1\), \(0\), or an arbitrary \(\epsilon \in [0,1]\). It is known that certain variants, in particular, even those involving comparison against \(0\) or \(1\), lead to undecidability [32].

We can model this setting by assuming a Markov chain \(M_{\mathit{aut}}\) with a set of atomic propositions \(AP_\mathit{aut}\) such that the action set of \(MD\) is \(2^{AP_\mathit{aut}}\). Let \(M := M_{\mathit{aut}} \otimes MD\) be the corresponding cascade product. Any acceptance condition over \(2^{AP}\) can be modeled by a DTL formula \(\phi_{\mathit{acc}}\) without occurrences of probabilistic operators.

Then, for any comparison operator \(\star \in \{\le,\ge,=\}\) and any \(\epsilon \in [0,1]\), we can express that the set of schedulers satisfying the comparison has positive probability mass as \[M\vDash\mathbb{P}\Bigl( \mathbb{P}\bigl( \phi_{acc} \mid AP_{aut}\bigr) \mathrel{\star} \epsilon \Bigr) > 0.\] Note that this property differs from the original one, since it requires the existence of a set of schedulers (of positive measure), rather than a single scheduler. Moreover, as we demonstrate in the next section, this property is decidable for \(\epsilon \in \{ 0,1\}\), unlike the original one.

4.4 Related logics↩︎

The most widely used probabilistic temporal logic, PCTL\(^*\) [5], combines probabilistic and temporal operators in a branching-time setting.

In the case of a precisely labeled system (when the labeling is injective), DTL subsumes PCTL\(^*\). Let \(J = [j_1,j_2]\) be an interval. In a precisely labeled system, the PCTL\(^*\) probabilistic operator \(\mathbb{P}_{J}(\phi)\) can be expressed in DTL by \[j_1 \le \mathbb{P}(\phi \mid [AP]) \le j_2,\] where conditioning on \([AP]\) corresponds to probability conditioning on the trace up to the current timestamp.

An approach orthogonal to ours to incorporating conditional probabilities into temporal logics is studied in [34], [35]. The authors consider conditional probabilities of the form \(\mathbb{P}(\psi \mid \phi)\), where both \(\psi\) and \(\phi\) are \(\omega\)-regular events, typically relying on the property \(\mathbb{P}(\psi \mid \phi) = \frac{\mathbb{P}(\psi \wedge \phi)}{\mathbb{P}(\phi)}\).

As discussed in Section 1.1 of [34], [35], this formalism is also used to express certain security properties involving independence. However, it can only express independence between specific \(\omega\)-regular outcomes (such as \(\LTLglobally l\) and \(\LTLfinally h\)), and does not allow expressing independence from an arbitrary history, as required for probabilistic non-interference and perfect indistinguishability.

The PHL logic for probabilistic hyperproperties combines probabilistic operators with explicit quantification over schedulers [36]. To mitigate undecidability, the corresponding model-checking procedure treats families of schedulers jointly.

Another logic for probabilistic hyperproperties, HyperPCTL [4], combines probabilistic reasoning with quantification over states. This allows, for example, expressing a restricted variant of probabilistic non-interference, stating that the distribution of observable outputs is independent of the initial secret state. The difference from the version of probabilistic non-interference considered in our paper is discussed in [nonintereference].

The extension of HyperPCTL called HyperPCTL\(^*\) [37] allows nesting of probabilistic measurements over paths of the system (sequences of system states) and measurements over tuples of paths. The key difference is that DTL conditions on observable traces (or projections of traces onto selected atomic propositions), whereas HyperPCTL\(^*\) reasons about concrete execution paths. Conditioning on traces naturally captures partial observations of an execution and therefore enables the specification of information-flow properties. For example, the version of probabilistic non-interference considered in [37] coincides with that of HyperPCTL [4] and requires only independence from the initial secret state.

Logics for possibilistic hyperproperties such as HyperLTL and HyperCTL\(^*\) [3] allow nesting and alternation of universal and existential path quantifiers, with temporal operators. Our qualitative fragment can be viewed as a probabilistic counterpart of HyperCTL\(^*\), where strict quantifiers are replaced by their "softer" probabilistic counterparts.

There are several program logics for probabilistic conditioning and independence, such as Lilac [38], Bluebell [39], and Probabilistic Separation Logic [40], as well as probabilistic relational program logics for security properties [41], [42]. The proof system presented in [43] enables reasoning about possibilistic hyperproperties expressed in HyperLTL.

5 Linear Fragment↩︎

The linear fragment of \(DTL\) is given by the following grammar: \[\begin{align} \kappa &\Coloneqq a \mid \kappa \wedge \kappa \mid \neg \kappa \mid \kappa \LTLuntil \kappa \mid \LTLnext \kappa, \\ \theta &\Coloneqq \mathbb{P}(\kappa \mid [A_1]) = \mathbb{P}(\kappa \mid [A_2]) \mid \LTLglobally\,\theta \mid \LTLnext \theta \mid \mathbb{P}(\theta \mid [B])=1,\\ \chi &\Coloneqq \mathbb{P}(\theta) = 1 \mid \chi\wedge\chi \mid \neg\chi. \end{align}\] Here \(A_1,A_2,B\subseteq AP\).

The linear fragment of DTL can express independence of the suffix from some part of the prefix, including properties like probabilistic non-interference and perfect indistinguishability.

In this chapter, we show that model-checking for the linear fragment is in \(\mathrm{PTIME}\), using an algorithm inspired by [11]. But first, we define an auxiliary construction.

5.1 Multidynamic Automata↩︎

We define a new type of automata that we use in this section. Intuitively, we use it to prove the generalized notion of equivalence of labeled Markov chains and prove the equivalence of two different dynamics on a graph with respect to some quadratic form.

Given a matrix \(W\in \mathbb{R}^{n\times n}\), and a multidynamic automaton \(D = (n,Q,Q_{in}, Q_{fin},\delta,z)\), we say that \(D\) globally satisfies the quadratic form \(W\), if for any path \(p\in Q^k\) with \(p(k-1)\in Q_{fin}\), the equality \(val(p)_1^T W val(p)_2 = 0\) holds.

5.2 Algorithm↩︎

6 Qualitative Fragment↩︎

The qualitative fragment restricts the nesting of probabilistic operators such that every operator except the outermost may compare probabilities only to \(0\) or \(1\).

We define the qualitative fragment of DTL by the following grammar. \[\begin{align} \alpha & \Coloneqq \psi \leq r \mid \alpha \wedge \alpha \mid \neg \alpha, \\ \psi& \Coloneqq \mathbb{P}(\gamma) \mid \psi + \psi \mid r\cdot \psi, \\ \gamma&\Coloneqq a \mid \neg a \mid \gamma \land \gamma \mid \gamma \vee \gamma \mid \LTLnext \gamma \mid \gamma \LTLuntil \gamma \mid \gamma \LTLr \gamma \mid \mathbb{P}(\gamma \mid [A], B ) =1 \mid \mathbb{P}(\gamma \mid [A], B ) >0 . \end{align}\]

The qualitative fragment captures some of the properties discussed in section [environment,dist_and_prob_aut]. In particular, it can express stochastic environment properties in which inner conditional probabilities are compared only to 0 or 1, distributional properties in which the labeling function checks only whether entries of the distribution vector are 0 or 1, as well as properties of probabilistic automata in which the acceptance probability is required to be 0 or 1. As mentioned earlier, the latter is undecidable in the original setting with strict existential quantification over schedulers; we show below that it becomes decidable when moving to our soft (probabilistic) quantification.

We call \(\mathbb{P}(\dots) = 1\) and \(\mathbb{P}(\dots) > 0\) universal and existential probabilistic operators, respectively.

For \(n,m,c\in \mathbb{N}\) define \(g_c(n+1,m) = c^{g_c(n,m)}\), and \(g_c(0,m) = m\). We define \(NSPACE(g(n,m))\) to be the class of languages that are accepted by a nondeterministic Turing machine that runs in space \(O(g_c(n,m))\) for some \(c>1\).

Below, we present the main result of this section. It relies on the notion of cascade compatibility, which generalizes properties of models constructed as cascade products of multiple components. A formal definition of this notion is given later in this section.

We prove this Theorem by presenting an algorithm that, for every subformula \(\gamma\), constructs an alternating Büchi automaton \(B_\gamma\) that models the semantic evaluation of \(\gamma\) on an input trace, cut, and timestamp, each encoded by infinite traces. This construction is inspired by the construction from the HyperCTL\(^*\) algorithm [46], combined with a reasoning about strongly connected components for the verification with respect to qualitative probabilistic formulas [5].

The automata construction is built recursively on the structure of formula \(\gamma\), and uses the Miyano-Hyashi construction for every alternation between universal, existential quantifiers, or the temporal operators \(\LTLu\) and \(\LTLr\).

6.1 Cascade property↩︎

We now generalize the property satisfied by the cascade product \(M_1 \otimes M_2\), which will be used to derive a corollary of 2.

Intuitively, the cascade property expresses a conditional independence assumption. Fix a prefix length \(n\) and a prefix \(T' \in (2^{AP})^n\). The property states that, once the projection of \(T'\) onto \(AP'\) is fixed, the future behavior of the atomic propositions in \(AP'\) is independent of the remaining part of the prefix over \(\overline{AP'}\).

Equivalently, conditioning on the full prefix \(T'\) yields the same distribution over future \(AP'\)-traces as conditioning only on the projected prefix \(T'_{AP'}\).

Given a cut \(C \colon AP \to \mathbb{N}_\omega\) and a number \(n \in \mathbb{N}\), we say that a property \(B \subseteq U(C)\) depends on the first \(n\) steps if for all traces \(T^1, T^2 \in (2^{AP})^\omega\), \[T^1[n] = T^2[n] \quad\Rightarrow\quad T^1_{U(C)} \in B \;\text{iff}\; T^2_{U(C)} \in B.\]

The next result is a corollary of 2, which uses the cascade property to prove that, in certain cases, the limit is reached in finitely many steps.

We say that a subformula is in the scope of a total condition on \(b\) if it occurs within a probabilistic operator of the form \(\mathbb{P}(\psi \mid [A], B)\) with \(b \in B\).

Since the cascade property is a conditional-independence requirement, it can be expressed in a linear fragment of DTL similarly to probabilistic non-interference. Let \(M\) be a Markov chain over \(AP\) and let \(AP' \subseteq AP\). Then \(M\) satisfies the cascade property with respect to \(AP'\) iff, for every formula \(x \in 2^{AP'}\), we have \[M \vDash\mathbb{P}\Bigl( \LTLglobally \bigl( \mathbb{P}(\LTLnext x \mid [AP]) = \mathbb{P}(\LTLnext x \mid [AP']) \bigr) \Bigr) = 1.\] Thus, the cascade property can be checked in polynomial time. It follows that the cascade compatibility of a given Markov chain and formula can also be checked in polynomial time.

Hence, 6 applies directly to systems constructed as cascade products. Moreover, it extends to the more general class of systems that are cascade-compatible with a given formula, and this property can be checked in polynomial time by 5.

6.2 Automata construction↩︎

Let \(M= (S, AP,l, P, i)\) be a precisely labeled Markov chain, and \(\gamma\) be a qualitative DTL formula defined by the grammar above. We define an alternating Büchi automaton \(B_{\gamma, M }\) recursively on the structure of \(\gamma\).

The automaton is over the alphabet \(\Sigma = 2^{AP} \times \{ 0,\bot,\top\}^{AP} \times \{ 0,\bot\}\). Intuitively, we interpret an infinite trace over \(\{ 0,\bot, \top\}\) as an element of \(\mathbb{N}_\omega\). For \(n\in \mathbb{N}\), a trace that starts with \(0^{n}\bot\) represents \(n\) and a trace that starts \(0^n \top\) represents \(\omega\). In the same way, an infinite trace over \(\{0,\bot\}\) encodes an element of \(\mathbb{N}\).

This way, an infinite trace over \(\{ 0,\bot,\top\}^{AP}\) represents a cut, and an infinite trace over \(\{ 0,\bot\}\) represents a timestamp. Intuitively, \(B_{\gamma, M}\) models the evaluation of \(\gamma\) for a given trace, a cut, and a timestamp.

Everywhere in this construction \(\sigma\in \Sigma\), \(t\in 2^{AP}\), \(\vec{v}\in \{ 0,\bot,\top \}^{AP}\), and \(b\in \{ 0,\bot \}\).

For \(a\in AP\), define \(B_{a,M} = (\{ q_0,q_{acc},q_{rej} \}, \Sigma, \delta_{a,M},q_0,q_{acc})\), where \[\delta_{a,M}(q_{rej}, \sigma ) = q_{rej}, \;\;\;\;\;\delta_{a,M}(q_{acc},\sigma ) = q_{acc},\] \[\delta_{a,M}(q_0, (t,\vec{v}, 0)) = q_0,\] \[\delta_{a,M}(q_0, (t,\vec{v},\bot)) = \begin{cases} q_{acc}, \;\;\;\text{if } a\in t, \\ q_{rej}. \;\;\;\text{else.} \end{cases}\]

The automaton \(B_{\neg a, M}\) is defined in the same way, with the only difference that \[\delta_{\neg a,M}(q_0, (t,\vec{v},\bot)) = \begin{cases} q_{acc}, \;\;\;\text{if } a\notin t, \\ q_{rej}, \;\;\;\text{else.} \end{cases}\]

The automata \(B_{\gamma_1\wedge \gamma_2,M}\) and \(B_{\gamma_1\vee \gamma_2,M}\) are constructed as an intersection and union of \(B_{\gamma_1,M}\) and \(B_{\gamma_2,M}\).

The automaton \(B_{\LTLnext \gamma, M}\) is defined using the automaton \(B_{\gamma,M} = (Q,\Sigma, \delta_\gamma, {q_0}_\gamma, F)\) as \(B_{\LTLnext \gamma, M} = (Q\times \{ q_0,q_\bot\}, \Sigma, \delta, {q_0}_\gamma \times \{q_0\}, F\times \{q_0, q_\bot\})\), where for \(q\in Q\), \(i\in \{ 0,\bot\}\), \[\delta((q,q_i), (t,\vec{v},b)) = \delta_\gamma(q,(t,\vec{v},i)) \times \{ q_b \} .\]

The automaton \(B_{\gamma_1 \LTLuntil \gamma_2,M}\) is defined using the automata \(B_{\gamma_1,M} = (Q_1,\Sigma, \delta_1, {q_0}_1, F_1)\) and \(B_{\gamma_2,M} = (Q_2,\Sigma, \delta_2, {q_0}_2, F_2)\). We assume that \(B_{\gamma_1,M}\) and \(B_{\gamma_2,M}\) are existential. Otherwise, we turn them into existential using Miyano-Hayashi construction [47].

\(B_{\gamma_1 \LTLuntil \gamma_2,M} = ((2^{Q_1}\times Q_2\times \{ q_0,q_U\}) \sqcup Q_1\sqcup Q_2, \Sigma, \delta, \{{q_0}_1\} \times {q_0}_2 \times \{ q_0 \}, F_1 \sqcup F_2)\). Here, for \(Q_1'\subseteq Q_1\), \(q_1\in Q_1\) and \(q_2\in Q_2\) we define \[\delta((Q_1', q_2, q_0),(t,\vec{v},0)) =\bigvee_{q_2'\in \delta_2(q_2,(t,\vec{v},0))}(\bigcup_{q_1\in Q_1'} \delta_1(q_1,(t,\vec{v},0)), q_2', q_0),\] \[\delta((Q_1', q_2, q_0),(t,\vec{v},\bot)) =((\bigvee_{q_1\in Q_1' ; \;q_1'\in \delta_1(q_1,(t,\vec{v},\bot))} q_1')\wedge\] \[\wedge (\bigvee_{q_2'\in \delta_2(q_2,(t,\vec{v},0))} (\bigcup_{q_1\in Q_1'} \delta_1(q_1,(t,\vec{v},0)),q_2',q_U))) \vee (\bigvee_{q_2'\in \delta_2(q_2,(t,\vec{v},\bot))} q_2'),\] \[\delta((Q_1', q_2, q_U),(t,\vec{v},b)) = \delta((Q_1', q_2, q_0),(t,\vec{v},\bot)),\] \[\delta(q_1,(t,\vec{v}, b)) = \delta_1(q_1,(t,\vec{v}, b)),\] \[\delta(q_2,(t,\vec{v}, b)) = \delta_2(q_2,(t,\vec{v}, b)).\]

The automaton \(B_{\gamma_1 \LTLr\gamma_2, M}\) is defined as the complement of \(B_{(\neg \gamma_1) \LTLu (\neg \gamma_2),M}\), since \(\gamma_1 \LTLr\gamma_2=\neg((\neg \gamma_1) \LTLu (\neg \gamma_2))\).

We define automata \(B_{\mathbb{P}(\gamma \mid A,B) = 1,M}\) and \(B_{\mathbb{P}(\gamma \mid A,B) >0,M}\), using the automaton \(B_{\gamma, M}\). First, we convert \(B_{\gamma, M}\) into a deterministic Rabin automaton \(D_{\gamma,M}\). Next, intuitively, we take a product of \(M = (S, AP, l, P, i)\) and \(D_{\gamma, M} = (Q_{\gamma}, \Sigma, \delta_\gamma, {q_0}_\gamma, Acc_\gamma)\), interpreting a cut \(C\) and a timestamp \(n\) as an input. Formally, define an MDP \(MD = (S\times Q_\gamma, \{ 0,\bot, \top\}^{AP}\times \{0,\bot \}, AP,l_{MD} , R, i_{MD})\), where \(l_{MD}(s,q) = l(s)\), and \[R((s,q), (\vec{v},b), (s',q')) = \begin{cases} P(s,s'), \;\text{if } \delta_\gamma(q,(l(s),\vec{v},b)) = q', \\ 0, \;\text{otherwise}. \end{cases}\] \[i_{MD} (s,q) = \begin{cases} i(s), \text{ if } q={q_0}_\gamma,\\ 0, \text{ otherwise.} \end{cases}\]

We call a set \(O\) of states of \(MD\) 0-strongly connected if for any \(o,o' \in O\), there exists a sequence \(o_1,\dots,o_k\), such that \(o_1 = o\), \(o_k = o'\), and for any \(1\le j < k\), \(o_j\in O\) and \(R(o_j,0^{|AP|+1}, o_{j+1})>0\). A set \(O\) is called 0-Bottom strongly connected component (0-BSCC) if it is a maximal 0-strongly connected set, and for any \(o\in O\) and \(e\notin O\), \(R(o, 0^{|AP|+1},e) = 0\).

We call 0-BSCC \(O\) of \(MD\) accepting, if there exists \((L_i,K_i) \in Acc_\gamma\), such that \(O\cap (S\times L_i) = \emptyset\) and \(O\cap (S\times K_i)\neq \emptyset\). Otherwise, we call \(BSCC\) \(O\) rejecting. Denote the union of all the accepting \(BSCC\) as \(ACC\) and the union of all the rejecting \(BSCC\) as \(REJ\).

Finally we define \(B_{\mathbb{P}(\gamma \mid [A],B) = 1, M} = ((S\times Q_\gamma \times \{ 0,1,\bot,\top\}^{AP} \times \{ 0, \bot\})\cup \{ q_{sink}\}, \Sigma, \delta, q_0,F^{=1})\) as a universal safety automaton, where \[q_0 = \{ (s,q,0^{AP},0) \mid i_{MD}(s,q) > 0 \}.\]

To define \(\delta\), first we need to define the following. Given \(\vec{v},\vec{v'}\in \{ 0,1,\bot,\top\}^{AP}\) and \(b,b'\in \{0,\bot \}\) define \(b'' = 0\), if \(b=b'=0\), otherwise \(b''=\bot\). Moreover, define \(\vec{v''}\in \{ 0,1,\bot,\top\}^{AP}\), such that for every \(a\in AP\), \[\vec{v''}_a = \begin{cases} \top, \text{ if } (a\in B) \vee (\vec{v}_a=\top) \vee (( \vec{v'}_a = \top) \wedge (\vec{v}_a =0)), \text{ else }\\ 0, \text{ if } (\vec{v}_a = \vec{v'}_a =0), \text{ else }\\ 1, \text{ if } ((\vec{v}_a = 1)\vee (\vec{v'}_a = \bot))\wedge (a\in A) \wedge (b'' = 0), \text{ else} \\ \bot. \end{cases}\] Define \(\vec{v''_0} \in \{0,\bot,\top \}^{AP}\) as \(\vec{v''}\) with \(1\) replaced by \(0\).

For \(s,s'\in S\), \(q,q'\in Q\) and \(t\in 2^{AP}\), such that for every \(a\), the implication \(\vec{v''}_a \in \{ 0,\top\} \Rightarrow l(s)_a = t_a\) holds, define \[\delta((s,q,\vec{v},b),(t,\vec{v'},b'))=\{ (s',q',\vec{v''},b'') \mid R((s,q),(\vec{v''_0},b''),(s',q')) > 0\},\] Otherwise, define \(\delta((s,q,\vec{v},b),(t,\vec{v'},b')) = q_{sink}\). Moreover, \(\delta(q_{sink}) = \{ q_{sink}\}\). \[F^{=1} = \overline{ REJ \times \{\bot,\top \}^{AP}\times \{\bot \}}\] Now let us define \(B_{\mathbb{P}(\gamma \mid [A],B) >0, M} = ((S\times Q_\gamma \times \{ 0,1,\bot,\top\}^{AP} \times \{ 0,\bot\})\cup \{ q_{sink}\}, \Sigma, \delta , {q_0} ,F^{>0} )\) as an existential reachability automaton, with \(q_0\) and \(\delta\) defined in the same way as in \(B_{\mathbb{P}(\gamma \mid [A],B) =1, M}\), but \[F^{>0} = ACC \times \{\bot,\top \}^{AP}\times \{\bot \}.\]

6.3 Correctness and the algorithm↩︎

7 Conclusion↩︎

We have introduced Disintegration Temporal Logic (DTL) for probabilistic hyperproperties. DTL reasons about probabilities conditioned on (possibly infinite) sequences of events using the notion of measure disintegration from probability theory. This allows the logic to express conditional independence and, consequently, hyperproperties like probabilistic non-interference and perfect indistinguishability. These hyperproperties belong to the linear fragment of DTL, which is decidable in polynomial time.

Moreover, we demonstrated applications of DTL to several classes of probabilistic systems. These include stochastic environments interacting with probabilistic systems, distributional properties of Markov decision processes, and probabilistic automata on infinite words. In each case, DTL reasons about conditional probability distributions induced by finite or infinite observations. For distributional properties and probabilistic automata, DTL replaces strict quantification over blind schedulers with “soft’’ probabilistic reasoning, yielding decidability in certain settings. Some of these properties belong to the qualitative fragment, for which we presented a model-checking algorithm.

References↩︎