Efficient simplification of bisimulation formulas

  • Uffe H. Engberg
  • Kim S. Larsen
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1019)


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.


Free Variable Universal Quantification Combine Structure Abstract Algorithm Function Check 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [1]
    W. Ackermann. Zum Hilbertschen Aufbau der reellen Zahlen. Math. Annalen, 99:118–133, 1928.Google Scholar
  2. [2]
    R. Bayer. Symmetric Binary B-Trees. Acta Inform., 1:290–306, 1972.Google Scholar
  3. [3]
    S.A.Cook. The Complexity of Theorem-Proving Procedures. In ACM STOC, pages 151–158, 1971.Google Scholar
  4. [4]
    U.H. Engberg. Simple Symbolic Bisimulations. In preparation.Google Scholar
  5. [5]
    U.H. Engberg and K.S. Larsen. Efficient Reduction of Bismulation Formulas. Preprint 47, Dept. of Math. and Computer Science, Odense University, 1993.Google Scholar
  6. [6]
    B.A. Galler and M.J. Fischer. An improved equivalence algorithm. Comm. ACM, 7:301–303, 1964.Google Scholar
  7. [7]
    M.R. Garey and D.S. Johnson. Computers and Intractability. W. H. Freeman, 1979.Google Scholar
  8. [8]
    L.J.Guibas and R,.Sedgewick. A Dichromatic Framework for Balanced Trees. IEEE FOCS, 8–21, 1978.Google Scholar
  9. [9]
    M. Hennessy and H. Lin. Symbolic Bismulations. Tech. Rep. 1/92, University of Sussex, 1992. Appear in Theoretical Computer Science 138 (1995) 353–389.Google Scholar
  10. [10]
    M. Hennessy and H. Lin. Proof systems for message-passing process algebras. CONCUR '93, pages 202–216, August 1993.Google Scholar
  11. [11]
    G.J. Klir and T.A. Folger. Fuzzy Sets, Uncertainty, and Information. Prentice-Hall, 1988.Google Scholar
  12. [12]
    H. Mannila and E. Ukkonen. The set union problem with backtracking. LNCS 226, 236–243, 1986.Google Scholar
  13. [13]
    K. Mehlhorn and A. Tsakalidis. Data Structures. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, chapter 6, pages 301–341. Elsevier Science Publishers, 1990.Google Scholar
  14. [14]
    R. Milner. Communication and Concurrency. Prentice-Hall, 1989.Google Scholar
  15. [15]
    Z. Schreiber. Verification of Value-Passing Systems. In First North American Process Algebra Workshop, pages 9.1–9.20. Tech. Rep. 92-15, Johns Hopkins University, 1992.Google Scholar
  16. [16]
    D. Scott. Notes on the formalization of logic. Technical report, Subfaculty of Phil., Oxford, 1981.Google Scholar
  17. [17]
    R.E. Tarjan. Efficiency of a good but not linear set union algorithm. JACM, 22:215–225, 1975.Google Scholar
  18. [18]
    R.E. Tarjan. Data Structures and Network Algorithms. Soc. for Industrial and Applied Math., 1983.Google Scholar
  19. [19]
    R.E. Tarjan and J.V. Leeuwen. Worst-Case Analysis of Set Union Algorithms. JACM, 31:245–281, 1984.Google Scholar
  20. [20]
    J. Westbrook and R.E. Tarjan. Amortized analysis of algorithms for set union with backtracking. SIAM J. Comput., 18(1):1–11, 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Uffe H. Engberg
    • 1
  • Kim S. Larsen
    • 2
  1. 1.BRICS (Basic Research in Computer Science, a Centre of the Danish National Research Foundation), Department of Computer ScienceUniversity of AarhusDenmark
  2. 2.Department of Mathematics and Computer ScienceOdense UniversityDenmark

Personalised recommendations