Modular State Spaces - A New Perspective

A modular Petri net is built from individual Petri nets, the instances, which have disjoint sets of internal transitions and interface transitions. Whereas internal transitions represent the internal behavior of an instance, interface transitions are used to synchronize behavior between instances. For a modular Petri net, we can use the modular state space as an implicit representation of its reachability graph. This concept has also been examined in [3] and [6]. The modular state space is the entirety of local reachability graphs that present the internal behavior of the instances and a synchronization graph that keeps record of the synchronized behavior. In this paper we present a data structure and a construction algorithm for the modular state space. Our conceptualization is a generalization of the work of [3], and we have emphasized the differences in our approach. Furthermore, we describe how reachability-set-based properties can be verified in the modular state space. For the evaluation of properties, we aggregate information from the local reachability graphs and then combine the aggregated information when inspecting the synchronization graph. This way, we can evaluate deadlock freedom more efficiently and can for the first time propose a method to evaluate the reachability of state predicates. In addition, we emphasize the capability of modular state spaces to cope with modular Petri nets where some modules are structurally equal. In fact, when a module is used in more than one instance, its local reachability graph needs to be represented only once. This leads to a state space reduction that is not fully covered by the exploitation of symmetries.