Temporal Properties of Conditional Independence in Dynamic Bayesian Networks

TL;DR

The paper tackles the problem of verifying how conditional-independence (CI) propositions evolve over time in Dynamic Bayesian Networks (DBNs) against temporal specifications. It introduces two specification formalisms, linear temporal logic (LTL) and non-deterministic Büchi automata (NBAs), to express temporal properties of CI, distinguishing between structural CI (graph-based) and stochastic CI (distribution-based). Structural CI model-checking for DBN-templates against LTL and NBAs is shown to lie in PSPACE and to be NP-hard as well as coNP-hard, with polynomial-time tractable cases under natural restrictions on the templates. In contrast, eventual stochastic CI is at least as hard as the Skolem problem for linear recurrence sequences (LRS), indicating deep number-theoretic hardness and challenging decidability for stochastic properties. The work thus provides a rigorous automata-theoretic and complexity-theoretic framework for CI verification in DBNs, with practical tractability only under restricted structural assumptions and significant hardness barriers for stochastic specifications.

Abstract

Dynamic Bayesian networks (DBNs) are compact graphical representations used to model probabilistic systems where interdependent random variables and their distributions evolve over time. 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). This problem has two variants. Stochastic CI properties take the given concrete probability distributions into account, while structural CI properties are viewed purely in terms of the graphical structure of the DBN. We show that deciding if a stochastic CI proposition eventually holds is at least as hard as the Skolem problem for linear recurrence sequences, a long-standing open problem in number theory. On the other hand, we show that verifying the evolution of structural CI propositions against LTL and NBA specifications is in PSPACE, and is NP- and coNP-hard. We also identify natural restrictions on the graphical structure of DBNs that make the verification of structural CI properties tractable.

Figures (3)

• Figure 1: The DBN-template described in Ex. \ref{['ex:intro']} and its unfolding as well as an example CPD.
• Figure 2: Bridge between islands $X_{i-1}$ and $X_i$. Initial template in dashed edges.
• Figure 3: An example of a DBN-template $\mathcal{T}$ with its unfolding and the transition system $\mathcal{S}$ constructed from $\mathcal{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 $W_1^2,W_1^1,W_2^1,W_3^2$ connecting $W_1^2$ and $W_3^2$ in the unfolding through the previous time slices.

Theorems & Definitions (23)

• Example 1.1
• Example 1.2
• Definition 2.1: Bayesian Network
• Definition 2.2: d-paths and d-separation
• Theorem 2.3: Soundness and completeness of d-separation, pearlbook, Meek
• Lemma 2.4
• proof
• Proposition 3.1
• proof
• Lemma 4.2