Abstract
In this paper we study the model of Time Petri Nets (TPNs) where a time interval is associated with the firing of a transition, but we extend it by considering general intervals rather than closed ones. A key feature of timed models is the memory policy, i.e. which timing informations are kept when a transition is fired. The original model selects an intermediate semantics where the transitions disabled after consuming the tokens, as well as the firing transition, are reinitialised. However this semantics is not appropriate for some applications. So we consider here two alternative semantics: the atomic and the persistent atomic ones. First we present relevant patterns of discrete event systems which show the interest of these semantics. Then we compare the expressiveness of the three semantics w.r.t. weak timed bisimilarity, establishing inclusion results in the general case. Furthermore we show that some inclusions are strict with unrestricted intervals even when nets are bounded. Then we focus on bounded TPNs with upper-closed intervals and we prove that the semantics are equivalent. Finally taking into account both the practical and the theoretical issues, we conclude that persistent atomic semantics should be preferred.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
References
Abdulla, P.A., Nylén, A.: Timed Petri nets and BQOs. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol. 2075, pp. 53–72. Springer, Heidelberg (2001)
Ajmone Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. Wiley Series in Parallel Computing. John Wiley and Sons, Chichester (1994) ISBN: 0-471-93059-8
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science B 126, 183–235 (1994)
Aura, T., Lilius, J.: A causal semantics for time Petri nets. Theoretical Computer Science 243(1–2), 409–447 (2000)
Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Transactions on Software Engineering 17(3), 259–273 (1991)
Berthomieu, B., Ribet, P.-O., Vernadat, F.: The tool TINA - Construction of Abstract State Spaces for Petri Nets and Time Petri Nets. International Journal of Production Research 42(14), 2741–2756 (2004)
Berthomieu, B., Vernadat, F.: State class constructions for branching analysis of time Petri nets. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 442–457. Springer, Heidelberg (2003)
Cassez, F., Roux, O.H.: Structural Translation of Time Petri Nets into Timed Automata. In: Huth, M. (ed.) Workshop on Automated Verification of Critical Systems (AVoCS 2004). Electronic Notes in Computer Science, August 2004. Elsevier, Amsterdam (2004)
de Frutos Escrig, D., Ruiz, V.V., Marroquín Alonso, O.: Decidability of properties of timed-arc Petri nets. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 187–206. Springer, Heidelberg (2000)
Diaz, M., Senac, P.: Time stream Petri nets: a model for timed multimedia information. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol. 815, pp. 219–238. Springer, Heidelberg (1994)
Gardey, G., Lime, D., Roux, O.(H.): Roméo: A tool for Time Petri Nets Analysis (2003), The tool can be freely downloaded from www.irccyn.ec-nantes.fr/irccyn/d/fr/equipes/TempsReel/logs
Khansa, W., Denat, J.P., Collart-Dutilleul, S.: P-Time Petri Nets for manufacturing systems. In: WODES 1996, Scotland, pp. 94–102 (1996)
Lilius, J.: Efficient state space search for time Petri nets. Electronic Notes in Theoretical Computer Science 18 (1999)
Lime, D., Roux, O.H.: State class timed automaton of a time Petri net. In: PNPM 2003, September 2003. IEEE Computer Society Press, Los Alamitos (2003)
Merlin, P.M.: A study of the recoverability of computing systems. PhD thesis, University of California, Irvine, CA (1974)
Popova, L.: On time Petri nets. Journal Information Processing and Cybernetics, EIK 27(4), 227–244 (1991)
Ramchandani, C.: Analysis of asynchronous concurrent systems by timed Petri nets. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA (1974)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bérard, B., Cassez, F., Haddad, S., Lime, D., Roux, O.H. (2005). Comparison of Different Semantics for Time Petri Nets. In: Peled, D.A., Tsay, YK. (eds) Automated Technology for Verification and Analysis. ATVA 2005. Lecture Notes in Computer Science, vol 3707. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11562948_23
Download citation
DOI: https://doi.org/10.1007/11562948_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-29209-8
Online ISBN: 978-3-540-31969-6
eBook Packages: Computer ScienceComputer Science (R0)