Fixed-delay events in generalized semi-Markov processes revisited. (English) Zbl 1343.68161
Katoen, Joost-Pieter (ed.) et al., CONCUR 2011 – concurrency theory. 22nd international conference, CONCUR 2011, Aachen, Germany, September 6–9, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-23216-9/pbk). Lecture Notes in Computer Science 6901, 140-155 (2011).
Summary: We study long run average behavior of generalized semi-Markov processes with both fixed-delay events as well as variable-delay events. We show that allowing two fixed-delay events and one variable-delay event may cause an unstable behavior of a GSMP. In particular, we show that a frequency of a given state may not be defined for almost all runs (or more generally, an invariant measure may not exist). We use this observation to disprove several results from literature. Next we study GSMP with at most one fixed-delay event combined with an arbitrary number of variable-delay events. We prove that such a GSMP always possesses an invariant measure which means that the frequencies of states are always well defined and we provide algorithms for approximation of these frequencies. Additionally, we show that the positive results remain valid even if we allow an arbitrary number of reasonably restricted fixed-delay events.
For the entire collection see [Zbl 1221.68022].
For the entire collection see [Zbl 1221.68022].
MSC:
| 68Q85 | Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) |
Software:
SMART_References:
| [1] | de Alfaro, L.: How to specify and verify the long-run average behavior of probabilistic systems. In: Proceedings of LICS 1998, pp. 454–465. IEEE Computer Society Press, Los Alamitos (1998) |
| [2] | Alur, R., Bernadsky, M.: Bounded model checking for GSMP models of stochastic real-time systems. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 19–33. Springer, Heidelberg (2006) · Zbl 1178.68332 · doi:10.1007/11730637_5 |
| [3] | Alur, R., Courcoubetis, C., Dill, D.: Model-checking for probabilistic real-time systems. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol. 510, pp. 115–136. Springer, Heidelberg (1991) · Zbl 0769.68088 · doi:10.1007/3-540-54233-7_128 |
| [4] | Alur, R., Courcoubetis, C., Dill, D.: Verifying automata specifications of probabilistic real-time systems. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, Springer, Heidelberg (1992) · Zbl 0769.68088 |
| [5] | Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994) · Zbl 0803.68071 · doi:10.1016/0304-3975(94)90010-8 |
| [6] | Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model-checking algorithms for continuous-time Markov chains. IEEE Transaction on Software Engineering 29(6), 524–541 (2003) · doi:10.1109/TSE.2003.1205180 |
| [7] | Barbot, B., Chen, T., Han, T., Katoen, J.-P., Mereacre, A.: Efficient CTMC model checking of linear real-time objectives. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 128–142. Springer, Heidelberg (2011) · Zbl 1315.68174 · doi:10.1007/978-3-642-19835-9_12 |
| [8] | Bernadsky, M., Alur, R.: Symbolic analysis for GSMP models with one stateful clock. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 90–103. Springer, Heidelberg (2007) · Zbl 1221.93016 · doi:10.1007/978-3-540-71493-4_10 |
| [9] | Brázdil, T., Krčál, J., Křetínský, J., Kučera, A., Řehák, V.: Measuring performance of continuous-time stochastic processes using timed automata. In: Proceedings of 14th International Conference on Hybrid Systems: Computation and Control (HSCC 2011), pp. 33–42, ACM Press, New York (2011) · Zbl 1361.68136 · doi:10.1145/1967701.1967709 |
| [10] | Brázdil, T.: Krčál, J., Křetínský, J., Řehák, V.: Fixed-delay Events in Generalized Semi-Markov Processes Revisited. ArXiv e-prints (September 2011) · Zbl 1343.68161 |
| [11] | Ciardo, G., Jones III, R., Miner, A., Siminiceanu, R.: Logic and stochastic modeling with SMART. Performance Evaluation 63(6), 578–608 (2006) · doi:10.1016/j.peva.2005.06.001 |
| [12] | D’Argenio, P., Katoen, J.: A theory of stochastic systems Part I: Stochastic automata. Information and Computation 203(1), 1–38 (2005) · Zbl 1105.68061 · doi:10.1016/j.ic.2005.07.001 |
| [13] | German, R., Lindemann, C.: Analysis of stochastic Petri nets by the method of supplementary variables. Performance Evaluation 20(1-3), 317–335 (1994) · doi:10.1016/0166-5316(94)90020-5 |
| [14] | Glynn, P.: A GSMP formalism for discrete event systems. Proceedings of the IEEE 77, 14–23 (1989) · doi:10.1109/5.21067 |
| [15] | Haas, P.: On simulation output analysis for generalized semi-markov processes. Commun. Statist. Stochastic Models 15, 53–80 (1999) · Zbl 1126.62306 · doi:10.1080/15326349908807525 |
| [16] | Haas, P.: Stochastic Petri Nets: Modelling, Stability, Simulation. Springer Series in Operations Research and Financial Engineering. Springer, Heidelberg (2010) |
| [17] | Haas, P., Shedler, G.: Regenerative generalized semi-Markov processes. Stochastic Models 3(3), 409–438 (1987) · Zbl 0636.60092 · doi:10.1080/15326348708807064 |
| [18] | Lindemann, C., Reuys, A., Thummler, A.: The DSPNexpress 2.000 performance and dependability modeling environment. In: Twenty-Ninth Annual International Symposium on Fault-Tolerant Computing, Digest of Papers, pp. 228–231. IEEE Computer Society Press, Los Alamitos (1999) · doi:10.1109/FTCS.1999.781055 |
| [19] | Lindemann, C., Shedler, G.: Numerical analysis of deterministic and stochastic Petri nets with concurrent deterministic transitions. Performance Evaluation 27, 565–582 (1996) · Zbl 0875.68666 · doi:10.1016/S0166-5316(96)90046-2 |
| [20] | López, G., Hermanns, H., Katoen, J.: Beyond memoryless distributions: Model checking semi-markov chains. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol. 2165, pp. 57–70. Springer, Heidelberg (2001) · Zbl 1007.68514 · doi:10.1007/3-540-44804-7_4 |
| [21] | Marsan, M., Chiola, G.: On Petri nets with deterministic and exponentially distributed firing times. In: Rozenberg, G. (ed.) APN 1987. LNCS, vol. 266, pp. 132–145. Springer, Heidelberg (1987) · doi:10.1007/3-540-18086-9_23 |
| [22] | Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. Wiley, Chichester (1995) · Zbl 0843.68080 |
| [23] | Matthes, K.: Zur Theorie der Bedienungsprozesse. In: Transactions of the Third Prague Conference on Information Theory, Statistical Decision Functions, Random Processes, pp. 513–528 (1962) |
| [24] | Meyn, S., Tweedie, R.: Markov Chains and Stochastic Stability. Cambridge University Press, Cambridge (2009) · Zbl 1165.60001 · doi:10.1017/CBO9780511626630 |
| [25] | Roberts, G., Rosenthal, J.: General state space Markov chains and MCMC algorithms. Probability Surveys 1, 20–71 (2004) · Zbl 1189.60131 · doi:10.1214/154957804100000024 |
| [26] | Younes, H., Simmons, R.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, p. 223–235. Springer, Heidelberg (2002) · Zbl 1010.68513 · doi:10.1007/3-540-45657-0_17 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
