{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,20]],"date-time":"2025-07-20T03:52:49Z","timestamp":1752983569683},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642401954"},{"type":"electronic","value":"9783642401961"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40196-1_30","type":"book-chapter","created":{"date-parts":[[2013,7,22]],"date-time":"2013-07-22T21:54:56Z","timestamp":1374530096000},"page":"355-371","source":"Crossref","is-referenced-by-count":15,"title":["Transient Analysis of Networks of Stochastic Timed Automata Using Stochastic State Classes"],"prefix":"10.1007","author":[{"given":"Paolo","family":"Ballarini","sequence":"first","affiliation":[]},{"given":"Nathalie","family":"Bertrand","sequence":"additional","affiliation":[]},{"given":"Andr\u00e1s","family":"Horv\u00e1th","sequence":"additional","affiliation":[]},{"given":"Marco","family":"Paolieri","sequence":"additional","affiliation":[]},{"given":"Enrico","family":"Vicario","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"30_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/11730637_5","volume-title":"Hybrid Systems: Computation and Control","author":"R. Alur","year":"2006","unstructured":"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.\u00a03927, pp. 19\u201333. Springer, Heidelberg (2006)"},{"key":"30_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/3-540-54233-7_128","volume-title":"Automata, Languages and Programming","author":"R. Alur","year":"1991","unstructured":"Alur, R., Courcoubetis, C., Dill, D.: Model-checking for Probabilistic Real-time Systems. In: Leach Albert, J., Monien, B., Rodr\u00edguez-Artalejo, M. (eds.) ICALP 1991. LNCS, vol.\u00a0510, pp. 115\u2013126. Springer, Heidelberg (1991)"},{"key":"30_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/BFb0031986","volume-title":"Real-Time: Theory in Practice","author":"R. Alur","year":"1992","unstructured":"Alur, R., Courcoubetis, C., Dill, D.L.: 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.\u00a0600, pp. 28\u201344. Springer, Heidelberg (1992)"},{"issue":"2","key":"30_CR4","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1016\/0304-3975(94)90010-8","volume":"126","author":"R. Alur","year":"1994","unstructured":"Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci.\u00a0126(2), 183\u2013235 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"30_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1007\/978-3-540-77050-3_15","volume-title":"FSTTCS 2007","author":"C. Baier","year":"2007","unstructured":"Baier, C., Bertrand, N., Bouyer, P., Brihaye, T., Gr\u00f6\u00dfer, M.: Probabilistic and topological semantics for timed automata. In: Arvind, V., Prasad, S. (eds.) FSTTCS 2007. LNCS, vol.\u00a04855, pp. 179\u2013191. Springer, Heidelberg (2007)"},{"key":"30_CR6","doi-asserted-by":"crossref","unstructured":"Baier, C., Bertrand, N., Bouyer, P., Brihaye, T., Gr\u00f6\u00dfer, M.: Almost-sure model checking of infinite paths in one-clock timed automata. In: LICS 2008, pp. 217\u2013226. IEEE CS (2008)","DOI":"10.1109\/LICS.2008.25"},{"key":"30_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/3-540-48683-6_30","volume-title":"Computer Aided Verification","author":"G. Behrmann","year":"1999","unstructured":"Behrmann, G., Larsen, K.G., Pearson, J., Weise, C., Yi, W.: Efficient timed reachability analysis using clock difference diagrams. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 341\u2013353. Springer, Heidelberg (1999)"},{"key":"30_CR8","doi-asserted-by":"crossref","unstructured":"Bertrand, N., Bouyer, P., Brihaye, T., Markey, N.: Quantitative model-checking of one-clock timed automata under probabilistic semantics. In: QEST 2008, pp. 55\u201364. IEEE CS (2008)","DOI":"10.1109\/QEST.2008.19"},{"key":"30_CR9","unstructured":"Bobbio, A., Telek, M.: Markov regenerative SPN with non-overlapping activity cycles. In: IPDS 1995, pp. 124\u2013133. IEEE CS (1995)"},{"key":"30_CR10","doi-asserted-by":"crossref","unstructured":"Bouyer, P., Brihaye, T., Jurdzinski, M., Menet, Q.: Almost-sure model-checking of reactive timed automata. In: QEST 2012, pp. 138\u2013147. IEEE CS (2012)","DOI":"10.1109\/QEST.2012.10"},{"issue":"5","key":"30_CR11","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1007\/s10009-010-0156-8","volume":"12","author":"G. Bucci","year":"2010","unstructured":"Bucci, G., Carnevali, L., Ridi, L., Vicario, E.: Oris: a tool for modeling, verification and evaluation of real-time systems. Int. J. on Softw. Tools for Techn. Transfer\u00a012(5), 391\u2013403 (2010)","journal-title":"Int. J. on Softw. Tools for Techn. Transfer"},{"key":"30_CR12","doi-asserted-by":"crossref","unstructured":"Bucci, G., Piovosi, R., Sassoli, L., Vicario, E.: Introducing probability within state class analysis of dense time dependent systems. In: QEST 2005, pp. 13\u201322. IEEE CS (2005)","DOI":"10.1109\/QEST.2005.17"},{"issue":"2","key":"30_CR13","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1109\/TSE.2008.101","volume":"35","author":"L. Carnevali","year":"2009","unstructured":"Carnevali, L., Grassi, L., Vicario, E.: State-density functions over DBM domains in the analysis of non-Markovian models. IEEE Trans. Softw. Eng.\u00a035(2), 178\u2013194 (2009)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"30_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"409","DOI":"10.1007\/978-3-642-24270-0_30","volume-title":"Computer Safety, Reliability, and Security","author":"L. Carnevali","year":"2011","unstructured":"Carnevali, L., Ridi, L., Vicario, E.: A framework for simulation and symbolic state space analysis of non-Markovian models. In: Flammini, F., Bologna, S., Vittorini, V. (eds.) SAFECOMP 2011. LNCS, vol.\u00a06894, pp. 409\u2013422. Springer, Heidelberg (2011)"},{"issue":"7","key":"30_CR15","doi-asserted-by":"publisher","first-page":"506","DOI":"10.1109\/32.297939","volume":"20","author":"G. Ciardo","year":"1994","unstructured":"Ciardo, G., German, R., Lindemann, C.: A characterization of the stochastic process underlying a stochastic Petri net. IEEE Trans. Softw. Eng.\u00a020(7), 506\u2013515 (1994)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"30_CR16","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1017\/S0305004100030437","volume":"51","author":"D.R. Cox","year":"1955","unstructured":"Cox, D.R.: The analysis of non-Markovian stochastic processes by the inclusion of supplementary variables. Math. Proc. Cambridge\u00a051, 433\u2013441 (1955)","journal-title":"Math. Proc. Cambridge"},{"key":"30_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/3-540-52148-8_17","volume-title":"Automatic Verification Methods for Finite State Systems","author":"D.L. Dill","year":"1990","unstructured":"Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Sifakis, J. (ed.) CAV 1989. LNCS, vol.\u00a0407, pp. 197\u2013212. Springer, Heidelberg (1990)"},{"key":"30_CR18","doi-asserted-by":"crossref","unstructured":"Haas, P.J.: Stochastic Petri Nets: Modelling, Stability, Simulation. Springer (2002)","DOI":"10.1007\/b97265"},{"key":"30_CR19","doi-asserted-by":"crossref","unstructured":"Horv\u00e1th, A., Paolieri, M., Ridi, L., Vicario, E.: Probabilistic model checking of non-Markovian models with concurrent generally distributed timers. In: QEST 2011, pp. 131\u2013140. IEEE CS (2011)","DOI":"10.1109\/QEST.2011.23"},{"issue":"7-8","key":"30_CR20","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1016\/j.peva.2011.11.002","volume":"69","author":"A. Horv\u00e1th","year":"2012","unstructured":"Horv\u00e1th, A., Paolieri, M., Ridi, L., Vicario, E.: Transient analysis of non-Markovian models using stochastic state classes. Perform. Eval.\u00a069(7-8), 315\u2013335 (2012)","journal-title":"Perform. Eval."},{"key":"30_CR21","unstructured":"Kulkarni, V.: Modeling and analysis of stochastic systems. Chapman & Hall (1995)"},{"key":"30_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M. Kwiatkowska","year":"2011","unstructured":"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.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"30_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/3-540-44618-4_11","volume-title":"CONCUR 2000 - Concurrency Theory","author":"M. Kwiatkowska","year":"2000","unstructured":"Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Verifying quantitative properties of continuous probabilistic timed automata. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, pp. 123\u2013137. Springer, Heidelberg (2000)"},{"issue":"1","key":"30_CR24","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/S0304-3975(01)00046-9","volume":"282","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Segala, R., Sproston, J.: Automatic verification of real-time systems with discrete probability distributions. Theor. Comput. Sci.\u00a0282(1), 101\u2013150 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"30_CR25","doi-asserted-by":"crossref","unstructured":"Maler, O., Larsen, K.G., Krogh, B.H.: On zone-based analysis of duration probabilistic automata. In: INFINITY, pp. 33\u201346 (2010)","DOI":"10.4204\/EPTCS.39.3"},{"issue":"5","key":"30_CR26","doi-asserted-by":"publisher","first-page":"703","DOI":"10.1109\/TSE.2009.36","volume":"35","author":"E. Vicario","year":"2009","unstructured":"Vicario, E., Sassoli, L., Carnevali, L.: Using stochastic state classes in quantitative evaluation of dense-time reactive systems. IEEE Trans. Softw. Eng.\u00a035(5), 703\u2013719 (2009)","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40196-1_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,15]],"date-time":"2019-05-15T22:49:39Z","timestamp":1557960579000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40196-1_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642401954","9783642401961"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40196-1_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}