|
Abstract : |
We present the edge-Streett/edge-Rabin environment for doing verification using language containment. This environment has a number of desirable properties compared with the L-process/L-automaton environment ([Kur87b]), which is a practical language-containment-based formal verification environment: ffl It contains the L-environment as a subset. ffl It can be exponentially more compact than the L-environment. ffl We present BDD-based algorithms for main verification functions in this environment, and argue that they are efficient. Furthermore, if the specifications come from the L-environment, our algorithms reduce to the algorithms of [HTKB92] and [HBK93] for the L-environment. ffl It is in some sense maximal, i.e. language containment check for the next natural extension to our environment is NP-complete (as opposed to polynomial). We have implemented our algorithms in our verification tool, and will present a flexible user interface to this environment. 1, |
