Efficient Simplification of Bisimulation Formulas
Uffe H. Engberg
Kim S. Larsen
In TACAS, pages
The problem of checking or optimally simplifying bisimulation
formulas is likely to be computationally very hard. We take a different view
at the problem: we set out to define a very fast algorithm, and then see what
we can obtain. Sometimes our algorithm can simplify a formula perfectly,
sometimes it cannot. However, the algorithm is extremely fast and can,
therefore, be added to formula-based bisimulation model checkers at
practically no cost. When the formula can be simplified by our algorithm,
this can have a dramatic positive effect on the better, but also more time
consuming, theorem provers which will finish the job.
Univ. of Aarhus and Odense, Denmark.
Available as PostScript,
BRICS WWW home page