This paper investigates the verification of temporal properties of conditional independence (CI) propositions in Dynamic Bayesian Networks (DBNs). The task involves checking whether the evolution of CI properties over time, represented as an infinite trace, satisfies specifications expressed in Linear Temporal Logic (LTL) or Non-deterministic Büchi Automata (NBAs). The core idea is to distinguish between stochastic CI (considering concrete probability distributions) and structural CI (based purely on graphical structure). The main empirical claim is that verifying stochastic CI properties is at least as hard as the Skolem problem for linear recurrence sequences, while verifying structural CI properties is PSPACE-complete, but becomes tractable (in P) for restricted DBN structures.
Problem
The paper addresses several bottlenecks related to the verification of conditional independence in DBNs:
Lack of formal verification for temporal CI properties: There is a need for formal methods to verify how conditional independence properties evolve over time in DBNs against temporal logic specifications.
Computational complexity of stochastic CI: Deciding if a stochastic CI proposition eventually holds is computationally challenging, being at least as hard as the Skolem problem for linear recurrence sequences, a long-standing open problem in number theory.
Computational complexity of structural CI: Verifying the evolution of structural CI propositions against LTL and NBA specifications is complex, falling into PSPACE, and is NP-hard and coNP-hard.
Intricacy of d-separation completeness for DBNs: While d-separation is known to characterize structural CIs in static Bayesian Networks, extending this completeness to DBNs, where parameters are constrained across time slices, is intricate and not straightforward.
Key Contributions
Introduction of temporal specification mechanisms (LTL and NBAs) for the evolution of structural and stochastic CI propositions in DBN-templates and DBNs, respectively, and formulation of the resulting structural and stochastic CI model-checking problems.
Demonstration that structural CI model-checking problems for DBN-templates against LTL formulas and NBAs are both in PSPACE, and are NP-hard as well as coNP-hard.
Proof that under the natural restriction where the initial template of a DBN-template only contains edges that also appear as intra-slice edges in the step template, the structural CI model-checking problems are in P.
Proof that checking eventual stochastic CI in full DBNs with Conditional Probability Distributions (CPDs) is at least as hard as the Skolem problem for linear recurrence sequences.
Method
The method involves defining conditional independence (CI) propositions, representing their evolution as a trace, and then model-checking this trace against temporal logic specifications.
Conditional Independence:
Stochastic CI: For sets of random variables X, Y, Z, denoted (X ⊥ Y | Z), it holds if for any values x, y, z (provided Pr[Z = z] > 0), Pr(X = x, Y = y | Z = z) = Pr(X = x | Z = z) ⋅ Pr(Y = y | Z = z).
Structural CI: For sets X, Y, Z, denoted (X ⊥ Y | Z), it holds if Z d-separates X and Y in the underlying Directed Acyclic Graph (DAG) template.
DBN Representation:
A DBN is defined by an initial Bayesian Network (BN) for variables V⁰ and a step BN for variables Vᵗ⁺¹ conditioned on Vᵗ. These define a DBN-template TDBN = (V, E⁰, Estep).
The DBN-template can be "unfolded" into an infinite Directed Acyclic Graph (DAG) representing dependencies over time.
An atomic proposition of structural CI (X ⊥ Y | Z) holds at time t if (Xᵗ ⊥ Yᵗ | Zᵗ) holds in the unfolding of T.
An atomic proposition of stochastic CI (X ⊥ Y | Z) holds at time t in a DBN B if (Xᵗ ⊥ Yᵗ | Zᵗ) holds in the BN formed at time t.
Trace Generation:
For a finite set A of structural CI propositions, a DBN-template defines a trace τ ∈ (2ᴬ)ω, an infinite word where the t-th position indicates which propositions hold at time t.
Similarly, for a finite set B of stochastic CI propositions, a full DBN defines a trace τ ∈ (2ᴮ)ω.
Temporal Logic Specifications:
Linear Temporal Logic (LTL): Formulae φ over atomic propositions A are syntactically given by φ := a | ¬φ | φ ∧ φ | Oφ | φ U φ. Operators include O (next), U (until), ◇ (eventually), and □ (globally).
Non-deterministic Büchi Automata (NBAs): An NBA is a tuple A = (Q, Σ, Δ, Q₀, F) that accepts ω-regular languages.
Model Checking Problems:
Structural LTL/NBA model-checking: Decide if the trace of a DBN-template satisfies an LTL formula φ or is accepted by an NBA A.
Stochastic LTL/NBA model-checking: Decide if the trace of a DBN with concrete CPDs satisfies an LTL formula φ or is accepted by an NBA A.
Transition System Construction for Structural CI:
The trace of a DBN-template with respect to structural CI propositions is ultimately periodic.
This trace can be represented as the run of a deterministic transition system S = (Q, q₀, →, A, L).
State Space: Q consists of BN-templates representing connections via collision-free d-paths. For t > 0, there are 2^O(|V|²) possible representatives, each representable as a graph with O(|V|²) vertices.
Transition Relation: The successor of a representative BN-template is computed in polynomial time by constructing a graph with vertices U ∪ V ∪ U' ∪ V' and adding edges based on the current template and step template.
Labeling Function: The labeling function L: Q → 2ᴬ determines which CI propositions hold in a given state by running d-separation queries on the representative BN-template, computable in time polynomial in |V| and |A|.
Technical Details
Conditional Independence:
Stochastic CI: Pr(X = x, Y = y | Z = z) = Pr(X = x | Z = z) ⋅ Pr(Y = y | Z = z) for Pr[Z = z] > 0.
Structural CI: (X ⊥ Y | Z) if Z d-separates X and Y.
DBN Template: TDBN = (V, E⁰, Estep). V is a finite set of random variables. E⁰ are initial dependencies, Estep are step-wise dependencies.
Trace Representation: A DBN-template's trace is ultimately periodic and can be represented as a deterministic transition system with 2^O(|V|²) states.
State Representation: Each state of the transition system can be represented in O(|V|²) space.
Computational Complexity (Structural CI):
Structural LTL and NBA model-checking problems for DBN-templates are in PSPACE, NP-hard, and coNP-hard.
For restricted DBN-templates (where initial template edges also appear as intra-slice edges in the step template), these problems are in PTIME.
The trace of a restricted DBN-template is ultimately constant after at most |V|² time steps.
Computational Complexity (Stochastic CI):
Checking eventual stochastic CI (e.g., ◇(X ⊥ Y)) is at least as hard as the Skolem problem for linear recurrence sequences.
A rational LRS of order k is a sequence (u_n)_n=0^∞ satisfying u_n+k = a_k-1 u_n+k-1 + ... + a₀ u_n. The Skolem problem asks if u_n = 0 for some n.
The reduction involves constructing a DBN with [log k] + 2 binary variables X, Z₁, ..., Z_l, Y such that ◇(X ⊥ Y) holds if and only if the LRS has a zero term.
Transition System Computation:
Successor function can be computed in time polynomial in |V|.
Labeling function can be computed in time polynomial in |V|, |A|.
Results
Computational Complexity for Structural CI:
DBN-templates (General): Structural LTL and NBA model-checking problems are in PSPACE, and are NP-hard as well as coNP-hard.
DBN-templates (Restricted): Structural LTL and NBA model-checking problems are in PTIME.
Computational Complexity for Stochastic CI:
DBNs (General): Checking eventual stochastic CI (e.g., ◇(X ⊥ Y)) is at least as hard as the Skolem problem for linear recurrence sequences. This implies that a decidability result for stochastic CI model-checking problems is out of reach without a breakthrough in analytic number theory.
Trace Properties:
The trace of a DBN-template with structural CI propositions is ultimately periodic.
For restricted DBN-templates, the trace is ultimately constant after at most |V|² time steps.
Weaknesses / Limitations
Completeness of d-separation for DBNs: The paper notes that while Proposition 3.1 shows soundness (structural CI implies stochastic CI), the converse direction (completeness of d-separation for DBNs) is intricate. This is because DBNs impose constraints on parameters by identifying distributions of the same variables across time slices, which reduces the dimensionality of the parameter space and makes generalizing the completeness proof challenging.
Hardness of Stochastic CI Verification: The result that checking eventual stochastic CI is as hard as the Skolem problem implies that a general decidability result for stochastic LTL or NBA model-checking of DBNs is currently out of reach without a major breakthrough in number theory.
Evidence
Method evidence: "In this paper, we study the verification of the evolution of conditional-independence (CI) propositions against temporal logic specifications. To this end, we consider two specification formalisms over CI propositions: linear temporal logic (LTL), and non-deterministic Büchi automata (NBAs)." (section: Abstract)
Result evidence: "In Sec. 4, we show that the structural CI model-checking problems of DBN-templates against LTL formulas and against NBAs are both in PSPACE and NP-hard as well as coNP-hard. Under the natural restriction that the initial template of a DBN-template only contains edges that also appear as intra-slice edges in the step template, we prove that the problems are in P." (section: 1.1 Contributions)
Limitation evidence: "Given full DBNs with CPDs, we show in Sec. 5 that checking eventual stochastic CI is as hard as the Skolem problem for linear recurrence sequences, a famous number-theoretic problem whose decidability status has been open for many decades. This implies that a decidability result for the stochastic CI model-checking problems is out of reach without a breakthrough in analytic number theory." (section: 1.1 Contributions)
Additional Figures
Figure 1: The DBN-template described in Ex. 1.1 and its unfolding as well as an example CPD.
Figure 2: Bridge between islands X i−1 and X i . Initial tem- plate in dashed edges. The improved complexity for restricted DBN-templates follows from the insight that the trace of a restricted DBN- template on variables V is constant from time ∣V∣ 2 onwards.
Figure 3: An example of a DBN-template T with its un- folding and the transition system S constructed from T . Variables U ij without outgoing edges are omitted. Note, e.g., that the variable U 13 is connected to W 1 and W 2 after two time steps reflecting that there is a collision-free d-path