Abstract
In this paper we discuss several approaches to time in Petri nets. If time is considered for performance analysis, probability distributions for choices should be included into the model and thus we need Petri nets with time and stochastics. In literature, most attention is paid to models where the time is expressed by delaying transitions and for the stochastic case to continuous time models with exponential enabling distributions, known by its software tools as GSPN. Here we focus on discrete models where the time is expressed by delaying tokens and the probability distributions are discrete, because this model class has some advantages. We show how model checking methods can be applied for the non-stochastic case. For the stochastic case we show how Markov techniques can be used. We also consider structural analysis techniques, which do not need the state space.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
van der Aalst, W.M.P., van Hee, K.M., Reijers, H.A.: Analysis of discrete-time stochastic Petri nets. Statistica Neerlandica 54(2), 237–255 (2000)
van der Aalst, W.M.P.: Interval Timed Coloured Petri Nets and their Analysis. PhD thesis, Eindhoven University of Technology (1993)
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–70. Springer, Heidelberg (2001)
Marsan, M.A., Conte, G., Balbo, G.: A class of generalized stochastic Petri nets for the performance evaluation of multiprocessor systems. ACM Trans. Comput. Syst. 2(2), 93–122 (1984)
Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
Bengtsson, J., Larsen, K.G., Larsson, F., Pettersson, P., Yi, W.: Uppaal - a tool suite for automatic verification of real-time systems. In: Alur, R., Sontag, E.D., Henzinger, T.A. (eds.) HS 1995. LNCS, vol. 1066, pp. 232–243. Springer, Heidelberg (1996)
Bera, D., van Hee, K.M., Sidorova, N.: Discrete timed Petri nets. Computer Science Report 13-03, Technische Universiteit Eindhoven, P.O. Box 513, 5600 MB Eindhoven, The Netherlands (April 2013)
Berthelot, G., Boucheneb, H.: Occurrence graphs for interval timed coloured nets. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol. 815, pp. 79–98. Springer, Heidelberg (1994)
Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. Softw. Eng. 17(3), 259–273 (1991)
Berthomieu, B., Menasche, M.: An enumerative approach for analyzing time Petri nets. In: Proceedings IFIP, pp. 41–46. Elsevier Science Publishers (1983)
Boucheneb, H.: Interval timed coloured Petri net: efficient construction of its state class space preserving linear properties. Form. Asp. Comput. 20(2), 225–238 (2008)
Bouyer, P., Haddad, S., Reynier, P.-A.: Undecidability results for timed automata with silent transitions. Fundam. Inf. 92(1-2), 1–25 (2009)
Boyer, M., Roux, O.H.: On the compared expressiveness of arc, place and transition time Petri nets. Fundam. Inf. 88(3), 225–249 (2008)
Cassez, F., Roux, O.-H.: Structural translation from time Petri nets to timed automata. Electron. Notes Theor. Comput. Sci. 128(6), 145–160 (2005)
Cerone, A., Maggiolio-Schettini, A.: Time-based expressivity of timed Petri nets for system specification. Theor. Comput. Sci. 216(1-2), 1–53 (1999)
Ghezzi, C., Mandrioli, D., Morasca, S., Pezze, M.: A unified high-level Petri net formalism for time-critical systems. IEEE Trans. Softw. Eng. 17(2), 160–172 (1991)
van Glabbeek, R.: The linear time-branching time spectrum. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 278–297. Springer, Heidelberg (1990)
Haddad, S., Moreaux, P.: Sub-stochastic matrix analysis for bounds computation - theoretical results. European Journal of Operational Research 176(2), 999–1015 (2007)
van Hee, K.M., Somers, L.J., Voorhoeve, M.: Executable specifications for distributed information systems. In: Proceedings of the IFIP TC 8/WG 8.1, pp. 139–156. Elsevier (1989)
Jantzen, M.: Language theory of Petri nets. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 254, pp. 397–412. Springer, Heidelberg (1987)
Jensen, K.: An introduction to the theoretical aspects of coloured Petri nets. In: de Bakker, J.W., de Roever, W.-P., Rozenberg, G. (eds.) REX 1993. LNCS, vol. 803, pp. 230–272. Springer, Heidelberg (1994)
Knapik, M., Penczek, W., Szreter, M., Polrola, A.: Bounded parametric verification for distributed time Petri nets with discrete-time semantics. Fundam. Inf. 101(1-2), 9–27 (2010)
Christensen, S., Kristensen, L.M., Mailund, T.: Condensed state spaces for timed petri nets. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol. 2075, pp. 101–120. Springer, Heidelberg (2001)
Lime, D., Roux, O.H.: Model checking of time Petri nets using the state class timed automaton. Discrete Event Dynamic Systems 16(2), 179–205 (2006)
Lime, D., Roux, O.H.: Model checking of time Petri nets using the state class timed automaton. Discrete Event Dynamic Systems 16(2), 179–205 (2006)
Ajmone Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with generalized stochastic Petri nets. SIGMETRICS Perform. Eval. Rev. 26(2) (August 1998)
Merlin, P.M., Farber, D.J.: Recoverability of communication protocols: Implications of a theoretical study. IEEE Trans. Comm. (September 1976)
Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, SFCS 1977, pp. 46–57. IEEE Computer Society, Washington, DC (1977)
Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming, 1st edn. John Wiley and Sons, Inc., New York (1994)
Ramachandani, C.: Analysis of asynchronous concurrent systems by timed Petri nets. PhD thesis, Massachusetts Institute of Tenchnology, Cambridge, MA (1974)
Ramamoorthy, C.V., Ho, G.S.: Performance evaluation of asynchronous concurrent systems using Petri nets. IEEE Transactions on Software Engineering 6(5), 440–449 (1980)
Recalde, L., Haddad, S., Silva, M.: Continuous Petri nets: Expressive power and decidability issues. Int. J. Found. Comput. Sci. 21(2), 235–256 (2010)
Ross, S.M.: Introduction to Probability Models, 9th edn. Academic Press, Inc., Orlando (2006)
Valero Ruiz, V., de Frutos Escrig, D., Cuartero Gomez, F.: On non-decidability of reachability for timed-arc Petri nets. In: Proc. 8th. International Workshop on Petri Nets and Performance Models, pp. 188–196 (1999)
Sifakis, J.: Use of Petri nets for performance evaluation. In: Proceedings of the Third International Symposium on Measuring, Modelling and Evaluating Computer Systems, Bonn - Bad Godesberg, Germany, October 3-5, pp. 75–93. North-Holland (1977)
Starke, P.H.: Some properties of timed nets under the earliest firing rule. In: Rozenberg, G. (ed.) APN 1989. LNCS, vol. 424, pp. 418–432. Springer, Heidelberg (1990)
CPN website, http://www.cpntools.org/
ExSpecT website, http://www.exspect.com/
Great SPN website, http://www.di.unito.it/~greatspn/index.html
UPPAAL website, http://www.uppaal.org/
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
van Hee, K., Sidorova, N. (2013). The Right Timing: Reflections on the Modeling and Analysis of Time. In: Colom, JM., Desel, J. (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2013. Lecture Notes in Computer Science, vol 7927. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-38697-8_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-38697-8_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-38696-1
Online ISBN: 978-3-642-38697-8
eBook Packages: Computer ScienceComputer Science (R0)