Symbolic Synthesis via BDDs

This lecture covers the efficient symbolic reactive synthesis for finite-horizon tasks using Binary Decision Diagrams (BDDs) to compactly represent Boolean functions and sets, as demonstrated by Keliang He, Andrew Wells, Lydia E. Kavraki, and Moshe Y. Vardi from Rice University. The presentation delves into the main parts of the problem, including Transition System and DFA, given with respect to Boolean variables, and computations involving Boolean functions and sets. The lecture also includes an example from Wikipedia and references a paper by R. E. Bryant on graph-based algorithms for Boolean function manipulation.