The First Steps Towards Using State Spaces of Object-Oriented Petri Nets

Petri nets, object-orientation, state spaces

The article discusses the notion of state spaces of object-oriented Petri nets associated to the tool called PNtalk and the role of identifiers of dynamically appearing and disappearing instances within these state spaces.

This article describes the first steps towards state spaces-based formal analysis and verification using the kind of object-oriented Petri nets supported by the tool called PNtalk which has been developed at the Technical University of Brno. These nets are denoted simply as OOPNs in the following. After a short review of the concept of OOPNs the notion of their state spaces is discussed including problems associated to efficiently treating identifiers of dynamically appearing and disappearing instances. Methods of working with identifiers based on sophisticated naming rules and methods based on using name-abstracting mechanisms are described and compared. Subsequently, several techniques of making the generation of OOPNs' state spaces more efficient are briefly mentioned, as well. The introduced notions and methods can be considered to form a basis for future studies on formal analysis and verification over suitably reduced state spaces of OOPNs.