Hierarchical image computation with dynamic conjunction scheduling

Image computation is the core operation for optimization and formal verification of sequential systems like controllers or protocols. State exploration techniques based on ordered binary decision diagrams (OBDDs) use a partitioned representation of the transition relation to keep the OBDD-sizes manageable. This paper presents algorithms for building a hierarchically partitioned transition relation and conjunction scheduling based on this partitioning. The conjunction scheduling algorithm allows one to dynamically reorder partitions and is targeted to improve the AndExist operation. Model checking experiments prove the effectiveness of the new algorithms