Skip to main content
SpringerLink
Log in

Probabilistic Time Petri Nets

  • Conference paper
  • First Online:
Application and Theory of Petri Nets and Concurrency (PETRI NETS 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9698))

Abstract

We introduce a new model for the design of concurrent stochastic real-time systems. Probabilistic time Petri nets (PTPN) are an extension of time Petri nets in which the output of tokens is randomised. Such a design allows us to elegantly solve the hard problem of combining probabilities and concurrency. This model further benefits from the concision and expressive power of Petri nets. Furthermore, the usual tools for the analysis of time Petri nets can easily be adapted to our probabilistic setting. More precisely, we show how a Markov decision process (MDP) can be derived from the classic atomic state class graph construction. We then establish that the schedulers of the PTPN and the adversaries of the MDP induce the same Markov chains. As a result, this construction notably preserves the lower and upper bounds on the probability of reaching a given target marking. We also prove that the simpler original state class graph construction cannot be adapted in a similar manner for this purpose.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

References

  1. Stewart, W.J.: Introduction to the Numerical Solutions of Markov Chains. Princeton University Press, Princeton (1994)

    MATH  Google Scholar 

  2. Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, London (1994)

    Book  MATH  Google Scholar 

  3. Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theoret. Comput. Sci. 282(1), 101–150 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  4. Eisentraut, C., Hermanns, H., Zhang, L.: On probabilistic automata in continuous time. In: 25th Annual IEEE Symposium on Logic in Computer Science (LICS), pp. 342–351. IEEE (2010)

    Google Scholar 

  5. Bertrand, N., Bouyer, P., Brihaye, T., Menet, Q., Baier, C., Größer, M., Jurdziński, M.: Stochastic timed automata. Log. Meth. Comput. Sci. 10(4), 6 (2014)

    MathSciNet  MATH  Google Scholar 

  6. Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of deadline properties in the IEEE 1394 FireWire root contention protocol. Formal Aspects of Comput. 14(3), 295–318 (2003)

    Article  MATH  Google Scholar 

  7. Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585–591. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  8. 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)

    Article  Google Scholar 

  9. Molloy, M.K.: Discrete time stochastic Petri nets. IEEE Trans. Softw. Eng. 11(4), 417–423 (1985)

    Article  MathSciNet  MATH  Google Scholar 

  10. Vicario, E., Sassoli, L., Carnevali, L.: Using stochastic state classes in quantitative evaluation of dense-time reactive systems. IEEE Trans. Softw. Eng. 35(5), 703–719 (2009)

    Article  Google Scholar 

  11. Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. Soft. Eng. 3, 259–273 (1991)

    Article  MathSciNet  Google Scholar 

  12. Berthomieu, B., Menasche, M.: An enumerative approach for analyzing time Petri nets: In: Mason, R.E.A. (ed.) Information Processing: Proceedings of the IFIP Congress, vol. 9 of IFIP Congress Series, pp. 41–46 (1983)

    Google Scholar 

  13. Dugan, J.B., Trivedi, K.S., Geist, R.M., Nicola, V.F.: Extended stochastic Petri nets: applications and analysis. Technical report, DTIC Document (1984)

    Google Scholar 

  14. 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)

    Chapter  MATH  Google Scholar 

  15. Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  16. Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Formal Meth. Syst. Des. 43(2), 164–190 (2013)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. UMR CNRS 6597, École Centrale de Nantes, IRCCyN, Nantes, France

    Yrvann Emzivat, Didier Lime & Olivier H. Roux

  2. UMR CNRS 6241, Université de Nantes, LINA, Nantes, France

    Benoît Delahaye

  3. Renault S.A.S., Technocentre Renault, Guyancourt, France

    Yrvann Emzivat

Authors
  1. Yrvann Emzivat
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Benoît Delahaye
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Didier Lime
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Olivier H. Roux
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Yrvann Emzivat .

Editor information

Editors and Affiliations

  1. Université Pierre and Marie Curie, Paris, France

    Fabrice Kordon

  2. Department Informatik, Universität Hamburg Department Informatik, Hamburg, Germany

    Daniel Moldt

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Emzivat, Y., Delahaye, B., Lime, D., Roux, O.H. (2016). Probabilistic Time Petri Nets. In: Kordon, F., Moldt, D. (eds) Application and Theory of Petri Nets and Concurrency. PETRI NETS 2016. Lecture Notes in Computer Science(), vol 9698. Springer, Cham. https://doi.org/10.1007/978-3-319-39086-4_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-39086-4_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-39085-7

  • Online ISBN: 978-3-319-39086-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation