Zeuge für die Verwendung von BDDs durch $EU(\phi_1,\phi_2)$

Question

Ich wollte fragen, ob Sie einen Algorithmus kennen, um den Zeugen für $EU(\phi_1,\phi_2)$ (CTL-Formel „Exist Until“) mithilfe von BDDs (Binäres Entscheidungsdiagramm).In der Praxis sollten Sie zur Berechnung von $EU(\phi_1,\phi_2)$ den Fixpunkt verwenden, also:

$\qquad \displaystyle EU(\phi_1,\phi_2)=\mu.Q (\phi_2 \vee (\phi_1 \wedge EX Q)) $

Wenn wir die Rekursion abwickeln, erhalten wir:

$qquad displaystyle begin{align} Q_0 &= textrm{false} Q_1 &= phi_2 Q_2 &= phi_2 vee (phi_1 wedge EX phi_2) vdots end {Align} $

und so weiter.

Um einen Zeugen (Pfad) zu generieren, können wir eine Vorwärts-Erreichbarkeitsprüfung innerhalb der Sequenz von $Q_i's$ durchführen, also einen Pfad finden

$\qquad \displaystyle \pi= s_1 ightarrow s_2 ightarrow \cdots ightarrow s_n$

so dass $s_i \in Q_{n-i} \cap R(s_{i-1})$ (wobei $R(s_{i-1})= \{ s \mid R(s_{i-1},s ) \}$ und $R(s_{i-1},s$) ist der Übergang von $s_{i-1}$ zu $s$ ) wobei $s_0 \in Q_n $ und $s_n \in Q_1=\ phi_2$.

Wie kann man das mit BDDs machen?

Answer 1

Was Sie beschreiben, ist eine symbolische Modellprüfung, die hier behandelt wird Satz Folien, unter Verwendung reduzierter geordneter BDDs.

Kurz gesagt, Sie führen immer noch die Fixpunktiteration durch, wobei die Hauptfrage darin besteht, wie die Transformation $Q\mapsto \phi_2\vee(\phi_1\wedge EXQ)$ auf BDDs durchgeführt wird.Die elementaren Operationen, die Sie benötigen, sind Umbenennen (um nicht gestrichene durch gestrichene Variablen in $Q$ zu ersetzen und $Q'$ zu erhalten), boolesche Operationen (um $\phi_2\vee(\phi_1\wedge R\wedge Q')$ zu bilden) und Abstraktion (um existenzielle Quantoreneliminierung für die geprimten Variablen durchzuführen).Die Zeugengenerierung kann dann auf ähnliche Weise ausgehend von den Anfangszuständen erfolgen, wobei bei Schritt $i$ vorausgesetzt wird, dass $s_i$ in $Q_{n-i}$ liegt, wie Sie es oben getan haben.