{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T12:01:00Z","timestamp":1742385660511},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540331025"},{"type":"electronic","value":"9783540331032"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11691617_6","type":"book-chapter","created":{"date-parts":[[2006,3,28]],"date-time":"2006-03-28T09:14:13Z","timestamp":1143537253000},"page":"89-107","source":"Crossref","is-referenced-by-count":4,"title":["Symbolic Model Checking of Stochastic Systems: Theory and Implementation"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Kuntz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Markus","family":"Siegle","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"6_CR1","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1145\/190.191","volume":"2","author":"M. Ajmone Marsan","year":"1984","unstructured":"Ajmone Marsan, M., Balbo, G., Conte, G.: A Class of Generalized Stochastic Petri Nets for the Performance Evaluation of Multiprocessor Systems. ACM Transactions on Computer Systems\u00a02(2), 93\u2013122 (1984)","journal-title":"ACM Transactions on Computer Systems"},{"key":"6_CR2","volume-title":"Modelling with Generalized Stochastic Petri Nets","author":"M. Ajmone Marsan","year":"1995","unstructured":"Ajmone Marsan, M., Balbo, G., Conte, G., Donatelli, S., Franceschinis, G.: Modelling with Generalized Stochastic Petri Nets. Wiley, Chichester (1995)"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/3-540-61474-5_75","volume-title":"Computer Aided Verification","author":"A. Aziz","year":"1996","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Verifying continuous time Markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 146\u2013162. Springer, Heidelberg (1996)"},{"key":"6_CR4","first-page":"701","volume-title":"Int. Conf. on Dependable Systems and Networks: Performance and Dependability Symposium","author":"C. Baier","year":"2004","unstructured":"Baier, C., Cloth, L., Haverkort, B., Kuntz, M., Siegle, M.: Model Checking Actionand State-labelled Markov Chains. In: Int. Conf. on Dependable Systems and Networks: Performance and Dependability Symposium, pp. 701\u2013710. IEEE Computer Society Press, Los Alamitos (2004)"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"780","DOI":"10.1007\/3-540-45022-X_65","volume-title":"Automata, Languages and Programming","author":"C. Baier","year":"2000","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: On the logical characterization of performability properties. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol.\u00a01853, pp. 780\u2013792. Springer, Heidelberg (2000)"},{"issue":"7","key":"6_CR6","first-page":"1","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.P.: Model-Checking Algorithms for Continuous-Time Markov Chains. IEEE Trans. Software Eng.\u00a029(7), 1\u201318 (2003)","journal-title":"IEEE Trans. Software Eng."},{"key":"6_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"CONCUR\u201999. Concurrency Theory","author":"C. Baier","year":"1999","unstructured":"Baier, C., Katoen, J.-P., Hermanns, H.: Approximate Symbolic Model Checking of Continuous-Time Markov Chains. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 146\u2013162. Springer, Heidelberg (1999)"},{"key":"6_CR8","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/S0304-3975(97)00127-8","volume":"202","author":"M. Bernardo","year":"1998","unstructured":"Bernardo, M., Gorrieri, R.: A Tutorial on EMPA: A Theory of Concurrent Processes with Nondeterminism, Priorities, Probabilities and Time. Theoretical Computer Science\u00a0202, 1\u201354 (1998)","journal-title":"Theoretical Computer Science"},{"key":"6_CR9","unstructured":"Ciardo, G., Tilgner, M.: On the use of Kronecker operators for the solution of generalized stochastic Petri nets. Technical Report 96-35, ICASE (1996)"},{"issue":"10","key":"6_CR10","doi-asserted-by":"publisher","first-page":"956","DOI":"10.1109\/TSE.2002.1041052","volume":"28","author":"D. Deavours","year":"2002","unstructured":"Deavours, D., Clark, G., Courtney, T., Daly, D., Derisavi, S., Doyle, J., Sanders, W.H., Webster, P.: The Moebius Framework and its Implementation. IEEE Transactions on Software Engineering\u00a028(10), 956\u2013969 (2002)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"6_CR11","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M. Fischer","year":"1979","unstructured":"Fischer, M., Ladner, R.: Propositional dynamic logic of regular programs. J. Comput. System Sci.\u00a018, 194\u2013211 (1979)","journal-title":"J. Comput. System Sci."},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Interactive Markov Chains","year":"2002","unstructured":"Hermanns, H. (ed.): Interactive Markov Chains. LNCS, vol.\u00a02428. Springer, Heidelberg (2002)"},{"issue":"1-4","key":"6_CR13","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/S0166-5316(99)00056-5","volume":"39","author":"H. Hermanns","year":"2000","unstructured":"Hermanns, H., Herzog, U., Klehmet, U., Mertsiotakis, V., Siegle, M.: Compositional performance modelling with the TIPPtool. Performance Evaluation\u00a039(1-4), 5\u201335 (2000)","journal-title":"Performance Evaluation"},{"key":"6_CR14","unstructured":"Hermanns, H., Katoen, J.-P., Meyer-Kayser, J., Siegle, M.: Implementing a Model Checker for Performability Behaviour. In: Proc. Fifth Int. Workshop on Performability Modeling of Computer and Communication Systems (PMCCS-5), Erlangen, Germany, pp. 110\u2013115 (2001)"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/3-540-40911-4_24","volume-title":"Integrated Formal Methods","author":"H. Hermanns","year":"2000","unstructured":"Hermanns, H., Katoen, J.P., Meyer-Kayser, J., Siegle, M.: Towards model checking stochastic process algebra. In: Grieskamp, W., Santen, T., Stoddart, B. (eds.) IFM 2000. LNCS, vol.\u00a01945, pp. 420\u2013439. Springer, Heidelberg (2000)"},{"key":"6_CR16","unstructured":"Kuntz, M.: Symbolic Semantics and Verification of Stochastic Process Algebras. PhD thesis, Universit\u00e4t Erlangen-N\u00fcrnberg, Institut f\u00fcr Informatik 7 (2006) (to appear)"},{"key":"6_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/3-540-45605-8_12","volume-title":"Process Algebra and Probabilistic Methods. Performance Modeling and Verification","author":"M. Kuntz","year":"2002","unstructured":"Kuntz, M., Siegle, M.: Deriving symbolic representations from stochastic process algebras. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol.\u00a02399, pp. 188\u2013206. Springer, Heidelberg (2002)"},{"key":"6_CR18","unstructured":"Kuntz, M., Siegle, M.: A Stochastic Extension of the Logic PDL. In: Sixth Int. Workshop on Performability Modeling of Computer and Communication Systems (PMCCS-6), pp. 58\u201361 (2003)"},{"key":"6_CR19","unstructured":"Kuntz, M., Siegle, M.: A Stochastic Extension of the Logic PDL. Technical Report 2004-5, Universit\u00e4t der Bundeswehr M\u00fcnchen, Dept. of Computer Science (2004), \n                    \n                      http:\/\/fakinf.informatik.unibw-muenchen.de\/~msiegle\/PAPERS\/TR_2004_5.ps.gz"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-540-30233-9_22","volume-title":"Applying Formal Methods: Testing, Performance, and M\/E-Commerce","author":"M. Kuntz","year":"2004","unstructured":"Kuntz, M., Siegle, M., Werner, E.: CASPA - A Tool for Symbolic Performance and Dependability Evaluation. In: N\u00fa\u00f1ez, M., Maamar, Z., Pelayo, F.L., Pousttchi, K., Rubio, F. (eds.) FORTE 2004. LNCS, vol.\u00a03236, pp. 293\u2013307. Springer, Heidelberg (2004)"},{"issue":"2","key":"6_CR21","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/s10009-004-0140-2","volume":"6","author":"M. Kwiatkowska","year":"2004","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: A hybrid approach. International Journal on Software Tools for Technology Transfer (STTT)\u00a06(2), 128\u2013142 (2004)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"6_CR22","unstructured":"Meyer-Kayser, J.: Verifikation stochastischer prozessalgebraischer Modelle mit aCSL+. Technical Report IB 01\/03, Universit\u00e4at Erlangen-N\u00fcrnberg, Institut f\u00fcr Informatik 7 (2003) (in German)"},{"issue":"3-4","key":"6_CR23","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1016\/S0166-5316(99)00010-3","volume":"35","author":"W.D. Obal","year":"1999","unstructured":"Obal, W.D., Sanders, W.H.: State-space support for path-based reward variables. Performance Evaluation\u00a035(3-4), 233\u2013251 (1999)","journal-title":"Performance Evaluation"},{"issue":"3","key":"6_CR24","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1016\/0743-7315(92)90006-9","volume":"15","author":"W.H. Sanders","year":"1992","unstructured":"Sanders, W.H., Malhis, L.M.: Dependability evaluation using composed SANbased reward models. Journal of Parallel and Distributed Computing\u00a015(3), 238\u2013254 (1992)","journal-title":"Journal of Parallel and Distributed Computing"},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1007\/3-540-44667-2_9","volume-title":"Lectures on Formal Methods and Performance Analysis","author":"W.H. Sanders","year":"2001","unstructured":"Sanders, W.H., Meyer, J.F.: Stochastic Activity Networks: Formal Definitions and Concepts. In: Brinksma, E., Hermanns, H., Katoen, J.-P. (eds.) EEF School 2000 and FMPA 2000. LNCS, vol.\u00a02090, pp. 315\u2013343. Springer, Heidelberg (2001)"},{"key":"6_CR26","volume-title":"Behaviour analysis of communication systems: Compositional modelling, compact representation and analysis of performability properties","author":"M. Siegle","year":"2002","unstructured":"Siegle, M.: Behaviour analysis of communication systems: Compositional modelling, compact representation and analysis of performability properties. Shaker Verlag, Aachen (2002)"}],"container-title":["Lecture Notes in Computer Science","Model Checking Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11691617_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,12]],"date-time":"2019-03-12T01:55:08Z","timestamp":1552355708000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11691617_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540331025","9783540331032"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/11691617_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}