Abstract
Unfoldings are a well known partial-order semantics of P/T Petri nets that can be applied to various model checking or verification problems. For high-level Petri nets, the so-called symbolic unfolding generalizes this notion. A complete finite prefix of the unfolding of a P/T Petri net contains all information to verify, e.g., reachability of markings. We unite these two concepts and define complete finite prefixes of the symbolic unfolding of high-level Petri nets. For a class of safe high-level Petri nets, we generalize the well-known algorithm by Esparza et al. for constructing small such prefixes. Additionally, we identify a more general class of nets with infinitely many reachable markings, for which an approach with an adapted cut-off criterion extends the complete prefix methodology, in the sense that the original algorithm cannot be applied to the P/T net represented by a high-level net.
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
Abdulla, P.A., Iyer, S.P., Nylén, A.: Unfoldings of unbounded Petri nets. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 495–507. Springer, Heidelberg (2000). https://doi.org/10.1007/10722167_37
Best, E., Grahlmann, B.: Programming Environment based on Petri nets - Documentation and User Guide Version 1.4 (1995). https://uol.de/f/2/dept/informatik/ag/parsys/PEP1.4_man.ps.gz?v=1346500853
Chatain, T.: Symbolic unfoldings of high-level Petri nets and application to supervision of distributed systems, Ph. D. thesis, Universit é de Rennes (2006). https://www.sudoc.fr/246936924
Chatain, T., Fabre, E.: Factorization properties of symbolic unfoldings of colored Petri nets. In: Lilius, J., Penczek, W. (eds.) PETRI NETS 2010. LNCS, vol. 6128, pp. 165–184. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-13675-7_11
Chatain, T., Jard, C.: Symbolic diagnosis of partially observable concurrent systems. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 326–342. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-30232-2_21
Chatain, T., Jard, C.: Complete finite prefixes of symbolic unfoldings of safe time Petri nets. In: Donatelli, S., Thiagarajan, P.S. (eds.) ICATPN 2006. LNCS, vol. 4024, pp. 125–145. Springer, Heidelberg (2006). https://doi.org/10.1007/11767589_8
Desel, J., Juhás, G., Neumair, C.: Finite unfoldings of unbounded Petri nets. In: Cortadella, J., Reisig, W. (eds.) ICATPN 2004. LNCS, vol. 3099, pp. 157–176. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-27793-4_10
Ehrig, H., Hoffmann, K., Padberg, J., Baldan, P., Heckel, R.: High-level net processes. In: Brauer, W., Ehrig, H., Karhumäki, J., Salomaa, A. (eds.) Formal and Natural Computing. LNCS, vol. 2300, pp. 191–219. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45711-9_12
Engelfriet, J.: Branching processes of Petri nets. Acta Informatica 28(6), 575–591 (1991). https://doi.org/10.1007/BF01463946
Esparza, J., Römer, S., Vogler, W.: An improvement of McMillan’s unfolding algorithm. Formal Methods Syst. Des. 20(3), 285–310 (2002). https://doi.org/10.1023/A:1014746130920
Herbreteau, F., Sutre, G., Tran, T.Q.: Unfolding concurrent well-structured transition systems. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 706–720. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71209-1_55
Jensen, K.: Coloured Petri nets - basic concepts, analysis methods and practical use - volume 1, Second Edition. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (1996). https://doi.org/10.1007/978-3-662-03241-1
Khomenko, V., Koutny, M.: Branching processes of high-level Petri nets. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 458–472. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-36577-X_34
McMillan, K.L.: A technique of state space search based on unfolding. Formal Methods Syst. Des. 6(1), 45–65 (1995). https://doi.org/10.1007/BF01384314
Nielsen, M., Plotkin, G.D., Winskel, G.: Petri nets, event structures and domains, part I. Theor. Comput. Sci. 13, 85–108 (1981). https://doi.org/10.1016/0304-3975(81)90112-2
Presburger, M.: über die Vollständigkeit eines gewissen Systems der Arithmetik ganzer Zahlen, in welchem die Addition als einzige Operation hervortritt. In: Proc. Comptes-rendus du I Congrés des Mathématiciens des Pays Slaves, Varsovie 1929, pp. 92–101 (1930)
Reisig, W.: Understanding petri nets - modeling techniques, analysis methods, case studies. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-33278-4
Würdemann, N., Chatain, T., Haar, S.: Taking complete finite prefixes to high level, symbolically (Full Version) (2023). https://hal.inria.fr/hal-04029490
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Würdemann, N., Chatain, T., Haar, S. (2023). Taking Complete Finite Prefixes to High Level, Symbolically. In: Gomes, L., Lorenz, R. (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2023. Lecture Notes in Computer Science, vol 13929. Springer, Cham. https://doi.org/10.1007/978-3-031-33620-1_7
Download citation
DOI: https://doi.org/10.1007/978-3-031-33620-1_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-33619-5
Online ISBN: 978-3-031-33620-1
eBook Packages: Computer ScienceComputer Science (R0)