Temporal Properties of Conditional Independence in Dynamic Bayesian Networks

TL;DR

This paper investigates the verification of conditional independence properties in dynamic Bayesian networks over time, analyzing the computational complexity of different verification problems and identifying tractable cases.

Contribution

It introduces formal methods for verifying CI properties in DBNs against temporal logic specifications and characterizes their computational complexity.

Findings

Deciding stochastic CI properties is as hard as the Skolem problem.

Verifying structural CI properties against LTL and NBA is in PSPACE.

Certain structural restrictions make verification tractable.

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\"uchi 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.