Abstract
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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Buchholz, P., Kemper, P.: Efficient computation and representation of large reachability sets for composed automata. Discret. Event Dyn. Syst. 12(3), 265–286 (2002). https://doi.org/10.1023/A:1015669415634
Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 1020 states and beyond. Inf. Comput. 98(2), 142–170 (1992)
Christensen, S., Petrucci, L.: Modular analysis of Petri nets. Comput. J. 43(3), 224–242 (2000). https://doi.org/10.1093/comjnl/43.3.224
Garavel, H., Lang, F., Mounier, L.: Compositional verification in action. In: Howar, F., Barnat, J. (eds.) FMICS 2018. LNCS, vol. 11119, pp. 189–210. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-00244-2_13
Graf, S., Steffen, B.: Compositional minimization of finite state systems. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 186–196. Springer, Heidelberg (1991). https://doi.org/10.1007/BFb0023732
Latvala, T., Mäkelä, M.: LTL model checking for modular Petri nets. In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol. 3099, pp. 298–311. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27793-4_17
Le Cornec, Y.S.: Compositional analysis of modular Petri nets using hierarchical state space abstraction. In: Joint 5th International Workshop on Logics, Agents, and Mobility, LAM 2012, The 1st International Workshop on Petri Net-Based Security, WooPS 2012 and the 2nd International Workshop on Petri Nets Compositions, CompoNet 2012. CEUR Workshop Proceedings, Hamburg, Germany, vol. 853, pp. 119–133, June 2012
Miner, A.S., Ciardo, G.: Efficient reachability set generation and storage using decision diagrams. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol. 1639, pp. 6–25. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48745-X_2
Schmidt, K.: How to calculate symmetries of petri nets. Acta Inform. 36(7), 545–590 (2000). https://doi.org/10.1007/S002360050002
Schmidt, K.: LoLA a low level analyser. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 465–474. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-44988-4_27
Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) ICATPN 1989. LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1991). https://doi.org/10.1007/3-540-53863-1_36
Valmari, A.: Compositional analysis with place-bordered subnets. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol. 815, pp. 531–547. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58152-9_29
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2024 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Gaede, J., Wallner, S., Wolf, K. (2024). Modular State Spaces - A New Perspective. In: Kristensen, L.M., van der Werf, J.M. (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2024. Lecture Notes in Computer Science, vol 14628. Springer, Cham. https://doi.org/10.1007/978-3-031-61433-0_15
Download citation
DOI: https://doi.org/10.1007/978-3-031-61433-0_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-61432-3
Online ISBN: 978-3-031-61433-0
eBook Packages: Computer ScienceComputer Science (R0)