Substitution and Flip BDDs
TR-2003-41, Authors: Rune Møller Jensen and Henrik Reif Andersen
December 2003
Abstract
This report introduces two novel approaches for representing transition functions of finite transition systems encoded as Binary Decision Diagrams (BDDs). The first approach is substition BDDs where each transition is represented by a corresponding substitution on state variables. The second is flip BDDs where each transition is defined by the set of state variables with flipped value. We show that substitution BDDs can be used to find and propagate write conflicts in synchronous and asynchronous compositions. Furthermore, our experimental evaluation suggest that the complexity of image computations based on flip BDDs may compare positively to the usual relational product computation.
Technical report TR-2003-41 in IT University Technical Report Series, December 2003.
Available as
PDF.