Verifying Temporal Logic Properties in the Modular State Space

A modular Petri net is composed of multiple individual Petri nets, the modules, by fusing their interface transitions. Internal transitions are not related to other modules. Their behavior is recorded in local reachability graphs for each module. The behavior of interface transitions is recorded in a single synchronization graph, linking the local reachability graphs together to form the modular state space. Our notion of modular state spaces is similar to previous proposals [5, 6, 17] but drops a few assumptions for the sake of additional compression. In this paper, we study the verification of temporal logic properties using the modular state space. For linear time properties, we re-establish a result from [10] for our revised concepts. In our proof, we use completely different arguments and generalize the result to non-regular linear time properties. Modular state spaces do not easily permit the verification of branching time properties and there is no existing result on this matter. We demonstrate, however, that CTL properties can very well be verified after applying a certain refinement to the modular state space.