Abstract
We present a practically appealing extension of the probabilistic model checker PRISM rendering it to handle fixed-delay continuous-time Markov chains (fdCTMCs) with rewards, the equivalent formalism to the deterministic and stochastic Petri nets (DSPNs). fdCTMCs allow transitions with fixed-delays (or timeouts) on top of the traditional transitions with exponential rates. Our extension supports an evaluation of expected reward until reaching a given set of target states. The main contribution is that, considering the fixed-delays as parameters, we implemented a synthesis algorithm that computes the epsilon-optimal values of the fixed-delays minimizing the expected reward. We provide a performance evaluation of the synthesis on practical examples.
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
Similar content being viewed by others
Notes
- 1.
- 2.
- 3.
For the sake of simplicity, when multiple events \(X = \{e_1,\ldots ,e_n\}\) occur simultaneously, the successor is determined by the minimal element of X according to some fixed total order on \(F\).
- 4.
Computed for the rejuv model and the error bound 0.001, see Sect. 5.
References
Brázdil, T., Korenčiak, Ľ., Krčál, J., Novotný, P., Řehák, V.: Optimizing Performance of Continuous-Time Stochastic Systems Using Timeout Synthesis. In: Campos, J., Haverkort, B.R. (eds.) QEST 2015. LNCS, vol. 9259, pp. 141–159. Springer, Heidelberg (2015)
Fackrell, M.: Fitting with matrix-exponential distributions. Stoch. Models 21(2–3), 377–400 (2005)
German, R.: Performance Analysis of Communication Systems with Non-markovian Stochastic Petri Nets. Wiley, New York (2000)
Guet, C.C., Gupta, A., Henzinger, T.A., Mateescu, M., Sezgin, A.: Delayed continuous-time Markov chains for genetic regulatory circuits. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 294–309. Springer, Heidelberg (2012)
Haddad, S., Mokdad, L., Moreaux, P.: A new approach to the evaluation of non Markovian stochastic Petri nets. In: Donatelli, S., Thiagarajan, P.S. (eds.) ICATPN 2006. LNCS, vol. 4024, pp. 221–240. Springer, Heidelberg (2006)
Horváth, A., Paolieri, M., Ridi, L., Vicario, E.: Transient analysis of non-Markovian models using stochastic state classes. Perform. Eval. 69(7–8), 315–335 (2012)
Korenčiak, Ľ., Krčál, J., Řehák, V.: Dealing with zero density using piecewise phase-type approximation. In: Horváth, A., Wolter, K. (eds.) EPEW 2014. LNCS, vol. 8721, pp. 119–134. Springer, Heidelberg (2014)
Korenčiak, Ľ., Řehák, V., Farmadin, A.: Extension of PRISM by synthesis of optimal timeouts in fdCTMC. CoRR abs/1603.03252 (2016)
Krčál, J.: Formal analysis of discrete-event systems with hard real-time bounds. Ph.D. thesis, Faculty of Informatics, Masaryk University, Brno (2014)
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)
Lindemann, C.: An improved numerical algorithm for calculating steady-state solutions of deterministic and stochastic Petri net models. Perform. Eval. 18(1), 79–95 (1993)
Neuts, M.: Matrix-Geometric Solutions in Stochastic Models: An Algorithmic Approach. The Johns Hopkins University Press, Baltimore (1981)
Puterman, M.: Markov Decision Processes. Wiley, New York (1994)
Qiu, Q., Wu, Q., Pedram, M.: Stochastic modeling of a power-managed system: construction and optimization. In: ISLPED, pp. 194–199. ACM Press (1999)
Xie, W., Sun, H., Cao, Y., Trivedi, K.S.: Optimal webserver session timeout settings for web users. In: Computer Measurement Group Conferenceries, pp. 799–820 (2002)
Zimmermann, A.: Applied restart estimation of general reward measures. In: RESIM, pp. 196–204 (2006)
Zimmermann, A.: Modeling and evaluation of stochastic Petri nets with TimeNET 4.1. In: ICST, pp. 54–63. IEEE (2012)
Acknowledgments
We thank Vojtěch Forejt and David Parker for fruitful discussions. This work is partly supported by the Czech Science Foundation, grant No. P202/12/G061.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Korenčiak, Ľ., Řehák, V., Farmadin, A. (2016). Extension of PRISM by Synthesis of Optimal Timeouts in Fixed-Delay CTMC. In: Ábrahám, E., Huisman, M. (eds) Integrated Formal Methods. IFM 2016. Lecture Notes in Computer Science(), vol 9681. Springer, Cham. https://doi.org/10.1007/978-3-319-33693-0_9
Download citation
DOI: https://doi.org/10.1007/978-3-319-33693-0_9
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-33692-3
Online ISBN: 978-3-319-33693-0
eBook Packages: Computer ScienceComputer Science (R0)