Advertisement

Relaxed visibility enhances partial order reduction

  • Ilkka Kokkarinen
  • Doron Peled
  • Antti Valmari
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1254)

Abstract

State-space explosion is a central problem in the automatic verification (model-checking) of concurrent systems. Partial order reduction is a method that was developed to try to cope with the state-space explosion. Based on the observation that the order of execution of concurrent (independent) atomic actions is in many cases unimportant for the checked property, it allows reducing the state space by exploring fewer execution sequences. However, to be on the safe side, partial order reductions put constraints about commuting the order of atomic actions that may change the value of propositions appearing in the checked specification. In this paper we relax this constraint, allowing a weaker requirement to be imposed, achieving a better reduction. We demonstrate the benefits of our improved reduction with experimental results.

Keywords

Model Check Linear Temporal Logic Atomic Action Concurrent System Incoming Edge 
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.

References

  1. 1.
    C. Courcoubetis, M. Vardi, P. Wolper, M. Yannakakis, Memory-efficient algorithms for the verification of temporal properties, Formal Methods in System Design 1 (1992) 275–288.Google Scholar
  2. 2.
    R. Gerth, D. Peled, M. Vardi, P. Wolper, Simple On-the-fly Automatic Verification of Linear Temporal Logic, PSTV95, Protocol Specification Testing and Verification, 3–18, Chapman & Hall, 1995, Warsaw, Poland.Google Scholar
  3. 3.
    P. Godefroid. Using partial orders to improve automatic verification methods. In Proc. 2nd Workshop on Computer Aided Verification, LNCS 531, Springer-Verlag, New Brunswick, NJ, 1990, 176–185.Google Scholar
  4. 4.
    P. Godefroid, D. Pirottin, Refining dependencies improves partial order verification methods, 5th Conference on Computer Aided Verification, Elounda, Greece, LNCS 697, Springer-Verlag, 1993, 438–449.Google Scholar
  5. 5.
    P. Godefroid, P. Wolper, A Partial Approach to Model Checking, 6th Annual IEEE Symposium on Logic in Computer Science, 1991, Amsterdam, 406–415.Google Scholar
  6. 6.
    S. Katz, D. Peled, Verification of Distributed Programs using Representative Interleaving Sequences, Distributed Computing 6 (1992), 107–120.Google Scholar
  7. 7.
    S. Katz, D. Peled, Defining conditional independence using collapses, Theoretical Computer Science 101 (1992), 337–359.Google Scholar
  8. 8.
    I. Kokkarinen, Reduction of Parallel Labelled Transition Systems with Stubborn Sets, M. Sc. (Eng.) Thesis (in Finnish), 49 p.Google Scholar
  9. 9.
    L. Lamport, What good is temporal logic, Information Processing 83, Elsevier Science Publishers, 1983, 657–668.Google Scholar
  10. 10.
    D. Peled, All from one, one for all, on model-checking using representatives, 5th Conference on Computer Aided Verification, Elounda, Greece, 1993, LNCS 697, Springer-Verlag, 409–423.Google Scholar
  11. 11.
    D. Peled. Combining partial order reductions with on-the-fly model-checking. Formal Methods in System Design 8 (1996), 39–64.Google Scholar
  12. 12.
    A. Pnueli, The temporal logic of programs, 18th FOCS, IEEE Symposium on Foundation of Computer Science, 1977, 46–57.Google Scholar
  13. 13.
    A. Valmari, Stubborn sets for reduced state space generation, 10th International Conference on Application and Theory of Petri Nets, Bonn, Germany, 1989, LNCS 483, Springer-Verlag, 491–515.Google Scholar
  14. 14.
    A. Valmari, A stubborn attack on state explosion. Formal Methods in System Design, 1 (1992), 297–322.Google Scholar
  15. 15.
    A. Valmari, On-the-fly Verification with Stubborn Sets, 5th Conference on Computer Aided Verification, Elounda, Greece, 1993, LNCS 697, Springer-Verlag, 397–408.Google Scholar
  16. 16.
    B. Willems, P. Wolper, Partial-Order Methods for Model Checking: From Linear Time to Branching Time, 11th Annual IEEE Symposium on Logic in Computer Science, 1996.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Ilkka Kokkarinen
    • 1
  • Doron Peled
    • 2
  • Antti Valmari
    • 1
  1. 1.Software Systems LaboratoryTampere University of TechnologyTampereFinland
  2. 2.Bell LaboratoriesLucent TechnologiesMurray HillUSA

Personalised recommendations