Efficient Simplification of Bisimulation Formulas

Uffe H. Engberg
Kim S. Larsen

In TACAS, pages 89--103


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, DVI.

[BRICS symbol] BRICS WWW home page