Skip to main content
SpringerLink
Log in

Detection of Illegal Behaviours Based on Unfoldings

  • Conference paper
  • First Online:
Book cover Application and Theory of Petri Nets 1999 (ICATPN 1999)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1639))

Included in the following conference series:

Abstract

We show how the branching process approach can be used for the detection of illegal behaviors. Our study is based on the specification of properties in terms of testers that cover safety as well as liveness properties. We demonstrate that the unfolding method can be used in this context and propose an extension of it, called unfolding graphs, for the computation of failure equivalent graphs.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Best E., Partial Order Verification with PEP, Proc. POMIV’96, G. Holzmann, D. Peled and V. Pratt (eds), Am. Math. Soc., 1996.

    Google Scholar 

  2. Couvreur J.M, Paviot-Adet E, New Structural Invariants for Petri Nets Analysis, Proc. of ICATPN’94, LNCS 815, p 199–218, 1994

    Google Scholar 

  3. Couvreur J.-M., Poitrenaud D., Model Checking based on Occurrence Net Graph, Proc. of Formal Description Techniques IX, Theory, Applications and Tools, p. 380–395, 1996.

    Google Scholar 

  4. Engelfriet J., Branching Processes of Petri Nets, Acta Informatica, vol. 28, p. 575–591, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  5. Esparza J., Model Checking using Net Unfoldings, Proc. of TAPSOFT’93, LNCS vol. 668, p. 613–628, 1993.

    Google Scholar 

  6. Esparza J., Römer S., Vogler W. An Improvement of McMillan’s Unfolding Algorithm, Proc. of TACAS’96, LNCS vol. 1055, p. 87–106, 1996.

    Google Scholar 

  7. Godefroid P., Partial-Order Methods for the Verification of Concurent Systems, LNCS 1032, 1996.

    Google Scholar 

  8. Jensen K., Coloured Petri Nets, In Petri Nets: Central Model and their Properties, Advances in Petri Nets 1986, Part 1, Brauer W., Reisig W. & Rozenberg G. (eds), Springer Verlag, LNCS vol254, pp 248–299, Bad Honnef, Germany, September 19

    Chapter  Google Scholar 

  9. Kondratyev A., Kishinevsky M., Taubin A., Ten S., A structural Approach for the Analysis of Petri nets by Reducted Unfolding, Proc. of ICATPN’96, LNCS 1091, p 346–365, 1996

    Google Scholar 

  10. McMillan K.L., Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits, Proc. of the 4th Conference on Computer Aided Verification, LNCS vol. 663, p. 164–175, 1992.

    Google Scholar 

  11. Melzer S., Römer S., Deadlock Checking Using Net Unfoldings, Proc. of the 9th Conference on Computer Aided Verification, p. 352–363, 1997.

    Google Scholar 

  12. Murata T., Petri Nets: Properties, Analysis, and Applications, Proc. of the IEEE, vol. 77, n 4, p. 541–580, 1989.

    Article  Google Scholar 

  13. Nielsen M., Plotkin G., Winskel G., Petri Nets, Events Structures and Domains, Part I, Theoretical Computer Science, vol. 13, n 1, p. 85–108, 1981.

    Article  MATH  MathSciNet  Google Scholar 

  14. Peled D., All from One, One for All: on Model Checking Using Representatives, Proc. on the 5th Conference on Computer Aided Verification, LNCS vol. 697, p. 409–423, 1993.

    Google Scholar 

  15. Poitrenaud D., Graphes de Processus Arborescents pour la vérification de Propriétés, Thèse de Doctorat de l’Université Paris IV, 1996.

    Google Scholar 

  16. Valmari A., Compositional State Space Generation, Proc of ICATPN’90, p. 43–62, Paris, France, 1990.

    Google Scholar 

  17. Valmari A., Stubborn Sets for Reduced State Space Generation, Advances in Petri Nets, LNCS vol. 483, p. 491–515, 1991.

    Google Scholar 

  18. Valmari A., On-the-fly Verification with Stubborn Sets, Proc. of the 5th Conference on Computer Aided Verification, LNCS vol. 697, p. 397–408, 1993.

    Google Scholar 

  19. Varpaaniemi K., Rauhamaa M., The Subborn Set Method in Practice, Advances in Petri Nets, LNCS vol. 616, p. 389–393, 1992.

    Google Scholar 

  20. Wallner F., Model Checking LTL using Net Unfolding, Proc. on the 10th Conference on Computer Aided Verification, 1998.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LaBRI, Université de Bordeaux I, Talence, France

    Jean-Michel Couvreur

  2. LIP6, Université de Paris 6, Paris, France

    Denis Poitrenaud

Authors
  1. Jean-Michel Couvreur
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Denis Poitrenaud
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università di Torino, C.so Svizzera 185, I-10149, Torino, Italy

    Susanna Donatelli

  2. LIACS, Leiden University , 2300 RA, Leiden, The Netherlands

    Jetty Kleijn

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Couvreur, JM., Poitrenaud, D. (1999). Detection of Illegal Behaviours Based on Unfoldings. In: Donatelli, S., Kleijn, J. (eds) Application and Theory of Petri Nets 1999. ICATPN 1999. Lecture Notes in Computer Science, vol 1639. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48745-X_22

Download citation

  • DOI: https://doi.org/10.1007/3-540-48745-X_22

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66132-0

  • Online ISBN: 978-3-540-48745-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation