Download A Modular ROS package for Linear Temporal Logic based Motion

3.3 Binary Decision Diagrams library and cross product generation
Binary decision diagram (BDD) is a data structure that is extensively used for model
checking and synthesis of hardware circuits. BDD's are actually compact encoding of
splitting trees used to evaluate Boolean expressions. A BDD has a few properties (1)
being an acyclic graph, (2) it has shared sub-trees and (3) presents a compact way to
represent Boolean functions. These trees are ordered such that if a branch goes from node
i to node j then i < j, the BDD also has to be in a reduced form, these two properties if
adhered to define a BDD. The following Figure 11: Depicting the splitting tree of (q →
p) ^ r → (p ↔ r) ^ q and Figure 12: Depicting the binary decision diagram of (q → p) ^ r
→ (p ↔ r) ^ q show the Boolean expression (q → p) ^ r → (p ↔ r) ^ q. It clearly depicts
how easily a decision tree can be compressed using a BDD and how compact the final
representation becomes. This property of BDD is helpful in finding the satisfiability of
Boolean expressions because it has lesser memory and computation requirements to parse
from root to sink of the tree.
Figure 11: Depicting the splitting tree of (q → p) ^ r → (p ↔ r) ^ q
32