Abstract
The computation of a reachability graph is one of the most used method to check system properties. Its main drawback is the state explosion. Two different approaches are generally used to tackle this problem: by defining new concise graph representations for which verification methods are adapted; by reducing graphs while preserving observed properties. We propose a new representation of a reachability graph where nodes are particular Petri nets, occurrence nets, characterizing parts of the state space. Checking invariant properties can be done using efficient algorithms for occurrence nets. Moreover, our representation can be used to obtain a stuttering equivalent graph on which nexttime-less linear temporal formulae are verified.
Chapter PDF
Similar content being viewed by others
References
Berthelot, G.: «Checking Properties of Nets Using Transformations». Advances in Petri Nets 1985, Rozenberg, G. (ed.), Springer Verlag, LNCS vol 222, pp 19–40, 1986.
Clarke E., Grumberg O. & Long D.: «Verification tools for finite-state concurrent systems», In: A Decade of Concurrency - Reflections and Perspectives, LNCS vol 803, 1994.
Couvreur J.M. & Paviot-Adet E.: «New Structural Invariants for Petri Nets Analysis». 15th Int. Conference on Application and Theory of Petri Nets, Valette R. (ed), Springer Verlag, LNCS vol 815, pp 199–218, Zaragoza, Spain, June 1994.
Esparza J.: «Model Checking Using Net Unfoldings». Science of Computer Programming, vol 23, pp 151–195, 1994.
Esparza J., Römer S. & Vogler W.: «An Improvement of McMillan’s Unfolding Algo rithm». Proc. of 2nd Int. Workshop TACAS’96, Springer Verlag, LNCS vol 1055, pp 87–106, Passau, Germany, March 1996.
Grahlmann B. & Best E.: «PEP - More than a Petri Net Tool». Proc. of 2nd Int. Work shop TACAS’96, Springer Verlag, LNCS vol 1055, pp 397–401, Passau, Germany, March 1996.
Godefroid P. & Wolper P.: «A Partial Approach to Model Checking». Information and Computation, vol 110, No 2, pp 305–326, May 1994.
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 vol 254, pp 248–299, Bad Honnef, Germany, September 1986.
Kaivola R. & Valmari A.: «The Weakest Compositional Semantic Equivalence Pre-serving Nexttime-less Linear Temporal Logic». Proc. of the 3th Int. Conference on Concurrency Theory, Cleaveland W.R. (ed.), Springer Verlag, LNCS vol 630, pp 207–221, Stony Brook, NY, USA, August 1992.
Lamport L.: «What Good is Temporal Logic?», Proc. of the IFIP 9th World Computer Congress, pp 657–668, 1983.
McMillan K.L.: «Using Unfoldings to Avoid the State Explosion Problem in the Verifi¬cation of Asynchronous Circuits». Proc. of the 4th Int. conference on Computer-Aided Verification, Springer Verlag, LNCS vol 663, pp 164–175, Montreal, Canada, June 1992.
Murata T.: «Petri Nets: Properties, Analysis and Applications». Proc. of the IEEE, vol 77, No 4, pp 541–580, April 1989.
Nielsen M., Plotkin G. & Winskel G.: «Events Structures and Domains». Theoretical computer Science, vol 13, No 1, pp 85–108, 1980.
Pastor E., Roig O., Cortadella J. & Badia R.M.: «Petri Net Analysis using Boolean Manipulation». 15th Int. Conference on Application and Theory of Petri Nets, Valette R. (ed), Springer Verlag, LNCS vol 815, pp 416–435, Zaragoza, Spain, June 1994.
Reisig W.: «Petri Net Models of Distributed Algorithms». In Computer Science Today: Recent Trends and Developments, Jan van Leeuven (ed.), Springer Verlag, LNCS vol 1000, 1995.
Valmari A.: «Stubborn Sets for Reduced State Space Generation». Advances Petri Nets 90, Springer verlag, LNCS vol 483, pp 491–515, 1991.
Varpaaniemi K. & Rauhamaa M.: «The Stubborn Set Method in Practice». 13th Int. Conference on Application and Theory of Petri Nets, Jensen K. (ed), Springer Verlag, LNCS vol 616, pp 389–393, Sheffield, UK,June 1992.
Wolper P.: «On the relation of Programs and Computations to Models of Temporal Logic». Proc. of Temporal Logic in Specification, Banieqbal B., Barringer H. & Pnueli A. (eds.), Springer Verlag, LNCS vol 398, pp 75–123, 1989.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Couvreur, JM., Poitrenaud, D. (1996). Model Checking Based on Occurrence Net Graph. In: Gotzhein, R., Bredereke, J. (eds) Formal Description Techniques IX. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35079-0_24
Download citation
DOI: https://doi.org/10.1007/978-0-387-35079-0_24
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2883-4
Online ISBN: 978-0-387-35079-0
eBook Packages: Springer Book Archive