For the most recent entries see the Petri Nets Newsletter.

Compositional State Space Generation.

Valmari, Antti

In: Proceedings of the 11th International Conference on Application and Theory of Petri Nets, 1990, Paris, France, pages 43-62. 1990.

Also in: Rozenberg, G.: Lecture Notes in Computer Science, Vol. 674; Advances in Petri Nets 1993, pages 427-457. Springer-Verlag, 1993.

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: system verification; analysis of behaviour of nets; state space; compositionality; CSP; Communicating Sequential Processes; compositional state space generation; condensed state space; composed state space; failure equivalence.


Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography