Verifikation von bedingter Unabhängigkeit in dynamischen Bayesschen Netzwerken

Dynamic Bayesian Networks (DBNs) sind kompakte graphische Modelle, die probabilistische Systeme beschreiben, in denen sich abhängige Zufallsvariablen und ihre Verteilungen im Zeitverlauf verändern. In der vorliegenden Arbeit wird untersucht, wie die Entwicklung von bedingten Unabhängigkeits‑(CI)‑Aussagen gegen zeitliche Logik‑Spezifikationen verifiziert werden kann.

Zur Formalisierung werden zwei Spezifikationsformen verwendet: lineare temporale Logik (LTL) und nichtdeterministische Büchi-Automaten (NBA). Dabei unterscheiden sich die zu prüfenden CI‑Aussagen in zwei Varianten. Stochastische CI‑Eigenschaften berücksichtigen konkrete Wahrscheinlichkeitsverteilungen, während strukturelle CI‑Eigenschaften ausschließlich die graphische Struktur des DBNs betrachten.

Die Ergebnisse zeigen, dass die Frage, ob eine stochastische CI‑Aussage irgendwann zutrifft, mindestens so schwer ist wie das Skolem‑Problem für lineare Rekurrenz‑Sequenzen – ein langjähriges offenes Problem in der Zahlentheorie. Im Gegensatz dazu lässt sich die Verifikation struktureller CI‑Aussagen gegen LTL‑ und NBA‑Spezifikationen in PSPACE entscheiden, wobei die Aufgabe NP‑ und coNP‑schwer ist. Darüber hinaus identifiziert die Studie natürliche Beschränkungen der graphischen Struktur von DBNs, die die Verifikation struktureller CI‑Eigenschaften in praktikable Komplexitätsklassen bringen.

Diese Erkenntnisse liefern wichtige Einblicke in die Grenzen der automatischen Überprüfung dynamischer probabilistischer Modelle und legen zugleich Ansatzpunkte für zukünftige Forschung in der Verifikation von zeitabhängigen Unabhängigkeits‑Aussagen nahe.