{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,18]],"date-time":"2026-04-18T03:14:42Z","timestamp":1776482082529,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540253044","type":"print"},{"value":"9783540318620","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/978-3-540-31862-0_21","type":"book-chapter","created":{"date-parts":[[2010,3,12]],"date-time":"2010-03-12T13:28:55Z","timestamp":1268400535000},"page":"280-294","source":"Crossref","is-referenced-by-count":116,"title":["Symbolic and Parametric Model Checking of Discrete-Time Markov Chains"],"prefix":"10.1007","author":[{"given":"Conrado","family":"Daws","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"21_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"155","DOI":"10.1007\/3-540-60045-0_48","volume-title":"Computer Aided Verification","author":"A. Aziz","year":"1995","unstructured":"Aziz, A., Singhal, V., Balarin, F., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: It usually works: The temporal logic of stochastic systems. In: Wolper, P. (ed.) CAV 1995. LNCS, vol.\u00a0939, pp. 155\u2013165. Springer, Heidelberg (1995)"},{"key":"21_CR2","volume-title":"Handbook of Process Algebrea","author":"J. Bergstra","year":"2001","unstructured":"Bergstra, J., Fokkink, W., Ponse, A.: Process algebra with recursive operations. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebrea. Elsevier Science, Amsterdam (2001)"},{"issue":"4","key":"21_CR3","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1093\/comjnl\/37.4.243","volume":"37","author":"J.A. Bergstra","year":"1994","unstructured":"Bergstra, J.A., Bethke, I., Ponse, A.: Process algebra with iteration and nesting. The Computer Journal\u00a037(4), 243\u2013258 (1994)","journal-title":"The Computer Journal"},{"key":"21_CR4","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-73235-5","volume-title":"Rational Series and Their Languages. EATCS Monographs in Computer Science","author":"J. Berstel","year":"1988","unstructured":"Berstel, J., Reutenauer, C.: Rational Series and Their Languages. EATCS Monographs in Computer Science. Springer, Heidelberg (1988)"},{"key":"21_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"A. Bianco","year":"1995","unstructured":"Bianco, A., de Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Thiagarajan, P.S. (ed.) FSTTCS 1995. LNCS, vol.\u00a01026, pp. 499\u2013513. Springer, Heidelberg (1995)"},{"key":"21_CR6","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1109\/DSN.2003.1209963","volume-title":"Proceedings of the 2003 International Conference on Dependable Systems and Networks (DSN 2003)","author":"H. Bohnenkamp","year":"2003","unstructured":"Bohnenkamp, H., van der Stok, P., Hermanns, H., Vaandrager, F.: Cost-optimization of the IPv4 zeroconf protocol. In: Proceedings of the 2003 International Conference on Dependable Systems and Networks (DSN 2003), June 2003, pp. 531\u2013540. IEEE Computer Society, Los Alamitos (2003)"},{"key":"21_CR7","doi-asserted-by":"crossref","unstructured":"Brzozowsky, J.: Derivatives of regular expressions. Journal of ACM\u00a011(4) (1964)","DOI":"10.1145\/321239.321249"},{"issue":"4","key":"21_CR8","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM\u00a042(4), 857\u2013907 (1995)","journal-title":"Journal of the ACM"},{"key":"21_CR9","series-title":"Lecture Notes in Computer Science","first-page":"29","volume-title":"Process Algebra and Probabilistic Methods. Performance Modelling and Verification","author":"P. D\u2019Argenio","year":"2001","unstructured":"D\u2019Argenio, P., Jeannet, B., Jensen, H., Larsen, K.: Reachability analysis of probabilistic systems by successive refinements. In: de Luca, L., Gilmore, S. (eds.) PROBMIV 2001, PAPM-PROBMIV 2001, and PAPM 2001. LNCS, vol.\u00a02165, pp. 29\u201356. Springer, Heidelberg (2001)"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/3-540-45605-8_5","volume-title":"Process Algebra and Probabilistic Methods. Performance Modeling and Verification","author":"P. D\u2019Argenio","year":"2002","unstructured":"D\u2019Argenio, P., Jeannet, B., Jensen, H., Larsen, K.: Reduction and refinement strategies for probabilistic analysis. In: Hermanns, H., Segala, R. (eds.) PROBMIV 2002, PAPM-PROBMIV 2002, and PAPM 2002. LNCS, vol.\u00a02399, p. 57. Springer, Heidelberg (2002)"},{"key":"21_CR11","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/978-1-4613-2007-4_3","volume-title":"VLSI Specification, Verification and Synthesis","author":"M.J.C. Gordon","year":"1988","unstructured":"Gordon, M.J.C.: HOL: A proof generating system for higher-order logic. In: Birtwistle, G., Subrahmanyam, P.A. (eds.) VLSI Specification, Verification and Synthesis, pp. 73\u2013128. Kluwer Academic Publishers, Boston (1988)"},{"key":"21_CR12","volume-title":"Introduction to HOL (A theorem-proving environment for higher order logic)","author":"M.J.C. Gordon","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F.: Introduction to HOL (A theorem-proving environment for higher order logic). Cambridge University Press, Cambridge (1993)"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"Gramond, Rodger: Using JFLAP to interact with theorems in automata theory. SIGCSEB: SIGCSE Bulletin (ACM Special Interest Group on Computer Science Education)\u00a031 (1999)","DOI":"10.1145\/384266.299800"},{"issue":"5","key":"21_CR14","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and probability. Formal Aspects of Computing\u00a06(5), 512\u2013535 (1994)","journal-title":"Formal Aspects of Computing"},{"key":"21_CR15","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J.E. Hopcroft","year":"2000","unstructured":"Hopcroft, J.E., Motwani, R.R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley Longman, Reading (2000)"},{"key":"21_CR16","unstructured":"Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD thesis, University of Cambridge (2002)"},{"key":"21_CR17","unstructured":"Jeannet, B., D\u2019Argenio, P., Larsen, K.: Rapture: A tool for verifying Markov Decision Processes. In: I.\u00a0Cerna, editor, Tools Day 2002, Brno, Czech Republic, Technical Report. Faculty of Informatics, Masaryk University Brno (2002)"},{"key":"21_CR18","unstructured":"JFLAP (java formal languages and automata package) web page, http:\/\/www.cs.duke.edu\/~rodger\/tools\/jflap\/"},{"key":"21_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable Markov Chains. Graduate Texts in Mathematics","author":"J. Kemeny","year":"1976","unstructured":"Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains. Graduate Texts in Mathematics, 2nd edn. Springer, Heidelberg (1976)","edition":"2"},{"key":"21_CR20","volume-title":"Algorithms and Complexity: New Directions and Recent Results","author":"D.E. Knuth","year":"1976","unstructured":"Knuth, D.E., Yao, A.C.: The complexity of nonuniform random number generation. In: Traub, J.F. (ed.) Algorithms and Complexity: New Directions and Recent Results. Academic Press, New York (1976)"},{"key":"21_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"200","DOI":"10.1007\/3-540-46029-2_13","volume-title":"Computer Performance Evaluation","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM: Probabilistic symbolic model checker. In: Field, T., Harrison, P.G., Bradley, J., Harder, U. (eds.) TOOLS 2002. LNCS, vol.\u00a02324, pp. 200\u2013204. Springer, Heidelberg (2002)"},{"key":"21_CR22","unstructured":"PRISM web page, http:\/\/www.cs.bham.ac.uk\/~dxp\/prism\/"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing - ICTAC 2004"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-31862-0_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,19]],"date-time":"2020-11-19T04:30:00Z","timestamp":1605760200000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-31862-0_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540253044","9783540318620"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-31862-0_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005]]}}}