Optimizing Partitioning of Transition Relations by Using High-Level Information
2000
The computation of the reachable state set is a core task of optimization and formal verification of sequential systems like controllers or protocols. State exploration techniques based on OBDDs use a partitioned representation of the transition relation to keep the OBDD-sizes manageable. This paper presents a new approach that significantly increases the quality of the partitioning of the transition relation of controllers given in the high-level description language Protocol Compiler, resulting in a much more efficient reachable states computation.
- Correction
- Cite
- Save
- Machine Reading By IdeaReader
9
References
1
Citations
NaN
KQI