On Combining the Persistent Sets Method with the Covering Steps Graph Method

  • Pierre-Olivier Ribet
  • Fran çois
  • Bernard Berthomieu
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2529)


Concurrent systems are commonly verified after computing a state graph describing all possible behaviors. Unfortunately, this state graph is often too large to be effectively built. Partial-order techniques have been developed to avoid combinatorial explosion while preserving the properties of interest. This paper investigates the combination of two such approaches, persistent sets and covering steps, and proposes partial enumeration algorithms that cumulate their respective benefits.


Concurrent systems state space exploration partial-order persistent sets covering steps graph verification methods 


  1. [BF99]
    B. Bérard and L. Fribourg. Reachability analysis of (timed) petri nets using real arithmetic. In Proceedings of CONCUR’99, pages 178–193. Springer Verlag, LNCS 1664, 1999.Google Scholar
  2. [Cor96]
    J. C. Corbett. Evaluating deadlock detection methods for concurrent software. IEEE Transactions on software engineering, VOL. 22(NO. 3), March 1996.Google Scholar
  3. [CX97]
    F. Chu and X. Xie. Deadlock analysis of petri nets using siphons and mathematical programming. In IEEE Trans. on Robotics and Automation, volume 13, pages 793–804, 1997.CrossRefGoogle Scholar
  4. [God90]
    P. Godefroid. Using partial orders to improve automatic verification methods. In Proceedings of CAV’90, pages 321–340. ACM, DIMACS volume 3, 1990.Google Scholar
  5. [God96]
    P. Godefroid. Partial-Order Methods for the Verification of Concurrent Systems. Springer Verlag, LNCS 1032, 1996.Google Scholar
  6. [GP93]
    P. Godefroid and D. Pirottin. Refining dependencies improves partial-order verification methods. In Proceedings of CAV’93. Springer Verlag, LNCS 697, 1993.Google Scholar
  7. [GW93]
    P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Metho ds in System Design, 2(2):149–164, 1993.zbMATHCrossRefGoogle Scholar
  8. [Jen86]
    K. Jensen. Couloured petrinets. In Petri Nets: CentralMo deland Their Properties, pages 248–299. Springer-Verlag, LNCS 254, 1986.CrossRefGoogle Scholar
  9. [Maz86]
    A. Mazurkiewicz. Trace theory. In Petri Nets: Applications and Relationships to Other Model of Concurrency, Advances in Petri nets 1986, Part II; Proceedings of an advanced Course, pages 279–324. Springer Verlag, LNCS 255, 1986.Google Scholar
  10. [Mil89]
    R. Milner. Communication and Concurrency. Prentice Hall, 1989.Google Scholar
  11. [NT87]
    M. Naimi and M. Trehel. An improvement of the logN distributed algorithm for mutual exclusion. In Proceedings of ICDCS’87, pages 371–377, Washington, D.C., USA, September 1987. IEEE Computer Society Press.Google Scholar
  12. [Ove81]
    W. T. Overman. Verification of concurrent systems: function and timing. PhD thesis, University of California, 1981.Google Scholar
  13. [Pel93]
    D. Peled. All from one, one for all: On model checking using representatives. In Proceedings of CAV’93, pages 409–423. Springer Verlag, LNCS 697, 1993.Google Scholar
  14. [Pel98]
    Doron Peled. Ten years of partial order reduction. In Proceedings of CAV’98, pages 17–28. Springer Verlag, LNCS 1427, 1998.Google Scholar
  15. [PF90]
    D. H. Pitt and D. Freestone. The derivation of conformance tests from lotos specifications. IEEE Transactions on Software Engineering, 1990.Google Scholar
  16. [Rei85]
    W. Reisig. Petri Nets: an Introduction. Springer-Verlag, EATCS, 1985.Google Scholar
  17. [Val88a]
    A. Valmari. Error detection by reduced reachability graph generation. In Proceedings of ATPN’88. Springer Verlag, LNCS 424, 1988.Google Scholar
  18. [Val88b]
    A. Valmari. State Space Generation: Efficiency and Practicality. PhD thesis, Tampere University of Technology, 1988.Google Scholar
  19. [Val89]
    A. Valmari. Stubborn sets for reduced state space generation. In Proceedings of ATPN’89. Springer Verlag, LNCS 483, 1989.Google Scholar
  20. [Val90]
    A. Valmari. A stubborn attack on state explosion. In Proceedings of CAV’90, pages 25–42. ACM, DIMACS volume 3, 1990.Google Scholar
  21. [VAM96]
    F. Vernadat, P. Azéma, and F. Michel. Covering step graph. In Proceedings of ATPN’96. Springer Verlag, LNCS 1091, 1996.Google Scholar
  22. [VM97]
    F. Vernadat and F. Michel. Covering step graph preserving failure semantics. In Proceedings of ATPN’97. Springer Verlag, LNCS 1248, 1997.Google Scholar
  23. [WG93]
    P. Wolper and P. Godefroid. Partial-order methods for temporal verification. In Proceedings of CONCUR’93. Springer Verlag, LNCS 575, 1993.Google Scholar
  24. [ZDD93]
    M.C. Zhou, F. Dicesare, and A.A. Desrochers. A hybrid methodology for synthesis of petri net models for manufacturing systems. In IEEE Trans. on Robotics and Automation 8:3, pages 350–361, 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Pierre-Olivier Ribet
    • 1
  • Fran çois
    • 1
  • Bernard Berthomieu
    • 1
  1. 1.LAAS-CNRSToulouse cedexFrance

Personalised recommendations