Efficient Simplification of Bisimulation Formulas.

Uffe Engberg and Kim S. Larsen.
In 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 1019 of Lecture Notes in Computer Science, pages 111-132. Springer, 1995.

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.

---

publication

Link to the publication at the publisher's site - subscription may be required.
Text required by the publisher (if any): The final publication is available at link.springer.com.

open access (239 KB)

The same as the publisher's version, when the publisher permits. Otherwise, the author's last version before the publisher's copyright; this is often exactly the same, but sometimes fonts, page numbers, figure numbers, etc. are different. It may also be a full version. However, it is safe to read this version, and at the same time cite the official version, as long as references to concrete locations, numbered theorems, etc. inside the article are avoided.

other publications

Other publications by the author.