Advertisement

Partial Order Reductions for Bisimulation Checking

  • Michaela Huhn
  • Peter Niebert
  • Heike Wehrheim
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1530)

Abstract

Partial order methods have been introduced to avoid the state explosion problem in verification resulting from the representation of multiple interleavings of concurrent transitions. The basic idea is to build a reduced state space on which certain properties hold if and only if they hold for the full state space. Most often, the considered properties are linear-time properties. In this paper we suggest novel branching time reduction techniques which allow checking bisimulation equivalence on reduced state spaces. Our reduction takes place on bisimulation game graphs, thus jointly treating the systems under consideration. We show that reduction preserves winning strategies of the two players in the bisimulation game.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. dSdS95.
    de Souza, M.L., de Simone, R.: Using partial order methods for the verification of behavioural equivalences. In: von Bochmann, G. (ed.) Formal Description Techniques, FORTE 1995 (1995)Google Scholar
  2. FM90.
    Fernandez, J.-C., Mounier, L.: Verifying bisimulations ”on the fly”. In: Formal Description Techniques (FORTE), pp. 91–105 (1990)Google Scholar
  3. GKPP95.
    Gerth, R., Kuiper, R., Peled, D., Penczek, W.: A partial order approach to branching time model checking. In: Israeli Symp. on Theoretical Computer Science (1995)Google Scholar
  4. HWN98.
    Huhn, M., Wehrheim, H., Niebert, P.: Partial order reductions for bisimulation checking. Hildesheimer Informatik-Berichte 8/98, Institut für Informatik, Universität Hildesheim (1998)Google Scholar
  5. Kla94.
    Klarlund, N.: The limit view of infinite computations. BRICS Report Series RS-94-14, Department of Computer Science, University of Århus, Ny Munkegade, building 540, DK-8000 Århus C, Denmark (May 1994)Google Scholar
  6. KS90.
    Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Information and Computation 86, 46–68 (1990)CrossRefMathSciNetGoogle Scholar
  7. Maz95.
    Mazurkiewicz, A.: Introduction to trace theory, ch. 1, pp. 1–42. World Scientific, Singapore (1995)Google Scholar
  8. Mil89.
    Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)zbMATHGoogle Scholar
  9. Pel93.
    Peled, D.: All from one, one for all: On model checking using representatives. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993)Google Scholar
  10. Pom96.
    Workshop on Partial Order Methods in Verification. DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 29. American Mathematical Society (1996) Google Scholar
  11. PP95.
    Peled, D., Penczek, W.: Using asynchronous Büchi automata for efficient model-checking of concurrent systems. In: Protocol Specification, Testing and Verification, pp. 90–100 (1995)Google Scholar
  12. SNW93.
    Sassone, V., Nielsen, M., Winskel, G.: A classification of models for concurrency. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 82–96. Springer, Heidelberg (1993)Google Scholar
  13. Sti93.
    Stirling. C.: Modal temporal logics for processes. Tutorial handout, Computer Science Dept., Århus University, Århus, Denmark, Summerschool in Logical Methods in Concurrency, August 2-13 (1993)Google Scholar
  14. Tho94.
    Thomas, W.: Finite-state strategies in regular infinite games. In: Thiagarajan, P.S. (ed.) FSTTCS 1994. LNCS, vol. 880, pp. 148–158. Springer, Heidelberg (1994)Google Scholar
  15. WW96.
    Willems, B., Wolper, P.: Partial-order methods for model checking: From linear time to branching time. In: IEEE Symp. Logic in Comp. Sci (LICS), pp. 294–303. IEEE Computer Society Press, Los Alamitos (1996)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Michaela Huhn
    • 1
  • Peter Niebert
    • 2
  • Heike Wehrheim
    • 3
  1. 1.Institut für Rechnerentwurf und Fehlertoleranz(Prof. D. Schmid) Universität KarlsruheKarlsruheGermany
  2. 2.Institut für Informatik(Prof. U.Goltz) Universität HildesheimHildesheimGermany
  3. 3.Fachbereich Informatik, Abteilung Semantik(Prof. E.-R. Olderog) Universität OldenburgOldenburgGermany

Personalised recommendations