Regular Model Checking Made Simple and Efficient Parosh A. Abdulla, Bengt Jonsson, Marcus Nilsson, and Julien d'Orso
We present a new technique for computing the transitive closure of a
regular relation characterized by a finite-state transducer. The
construction starts from the original transducer, and repeatedly adds
new transitions which are compositions of currently existing
transitions. Furthermore, we define an equivalence relation which we
use to merge states of the transducer during the construction. The
equivalence relation can be determined by a simple local check, since
it is syntactically characterized in terms of "columns" that label
constructed states. This makes our algorithm both simpler to present
and more efficient to implement, compared to existing approaches. We
have implemented a prototype and carried out verification of a number
of parameterized protocols.
|
concur02@fi.muni.cz |