Efficient Simplification of Bisimulation Formulas

Uffe H. Engberg
Kim S. Larsen

In TACAS, pages 89--103

Abstract:

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.

Comments
Univ. of Aarhus and Odense, Denmark.

Available as PostScript, DVI.

BRICS WWW home page