This chapter gives an overview and some concrete examples of state space reduction methods. The main limitation of using state spaces to verify behavioural properties of systems is the state explosion problem [106], i.e., that state spaces of systems may have an astronomical number of reachable states, which means that they are too large to be handled with the available computing power (memory and CPU speed). Methods for alleviating this inherent complexity problem are an active area of research, which has led to the development of a large collection of state space reduction methods. These methods have significantly broadened the class of systems that can be verified, and state spaces can now be used to verify systems of industrial size. Some of these methods [18, 61, 62, 108] have been developed in the context of the CPN modelling language. Other methods (e.g., [55, 87, 104, 110]) have been developed outside the context of the CPN modelling language. Most state space reduction methods are independent of the concrete modelling language used and hence are applicable to a large class of such languages.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Keywords
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.
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Jensen, K., Kristensen, L.M. (2009). Advanced State Space Methods. In: Coloured Petri Nets. Springer, Berlin, Heidelberg. https://doi.org/10.1007/b95112_8
Download citation
DOI: https://doi.org/10.1007/b95112_8
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-00283-0
Online ISBN: 978-3-642-00284-7
eBook Packages: Computer ScienceComputer Science (R0)