Abstract
Time Petri nets have proved their interest in modeling real-time concurrent systems. Their usual semantics is defined in term of firing sequences, which can be coded in a (symbolic and global) state graph, computable from a bounded net. An alternative is to consider a “partial order” semantics given in term of processes, which keep explicit the notions of causality and concurrency without computing arbitrary interleavings. In ordinary place/transition bounded nets, it has been shown for many years that the whole set of processes can be finitely represented by a prefix of what is called the “unfolding”. This paper defines such a prefix for safe time Petri nets. It is based on a symbolic unfolding of the net, using a notion of “partial state”.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Kitai, T., Oguro, Y., Yoneda, T., Mercer, E., Myers, C.: Partial order reduction for timed circuit verification based on a level oriented model. IEICE Trans. E86-D(12), 2601–2611 (2001)
Penczek, W., Pólrola, A.: Abstractions and partial order reductions for checking branching properties of time Petri nets. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol. 2075, pp. 323–342. Springer, Heidelberg (2001)
Chatain, T., Jard, C.: Time Supervision of Concurrent Systems Using Symbolic Unfoldings of Time Petri Nets. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 196–210. Springer, Heidelberg (2005); Extended version available in INRIA Research Report RR-5706
Aura, T., Lilius, J.: Time processes for time Petri nets. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 136–155. Springer, Heidelberg (1997)
Lilius, J.: Efficient state space search for time Petri nets. In: MFCS Workshop on Concurrency 1998. ENTCS, vol. 18. Elsevier, Amsterdam (1999)
McMillan, K.L.: A technique of state space search based on unfolding. Formal Methods in System Design 6(1), 45–65 (1995)
Esparza, J., Römer, S., Vogler, W.: An improvement of McMillan’s unfolding algorithm. Formal Methods in System Design 20(3), 285–310 (2002)
Bieber, B., Fleischhack, H.: Model checking of time Petri nets based on partial order semantics. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 210–225. Springer, Heidelberg (1999)
Fleischhack, H., Stehno, C.: Computing a finite prefix of a time Petri net. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 163–181. Springer, Heidelberg (2002)
Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. Software Eng. 17(3), 259–273 (1991)
Semenov, A.L., Yakovlev, A.: Verification of asynchronous circuits using time Petri net unfolding. In: DAC, pp. 59–62. ACM Press, New York (1996)
Merlin, P., Farber, D.: Recoverability of communication protocols – implications of a theorical study. IEEE Transactions on Communications 24 (1976)
Engelfriet, J.: Branching processes of Petri nets. Acta Inf. 28(6), 575–591 (1991)
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)
Best, E.: Structure theory of Petri nets: the free choice hiatus. In: Proceedings of an Advanced Course on Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986-Part I, London, UK, pp. 168–205. Springer, Heidelberg (1987)
Baldan, P., Corradini, A., Montanari, U.: Contextual Petri nets, asymmetric event structures, and processes. Inf. Comput. 171(1), 1–49 (2001)
Vogler, W., Semenov, A.L., Yakovlev, A.: Unfolding and finite prefix for nets with read arcs. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 501–516. Springer, Heidelberg (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chatain, T., Jard, C. (2006). Complete Finite Prefixes of Symbolic Unfoldings of Safe Time Petri Nets. In: Donatelli, S., Thiagarajan, P.S. (eds) Petri Nets and Other Models of Concurrency - ICATPN 2006. ICATPN 2006. Lecture Notes in Computer Science, vol 4024. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11767589_8
Download citation
DOI: https://doi.org/10.1007/11767589_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-34699-9
Online ISBN: 978-3-540-34700-2
eBook Packages: Computer ScienceComputer Science (R0)