Abstract
Compositional state space generation means the generation of a condensed version of the state space of a system in a compositional manner. The system is divided to parts. The state spaces of the parts are generated, condensed and composed to get a state space of the system. The method may be applied recursively; that is, the state spaces of the parts may have been generated compositionally. The generated condensed state space is in a certain sense equivalent with the ordinary state space, thus it can be used for the analysis of certain properties of the system.
Compositional state space generation is a very desirable goal because it has the potential to significantly increase the size of systems analysable with given computer resources. In this paper the theoretical and technical prerequisites of compositional state space generation methods are discussed. Then one particular method is developed. The method guarantees that the composed state spaces are equivalent in the sense of the theory of Communicating Sequential Processes (CSP) with the corresponding ordinary state spaces. Therefore the method is suitable for the analysis of the language and deadlock properties of systems which are not expected to execute infinite sequences of invisible transitions. The method is demonstrated with the aid of an example.
Keywords
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
Best, E.: COSY: Its Relation to Nets and to CSP. [Brauer & 87b] pp. 416–440.
Brand, D. & Zafiropulo, P.: On Communicating Finite State Machines. Journal of the ACM 30 (2) 1983 pp. 323–342.
Brauer, W., Reisig, W. & Rozenberg, G. (ed.): Petri Nets, Central Models and Their Properties. Lecture Notes in Computer Science 254, Springer-Verlag 1987, 480 p.
Brauer, W., Reisig, W. & Rozenberg, G. (ed.): Petri Nets, Applications and Relationships to Other Models of Concurrency. Lecture Notes in Computer Science 255, Springer-Verlag 1987, 516 p.
Brookes, S. D., Hoare, C. A. R. & Roscoe, A. W.: A Theory of Communicating Sequential Processes. Journal of the ACM, Vol 31. No 3 July 1984, pp. 560–599.
Brookes, S. D. & Roscoe, A. W.: An Improved Failures Model for Communicating Sequential Processes. Proceedings of the NSF-SERC Seminar on Concurrency, Lecture Notes in Computer Science 197, Springer-Verlag 1985, pp. 281–305.
Clarke, E. M., Grümberg, O. & Browne, M. C.: Reasoning about Networks with Many Identical Finite-State Processes. Carnegie-Mellon University, Department of Computer Science, Report CMU-CS-86-155, Pittsburgh 1986, 18 p.
Clarke, E. M. & Grümberg, O.: Avoiding the State Explosion Problem in Temporal Logic Model Checking Algorithms. Conference Record of the 6th ACM Symposium on Principles of Distributed Computing 1987, pp. 294–303.
Clarke, E. M., Long, D. E. & McMillan, K. L.: Compositional Model Checking. Proceedings of the Fourth IEEE Symposium on Logic in Computer Science, June 4–8, 1989, Asilomar, California, USA.
Cleaveland, R., Parrow, J. & Steffen, B.: The Concurrency Workbench. Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems 1989, Lecture Notes in Computer Science 407, Springer-Verlag 1990, pp. 24–37.
Finkel, A.: The Minimal Coverability Graph for Petri Nets. Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris, France, pp. 1–21.
Graf, S. & Steffen, B.: Compositional Minimization of Finite State Processes. Computer-Aided Verification '90 (Proceedings of the Workshop on Computer-Aided Verification, Princeton, New Jersey, USA), AMS-ACM DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3, 1991, pp. 57–73. (Earlier version in DIMACS Technical Report 90-31, June 1990.)
Hoare, C. A. R.: Communicating Sequential Processes. Prentice-Hall International 1985, 256 p.
Huber, P., Jensen, K. & Shapiro, R. M.: Hierarchies in Coloured Petri Nets. Advances in Petri Nets 1990,Lecture Notes in Computer Science 483, Springer-Verlag 1991, pp. 313–341. (Earlier version in Proceedings of the 10th International Conference on Application and Theory of Petri Nets, Bonn, West Germany 1989, pp. 192–209).
Jantzen, M.: Complexity of Place/Transition Nets. [Brauer & 87a] pp. 413–434.
Jensen, K.: Coloured Petri Nets. [Brauer & 87a] pp. 248–299.
Kanellakis, P. C. & Smolka, S. A.: On the Analysis of Cooperation and Antagonism in Networks of Communicating Processes. Proceedings of the 4th Annual ACM Symposium on Principles of Distributed Computing, 1985, pp. 23–38.
Karp, R. M. & Miller, R. E.: Parallel Program Schemata. Journal of Computer and System Sciences 3 (1969) pp. 147–195.
Kemppainen, J., Levanto, M., Valmari, A. & Clegg, M.: “ARA” Puts Advanced Reachability Analysis Techniques together. Proceedings of the 5th Nordic Workshop on Programming Environment Reserach, Tampere University of Technology, Software Systems Laboratory Report 14, Tampere, Finland 1992.
Lindqvist, M: Parameterized Reachability Trees for Predicate/Transition Nets. Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris, France, pp. 22–42.
Milner, R.: A Calculus of Communicating Systems. Lecture Notes in Computer Science 92, Springer-Verlag 1980.
Milner, R.: Communication and Concurrency. Prentice-Hall 1989. 260 p.
Nielsen, M.: CCS — And Its Relationship to Net Theory. [Brauer & 87b] pp. 393–415.
Olderog, E.-R. & Hoare, C. A. R.: Specification-Oriented Semantics for Communicating Processes. Acta Informatica 23 (1986) pp. 9–66.
Olderog, E.-R.: TCSP: Theory of Communicating Sequential Processes. [Brauer & 87b] pp. 441–465.
Overman, W. T.: Verification of Concurrent Systems: Function and Timing. Ph.D. Dissertation, University of California Los Angeles 1981, 174 p.
Peterson, J. L.: Petri Net Theory and the Modeling of Systems. Prentice-Hall 1981, 290 p.
Pnueli, A.: Applications of Temporal Logic to the Specification and Verification of Concurrent Systems: A Survey of Current Trends. Current Trends in Concurrency, Lecture Notes in Computer Science 224, Springer-Verlag 1986, pp. 510–584.
Pomello,L.: Some Equivalence Notions for Concurrent Systems. Advances in Petri Nets 1985, Lecture Notes in Computer Science 222, Springer-Verlag 1986, pp. 381–400.
Quemada, J., Pavón, S. & Fernández, A.: State Exploration by Transformation with LOLA. Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems 1989, Lecture Notes in Computer Science 407, Springer-Verlag 1990, pp. 294–302.
Räuchle, T. & Toueg, S.: Exposure to Deadlock for Communicating Processes is Hard to Detect. Information Processing Letters 21 (1985) pp. 63–68.
Reisig, W.: Petri Nets: An Introduction. EATCS Monographs on Theoretical Computer Science 4, Springer-Verlag 1985, 161 p.
Reisig, W.: Place/Transition Systems. [Brauer & 87a] pp. 117–141.
Souissi, Y. & Memmi, G.: Compositions of Nets via a Communication Medium. Advances in Petri Nets 1990, Lecture Notes in Computer Science 483, Springer-Verlag 1991, pp. 457–470. (Earlier version in Proceedings of the 10th International Conference on Application and Theory of Petri Nets, Bonn, West Germany 1989, pp. 292–311).
Souissi, Y.: On Liveness Preservation by Composition of Nets via a Set of Places. Proceedings of the 11th International Conference on Application and Theory of Petri Nets, Paris, France, pp. 104–122.
Valmari, A. & Tiusanen, M. A Graph Model for Efficient Reachability Analysis of Description Languages. Proceedings of the 8th European Workshop on Application and Theory of Petri Nets, Zaragoza, Spain, 1987, pp. 349–366.
Valmari, A.: PC-Rimst — A Tool for Validating Concurrent Program Designs. Microprocessing and Microprogramming 24 (1988) 1–5 (Proceedings of the EUROMICRO '88) pp. 809–818.
Valmari, A.: Some Polynomial Space Complete Concurrency Problems. Tampere University of Technology, Software Systems Laboratory Report 4, 1988, 34 p.
Valmari, A.: Error Detection by Reduced Reachability Graph Generation. Proceedings of the 9th European Workshop on Application and Theory of Petri Nets, Venice, Italy 1988, pp. 95–112.
Valmari, A.: Eliminating Redundant Interleavings during Concurrent Program Verification. Proceedings of the PARLE '89, Parallel Architectures and Languages Europe, Eindhoven, Vol. II, Lecture Notes in Computer Science 366, pp. 89–103.
Valmari, A.: Stubborn Sets for Reduced State Space Generation. Advances in Petri Nets 1990, Lecture Notes in Computer Science 483, Springer-Verlag 1991, pp. 491–515. (Earlier version in Proceedings of the 10th International Conference on Application and Theory of Petri Nets, Bonn, West Germany 1989, Vol II, pp. 1–22.
Valmari, A.: State Space Generation with Induction (Short Version). Scandinavian Conference on Artificial Intelligence-89, Frontiers in Artificial Intelligence and Applications, IOS, Amsterdam, Netherlands 1989, pp. 99–115.
Valmari, A.: A Stubborn Attack on State Explosion. Computer-Aided Verification '90 (Proceedings of the Workshop on Computer-Aided Verification, Princeton, New Jersey, USA), AMS-ACM DIMACS Series in Discrete Mathematics and Theoretical Computer Science, Vol. 3, 1991, pp. 25–41. (Earlier version in DIMACS Technical Report 90-31, June 1990.)
Valmari, A. & Tienari, M.: An Improved Failures Equivalence for Finite-State Systems with A Reduction Algorithm. Proceedings of the 11th International IFIP WG 6.1 Symposium on Protocol Specification, Testing and Verification, Stockholm, Sweden, June 1991, pp. 1–16. To appear in the North-Holland Protocol Specification, Testing and Verification series.
Valmari, A. & Clegg, M.: Reduced Labelled Transition Systems Save Verification Effort. Proceedings of the CONCUR '91, Amsterdam, Lecture Notes in Computer Science 527, Springer-Verlag 1991, pp. 526–540.
Valmari, A.: Stubborn Sets of Coloured Petri Nets. Proceedings of the 12th International Conference on Application and Theory of Petri Nets, Gjern, Denmark 1991, pp. 102–121.
Vogler, W.: Failures Semantics and Deadlocking of Modular Petri Nets. Acta Informatica 26 (1989) pp. 333–348.
Vuong, S. T., Hui, D. D. & Cowan, D. D.: Valira — A Tool for Protocol Validation via Reachability Analysis. Protocol Specification, Testing and Verification VI, North-Holland 1987, pp. 35–41.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Valmari, A. (1993). Compositional state space generation. In: Rozenberg, G. (eds) Advances in Petri Nets 1993. ICATPN 1991. Lecture Notes in Computer Science, vol 674. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56689-9_54
Download citation
DOI: https://doi.org/10.1007/3-540-56689-9_54
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56689-2
Online ISBN: 978-3-540-47631-3
eBook Packages: Springer Book Archive