# 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