{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:59:27Z","timestamp":1779087567858,"version":"3.51.4"},"publisher-location":"Cham","reference-count":110,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319105741","type":"print"},{"value":"9783319105758","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-10575-8_28","type":"book-chapter","created":{"date-parts":[[2018,5,18]],"date-time":"2018-05-18T04:05:28Z","timestamp":1526616328000},"page":"963-999","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":86,"title":["Model Checking Probabilistic Systems"],"prefix":"10.1007","author":[{"given":"Christel","family":"Baier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"de Alfaro","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vojt\u011bch","family":"Forejt","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marta","family":"Kwiatkowska","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,5,19]]},"reference":[{"key":"28_CR1","series-title":"LNCS","first-page":"320","volume-title":"Proc. CONCUR\u201900","author":"P. Abdulla","year":"2000","unstructured":"Abdulla, P., Baier, C., Iyer, P., Jonsson, B.: Reasoning about probabilistic lossy channel systems. In: Palamidessi, C. (ed.) Proc. CONCUR\u201900. LNCS, vol.\u00a01877, pp.\u00a0320\u2013330. Springer, Heidelberg (2000)"},{"key":"28_CR2","series-title":"Wiley Series in Parallel Computing","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 Series in Parallel Computing. Wiley, New York (1995)"},{"key":"28_CR3","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-84800-223-4","volume-title":"A Process Algebraic Approach to Software Architecture Design","author":"A. Aldini","year":"2010","unstructured":"Aldini, A., Bernardo, M., Corradini, F.: A Process Algebraic Approach to Software Architecture Design. Springer, Heidelberg (2010)"},{"key":"28_CR4","unstructured":"de Alfaro, L.: Formal verification of probabilistic systems. Ph.D. thesis, Stanford University, Department of Computer Science (1997)"},{"key":"28_CR5","series-title":"LNCS","first-page":"351","volume-title":"CONCUR","author":"L. Alfaro de","year":"2001","unstructured":"de Alfaro, L., Henzinger, T.A., Jhala, R.: Compositional methods for probabilistic systems. In: Larsen, K.G., Nielsen, M. (eds.) CONCUR. LNCS, vol.\u00a02154, pp.\u00a0351\u2013365. Springer, Heidelberg (2001)"},{"key":"28_CR6","series-title":"LNCS","first-page":"395","volume-title":"Proc. Tools and Algorithms for Construction and Analysis of Systems (TACAS)","author":"L. Alfaro de","year":"2000","unstructured":"de Alfaro, L., Kwiatkowska, M., Norman, G., Parker, D., Segala, R.: Symbolic model checking of probabilistic processes using MTBDDs and the Kronecker representation. In: Graf, S., Schwartzbach, M.I. (eds.) Proc. Tools and Algorithms for Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a01785, pp.\u00a0395\u2013410. Springer, Heidelberg (2000)"},{"key":"28_CR7","volume-title":"Probability and Measure Theory","author":"R. Ash","year":"2000","unstructured":"Ash, R., Dol\u00e9ans-Dade, C.: Probability and Measure Theory. Harcourt\/Academic Press, San Diego (2000)"},{"key":"28_CR8","first-page":"57","volume-title":"Proc. of the 2nd ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)","author":"C. Baier","year":"2004","unstructured":"Baier, C., Ciesinski, F., Gr\u00f6\u00dfer, M.: ProbMeLa: a modeling language for communicating probabilistic systems. In: Proc. of the 2nd ACM-IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp.\u00a057\u201366. IEEE, Piscataway (2004)"},{"key":"28_CR9","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"430","DOI":"10.1007\/3-540-63165-8_199","volume-title":"Proc. International Colloqium on Automata, Languages and Programming (ICALP)","author":"C. Baier","year":"1997","unstructured":"Baier, C., Clarke, E., Hartonas-Garmhausen, V., Kwiatkowska, M., Ryan, M.: Symbolic model checking for probabilistic processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) Proc. International Colloqium on Automata, Languages and Programming (ICALP). LNCS, vol.\u00a01256, pp.\u00a0430\u2013440. Springer, Heidelberg (1997)"},{"key":"28_CR10","series-title":"LNCS","first-page":"34","volume-title":"Intl. AMAST Workshop, ARTS","author":"C. Baier","year":"1999","unstructured":"Baier, C., Engelen, B.: Establishing qualitative properties for probabilistic lossy channel systems: an algorithmic approach. In: Katoen, J.-P. (ed.) Intl. AMAST Workshop, ARTS. LNCS, vol.\u00a01601, pp.\u00a034\u201352. Springer, Heidelberg (1999)"},{"key":"28_CR11","series-title":"An EATCS Series","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/978-3-642-01492-5_13","volume-title":"Handbook of Weighted Automata, Monographs in Theoretical Computer Science","author":"C. Baier","year":"2009","unstructured":"Baier, C., Gr\u00f6\u00dfer, M., Ciesinski, F.: Model checking linear time properties of probabilistic systems. In: Droste, M., Kuich, W., Vogler, H. (eds.) Handbook of Weighted Automata, Monographs in Theoretical Computer Science. An EATCS Series, pp.\u00a0519\u2013570. Springer, Heidelberg (2009)"},{"key":"28_CR12","first-page":"493","volume-title":"Proc. 3rd IFIP Int. Conf. Theoretical Computer Science (TCS\u201906)","author":"C. Baier","year":"2004","unstructured":"Baier, C., Gr\u00f6\u00dfer, M., Leucker, M., Bollig, B., Ciesinski, F.: Controller synthesis for probabilistic systems. In: L\u00e9vy, J.J., Mayr, E., Mitchell, J. (eds.) Proc. 3rd IFIP Int. Conf. Theoretical Computer Science (TCS\u201906), pp.\u00a0493\u20135062. Kluwer Academic, Dordrecht (2004)"},{"issue":"9","key":"28_CR13","doi-asserted-by":"crossref","first-page":"76","DOI":"10.1145\/1810891.1810912","volume":"53","author":"C. Baier","year":"2010","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P.: Performance evaluation and model checking join forces. Commun. ACM 53(9), 76\u201385 (2010)","journal-title":"Commun. ACM"},{"key":"28_CR14","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"28_CR15","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1007\/s004460050046","volume":"11","author":"C. Baier","year":"1998","unstructured":"Baier, C., Kwiatkowska, M.: Model checking for a probabilistic branching time logic with fairness. Distrib. Comput. 11, 125\u2013155 (1998)","journal-title":"Distrib. Comput."},{"key":"28_CR16","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1109\/QEST.2008.29","volume-title":"Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems","author":"J. Barnat","year":"2008","unstructured":"Barnat, J., Brim, L., \u010cern\u00e1, I., \u010ce\u0161ka, M., T\u016fmov\u00e1, J.: ProbDiVinE-MC: multi-core LTL model checker for probabilistic systems. In: Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems, pp.\u00a077\u201378. IEEE, Washington (2008)"},{"key":"28_CR17","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"499","DOI":"10.1007\/3-540-60692-0_70","volume-title":"Proceedings of Foundations of Software Technology and Theoretical Computer Science","author":"A. Bianco","year":"1995","unstructured":"Bianco, A., De Alfaro, L.: Model checking of probabilistic and non-deterministic systems. In: Thiagarajan, P.S. (ed.) Proceedings of Foundations of Software Technology and Theoretical Computer Science. LNCS, vol.\u00a01026, pp.\u00a0499\u2013513. Springer, Heidelberg (1995)"},{"key":"28_CR18","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/978-3-642-45221-5_12","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning\u2014Proceedings of the 19th International Conference, LPAR-19","author":"F. Blahoudek","year":"2013","unstructured":"Blahoudek, F., Kret\u00ednsk\u00fd, M., Strejcek, J.: Comparison of LTL to deterministic Rabin automata translators. In: McMillan, K.L., Middeldorp, A., Voronkov, A. (eds.) Logic for Programming, Artificial Intelligence, and Reasoning\u2014Proceedings of the 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14\u201319, 2013. LNCS, vol.\u00a08312, pp.\u00a0164\u2013172. Springer, Heidelberg (2013)"},{"key":"28_CR19","series-title":"LNCS","first-page":"59","volume-title":"FMOODS\/FORTE","author":"J. Bogdoll","year":"2011","unstructured":"Bogdoll, J., Fioriti, L.M.F., Hartmanns, A., Hermanns, H.: Partial order methods for statistical model checking and simulation. In: Bruni, R., Dingel, J. (eds.) FMOODS\/FORTE. LNCS, vol.\u00a06722, pp.\u00a059\u201374. Springer, Heidelberg (2011)"},{"issue":"10","key":"28_CR20","doi-asserted-by":"crossref","first-page":"812","DOI":"10.1109\/TSE.2006.104","volume":"32","author":"H. Bohnenkamp","year":"2006","unstructured":"Bohnenkamp, H., D\u2019Argenio, P., Hermanns, H., Katoen, J.P.: MODEST: a compositional modeling formalism for hard and softly timed systems. IEEE Trans. Softw. Eng. 32(10), 812\u2013830 (2006)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"28_CR21","doi-asserted-by":"crossref","DOI":"10.1002\/0471200581","volume-title":"Queueing Networks and Markov Chains: Modeling and Performance Evaluation with Computer Science Applications","author":"G. Bolch","year":"1998","unstructured":"Bolch, G., Greiner, S., de Meer, H., Trivedi, K.: Queueing Networks and Markov Chains: Modeling and Performance Evaluation with Computer Science Applications. Wiley-Interscience, New York (1998)"},{"key":"28_CR22","unstructured":"Br\u00e1zdil, T.: Verification of probabilistic recursive sequential programs. Ph.D. thesis, Masaryk University (2007)"},{"key":"28_CR23","first-page":"33","volume-title":"Proceedings of LICS\u201911","author":"T. Br\u00e1zdil","year":"2011","unstructured":"Br\u00e1zdil, T., Bro\u017eek, V., Chatterjee, K., Forejt, V., Ku\u010dera, A.: Two views on multiple mean-payoff objectives in Markov decision processes. In: Proceedings of LICS\u201911, pp.\u00a033\u201342. IEEE, Piscataway (2011)"},{"key":"28_CR24","first-page":"349","volume-title":"21th IEEE Symp. Logic in Computer Science (LICS 2006)","author":"T. Br\u00e1zdil","year":"2006","unstructured":"Br\u00e1zdil, T., Bro\u017eek, V., Forejt, V., Ku\u010dera, A.: Stochastic games with branching-time winning objectives. In: 21th IEEE Symp. Logic in Computer Science (LICS 2006), pp.\u00a0349\u2013358. IEEE, Piscataway (2006)"},{"key":"28_CR25","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"98","DOI":"10.1007\/978-3-319-11936-6_8","volume-title":"Proc. 12th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201914)","author":"T. Br\u00e1zdil","year":"2014","unstructured":"Br\u00e1zdil, T., Chatterjee, K., Chmel\u00edk, M., Forejt, V., K\u0159et\u00ednsk\u00fd, J., Kwiatkowska, M., Parker, D., Ujma, M.: Verification of Markov decision processes using learning algorithms. In: Cassez, F., Raskin, J. (eds.) Proc. 12th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201914). LNCS, vol.\u00a08837, pp.\u00a098\u2013114. Springer, Heidelberg (2014)"},{"issue":"2","key":"28_CR26","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/s10703-012-0166-0","volume":"43","author":"T. Br\u00e1zdil","year":"2013","unstructured":"Br\u00e1zdil, T., Esparza, J., Kiefer, S., Ku\u010dera, A.: Analyzing probabilistic pushdown automata. Form. Methods Syst. Des. 43(2), 124\u2013163 (2013)","journal-title":"Form. Methods Syst. Des."},{"key":"28_CR27","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1007\/978-3-540-70583-3_13","volume-title":"Proc. 35th Int. Colloq. Automata, Languages and Programming, Part II (ICALP\u201908)","author":"T. Br\u00e1zdil","year":"2008","unstructured":"Br\u00e1zdil, T., Forejt, V., Ku\u010dera, A.: Controller synthesis and verification for Markov decision processes with qualitative branching time objectives. In: Aceto, L., Damg\u00e5rd, I., Goldberg, L., Halld\u00f3rsson, M., Ing\u00f3lfsd\u00f3ttir, A., Walukiewicz, I. (eds.) Proc. 35th Int. Colloq. Automata, Languages and Programming, Part II (ICALP\u201908). LNCS, vol.\u00a05126, pp.\u00a0148\u2013159. Springer, Heidelberg (2008)"},{"key":"28_CR28","series-title":"LIPIcs","first-page":"474","volume-title":"FSTTCS","author":"T. Br\u00e1zdil","year":"2012","unstructured":"Br\u00e1zdil, T., Hermanns, H., Kr\u010d\u00e1l, J., K\u0159et\u00ednsk\u00fd, J., \u0158eh\u00e1k, V.: Verification of open interactive Markov chains. In: D\u2019Souza, D., Kavitha, T., Radhakrishnan, J. (eds.) FSTTCS. LIPIcs, vol.\u00a018, pp.\u00a0474\u2013485. Schloss Dagstuhl\u2014Leibniz-Zentrum fuer Informatik, Dagstuhl (2012)"},{"key":"28_CR29","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1007\/978-3-642-39799-8_7","volume-title":"Computer Aided Verification","author":"Lubo\u0161 Brim","year":"2013","unstructured":"Brim, L., \u010ce\u0161ka, M., Dra\u017ean, S., \u0160afr\u00e1nek, D.: Exploring parameter space of stochastic biochemical systems using quantitative model checking. In: Sharygina and Veith [96], pp.\u00a0107\u2013123"},{"key":"28_CR30","series-title":"Natural Computing Series","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1007\/978-3-540-88869-7_22","volume-title":"Algorithmic Bioprocesses","author":"L. Cardelli","year":"2009","unstructured":"Cardelli, L.: Artificial biochemistry. In: Condon, A., Harel, D., Kok, J.N., Salomaa, A., Winfree, E. (eds.) Algorithmic Bioprocesses. Natural Computing Series, pp.\u00a0429\u2013462. Springer, Heidelberg (2009)"},{"key":"28_CR31","series-title":"LNCS","first-page":"371","volume-title":"Proc. 14th Int. Conf. Concurrency Theory (CONCUR\u201902)","author":"S. Cattani","year":"2002","unstructured":"Cattani, S., Segala, R.: Decision algorithms for probabilistic bisimulation. In: Brim, L., Jan\u010dar, P., K\u0159et\u00ednsk\u00fd, M., Ku\u010dera, A. (eds.) Proc. 14th Int. Conf. Concurrency Theory (CONCUR\u201902). LNCS, vol.\u00a02421, pp.\u00a0371\u2013385. Springer, Heidelberg (2002)"},{"key":"28_CR32","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Gaiser, A., K\u0159et\u00ednsk\u00fd, J.: Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. In: Sharygina and Veith [13, 21, 61], pp.\u00a0559\u2013575","DOI":"10.1007\/978-3-642-39799-8_37"},{"key":"28_CR33","series-title":"LNCS","first-page":"100","volume-title":"Proceedings of the International Conference for Computer Science Logic (CSL)","author":"K. Chatterjee","year":"2003","unstructured":"Chatterjee, K., Jurdzinski, M., Henzinger, T.: Simple stochastic parity games. In: Baaz, M., Makowsky, J.A. (eds.) Proceedings of the International Conference for Computer Science Logic (CSL). LNCS, vol.\u00a02803, pp.\u00a0100\u2013113. Springer, Heidelberg (2003)"},{"key":"28_CR34","first-page":"121","volume-title":"Proceedings of the Annual Symposium on Discrete Algorithms (SODA)","author":"K. Chatterjee","year":"2004","unstructured":"Chatterjee, K., Jurdzinski, M., Henzinger, T.: Quantitative stochastic parity games. In: Munro, J.I. (ed.) Proceedings of the Annual Symposium on Discrete Algorithms (SODA), pp.\u00a0121\u2013130. SIAM, Philadelphia (2004)"},{"key":"28_CR35","series-title":"LNCS","first-page":"325","volume-title":"STACS","author":"K. Chatterjee","year":"2006","unstructured":"Chatterjee, K., Majumdar, R., Henzinger, T.A.: Markov decision processes with multiple objectives. In: Durand, B., Thomas, W. (eds.) STACS. LNCS, vol.\u00a03884, pp.\u00a0325\u2013336. Springer, Heidelberg (2006)"},{"issue":"1","key":"28_CR36","doi-asserted-by":"crossref","first-page":"61","DOI":"10.1007\/s10703-013-0183-7","volume":"43","author":"T. Chen","year":"2013","unstructured":"Chen, T., Forejt, V., Kwiatkowska, M., Parker, D., Simaitis, A.: Automatic verification of competitive stochastic systems. Form. Methods Syst. Des. 43(1), 61\u201392 (2013)","journal-title":"Form. Methods Syst. Des."},{"key":"28_CR37","doi-asserted-by":"crossref","first-page":"85","DOI":"10.1109\/TASE.2013.20","volume-title":"Proc. 7th International Symposium on Theoretical Aspects of Software Engineering (TASE\u201913)","author":"T. Chen","year":"2013","unstructured":"Chen, T., Hahn, E.M., Han, T., Kwiatkowska, M., Qu, H., Zhang, L.: Model repair for Markov decision processes. In: Proc. 7th International Symposium on Theoretical Aspects of Software Engineering (TASE\u201913), pp.\u00a085\u201392. IEEE, Piscataway (2013)"},{"key":"28_CR38","first-page":"131","volume-title":"Proc. QEST 2007","author":"F. Ciesinski","year":"2007","unstructured":"Ciesinski, F., Baier, C.: LiQuor: a tool for qualitative and quantitative linear time analysis of reactive systems. In: Proc. QEST 2007, pp.\u00a0131\u2013132. IEEE, Piscataway (2007)"},{"issue":"33\u201334","key":"28_CR39","doi-asserted-by":"crossref","first-page":"3065","DOI":"10.1016\/j.tcs.2009.02.037","volume":"410","author":"F. Ciocchetta","year":"2009","unstructured":"Ciocchetta, F., Hillston, J.: Bio-PEPA: a framework for the modelling and analysis of biological systems. Theor. Comput. Sci. 410(33\u201334), 3065\u20133084 (2009)","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"28_CR40","doi-asserted-by":"crossref","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. J. ACM 42(4), 857\u2013907 (1995)","journal-title":"J. ACM"},{"key":"28_CR41","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"249","DOI":"10.1007\/3-540-48683-6_23","volume-title":"Proc. International Conference on Computer Aided Verification (CAV)","author":"M. Daniele","year":"1999","unstructured":"Daniele, M., Giunchiglia, F., Vardi, M.: Improved automata generation for linear temporal logic. In: Halbwachs, N., Peled, D. (eds.) Proc. International Conference on Computer Aided Verification (CAV). LNCS, vol.\u00a01633, pp.\u00a0249\u2013260. Springer, Heidelberg (1999)"},{"key":"28_CR42","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1109\/ACSD.2010.13","volume-title":"Proc. 10th Int. Conf. Application of Concurrency to System Design (ACSD\u201910)","author":"B. Delahaye","year":"2010","unstructured":"Delahaye, B., Caillaud, B., Legay, A.: Probabilistic contracts: a compositional reasoning methodology for the design of stochastic systems. In: Proc. 10th Int. Conf. Application of Concurrency to System Design (ACSD\u201910), pp.\u00a0223\u2013232. IEEE, Piscataway (2010)"},{"key":"28_CR43","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/978-3-642-18275-4_23","volume-title":"12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)","author":"B. Delahaye","year":"2011","unstructured":"Delahaye, B., Katoen, J.P., Larsen, K., Legay, A., Pedersen, M., Sher, F., Wasowski, A.: Abstract probabilistic automata. In: Jhala, R., Schmidt, D.A. (eds.) 12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). LNCS, vol.\u00a06538, pp.\u00a0324\u2013339. Springer, Heidelberg (2011)"},{"key":"28_CR44","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"9","DOI":"10.1007\/11901914_4","volume-title":"Proc. 4th Int. Symp. Automated Technology for Verification and Analysis (ATVA\u201906)","author":"A. Donaldson","year":"2006","unstructured":"Donaldson, A., Miller, A.: Symmetry reduction for probabilistic model checking using generic representatives. In: Graf, S., Zhang, W. (eds.) Proc. 4th Int. Symp. Automated Technology for Verification and Analysis (ATVA\u201906). LNCS, vol.\u00a04218, pp.\u00a09\u201323. Springer, Heidelberg (2006)"},{"issue":"6","key":"28_CR45","doi-asserted-by":"crossref","first-page":"621","DOI":"10.1007\/s10009-006-0014-x","volume":"8","author":"M. Duflot","year":"2006","unstructured":"Duflot, M., Kwiatkowska, M., Norman, G., Parker, D.: A formal analysis of Bluetooth device discovery. Int. J. Softw. Tools Technol. Transf. 8(6), 621\u2013632 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"28_CR46","first-page":"996","volume-title":"Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics","author":"E.A. Emerson","year":"1990","unstructured":"Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B: Formal Models and Semantics, pp.\u00a0996\u20131072. Elsevier, Amsterdam (1990). Chap.\u00a014"},{"key":"28_CR47","series-title":"LNCS","first-page":"192","volume-title":"Computer Aided Verification\u2014Proceedings of the 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014","author":"J. Esparza","year":"2014","unstructured":"Esparza, J., K\u0159et\u00ednsk\u00fd, J.: From LTL to deterministic automata: a Safraless compositional approach. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification\u2014Proceedings of the 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18\u201322, 2014. LNCS, vol.\u00a08559, pp.\u00a0192\u2013208. Springer, Heidelberg (2014)"},{"key":"28_CR48","doi-asserted-by":"crossref","unstructured":"Etessami, K., Kwiatkowska, M.Z., Vardi, M.Y., Yannakakis, M.: Multi-objective model checking of Markov decision processes. Log. Methods Comput. Sci. 4(4) (2008)","DOI":"10.2168\/LMCS-4(4:8)2008"},{"issue":"2","key":"28_CR49","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/2159531.2159534","volume":"13","author":"K. Etessami","year":"2012","unstructured":"Etessami, K., Yannakakis, M.: Model checking of recursive probabilistic systems. ACM Trans. Comput. Log. 13(2), 1\u201340 (2012)","journal-title":"ACM Trans. Comput. Log."},{"key":"28_CR50","volume-title":"An Introduction to Probability Theory and Its Applications","author":"W. Feller","year":"1950","unstructured":"Feller, W.: An Introduction to Probability Theory and Its Applications. Wiley, New York (1950)"},{"key":"28_CR51","first-page":"133","volume-title":"Proc. 7th Int. Conf. Quantitative Evaluation of Systems (QEST\u201910)","author":"L. Feng","year":"2010","unstructured":"Feng, L., Kwiatkowska, M., Parker, D.: Compositional verification of probabilistic systems using learning. In: Proc. 7th Int. Conf. Quantitative Evaluation of Systems (QEST\u201910), pp.\u00a0133\u2013142. IEEE, Piscataway (2010)"},{"key":"28_CR52","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/978-3-642-21455-4_3","volume-title":"Formal Methods for Eternal Networked Software Systems (SFM\u201911)","author":"V. Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D.: Automated verification techniques for probabilistic systems. In: Bernardo, M., Issarny, V. (eds.) Formal Methods for Eternal Networked Software Systems (SFM\u201911). LNCS, vol.\u00a06659, pp.\u00a053\u2013113. Springer, Heidelberg (2011)"},{"key":"28_CR53","series-title":"LNCS","first-page":"112","volume-title":"Proc. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201911)","author":"V. Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Abdulla, P., Leino, K. (eds.) Proc. 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201911). LNCS, vol.\u00a06605, pp.\u00a0112\u2013127. Springer, Heidelberg (2011)"},{"issue":"2\/3","key":"28_CR54","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1023\/A:1008647823331","volume":"10","author":"M. Fujita","year":"1997","unstructured":"Fujita, M., McGeer, P.C., Yang, J.C.Y.: Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Form. Methods Syst. Des. 10(2\/3), 149\u2013169 (1997)","journal-title":"Form. Methods Syst. Des."},{"key":"28_CR55","first-page":"130","volume-title":"Proc. 5th Annual Symposium on Logic in Computer Science (LICS)","author":"R. Glabbeek van","year":"1990","unstructured":"van Glabbeek, R., Smolka, S.A., Steffen, B., Tofts, C.M.N.: Reactive, generative, and stratified models of probabilistic processes. In: Proc. 5th Annual Symposium on Logic in Computer Science (LICS), pp.\u00a0130\u2013141. IEEE, Piscataway (1990)"},{"key":"28_CR56","series-title":"LNCS","volume-title":"Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001]","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001]. LNCS, vol.\u00a02500. Springer, Heidelberg (2002)"},{"key":"28_CR57","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"660","DOI":"10.1007\/978-3-642-14295-6_56","volume-title":"22nd International Conference on Computer Aided Verification (CAV)","author":"E. Hahn","year":"2010","unstructured":"Hahn, E., Hermanns, H., Wachter, B., Zhang, L.: PARAM: a model checker for parametric Markov models. In: Touili, T., Cook, B., Jackson, P. (eds.) 22nd International Conference on Computer Aided Verification (CAV). LNCS, vol.\u00a06174, pp.\u00a0660\u2013664. Springer, Heidelberg (2010)"},{"key":"28_CR58","series-title":"LNCS","first-page":"353","volume-title":"Proc. TACAS 2010","author":"E.M. Hahn","year":"2010","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PASS: abstraction refinement for infinite probabilistic models. In: Esparza, J., Majumdar, R. (eds.) Proc. TACAS 2010. LNCS, vol.\u00a06015, pp.\u00a0353\u2013357. Springer, Heidelberg (2010)"},{"issue":"5","key":"28_CR59","doi-asserted-by":"crossref","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 reliability. Form. Asp. Comput. 6(5), 512\u2013535 (1994)","journal-title":"Form. Asp. Comput."},{"key":"28_CR60","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1007\/3-540-48778-6_6","volume-title":"5th International AMAST Workshop on Formal Methods for Real-Time and Probabilistic Systems (ARTS)","author":"V. Hartonas-Garmhausen","year":"1999","unstructured":"Hartonas-Garmhausen, V., Campos, S., Clarke, E.: ProbVerus: probabilistic symbolic model checking. In: Katoen, J. (ed.) 5th International AMAST Workshop on Formal Methods for Real-Time and Probabilistic Systems (ARTS). LNCS, vol.\u00a01601, pp.\u00a096\u2013110. Springer, Heidelberg (1999)"},{"key":"28_CR61","doi-asserted-by":"crossref","DOI":"10.1002\/0470841923","volume-title":"Performance of Computer Communication Systems: A Model-Based Approach","author":"B. Haverkort","year":"1998","unstructured":"Haverkort, B.: Performance of Computer Communication Systems: A Model-Based Approach. Wiley, Chichester (1998)"},{"issue":"3","key":"28_CR62","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1016\/j.tcs.2007.11.013","volume":"319","author":"J. Heath","year":"2008","unstructured":"Heath, J., Kwiatkowska, M., Norman, G., Parker, D., Tymchyshyn, O.: Probabilistic model checking of complex biological pathways. Theor. Comput. Sci. 319(3), 239\u2013257 (2008)","journal-title":"Theor. Comput. Sci."},{"key":"28_CR63","first-page":"1","volume-title":"Proc. CMSB\u201911","author":"T.A. Henzinger","year":"2011","unstructured":"Henzinger, T.A., Mateescu, M.: Propagation models for computing biochemical reaction networks. In: Fages, F. (ed.) Proc. CMSB\u201911, pp.\u00a01\u20133. ACM, New York (2011)"},{"key":"28_CR64","series-title":"LNCS","first-page":"311","volume-title":"FMCO\u201909","author":"H. Hermanns","year":"2010","unstructured":"Hermanns, H., Katoen, J.P.: The how and why of interactive Markov chains. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO\u201909. LNCS, vol.\u00a06286, pp.\u00a0311\u2013337. Springer, Heidelberg (2010)"},{"key":"28_CR65","series-title":"LNCS","volume-title":"Proc. 2nd Joint Int. Workshop Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM-PROBMIV)","year":"2002","unstructured":"Hermanns, H., Segala, R. (eds.): Proc. 2nd Joint Int. Workshop Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM-PROBMIV). LNCS, vol.\u00a02399. Springer, Heidelberg (2002)"},{"issue":"1","key":"28_CR66","doi-asserted-by":"crossref","first-page":"96","DOI":"10.1016\/j.tcs.2005.08.005","volume":"346","author":"J. Hurd","year":"2005","unstructured":"Hurd, J., McIver, A., Morgan, C.: Probabilistic guarded commands mechanized in HOL. Theor. Comput. Sci. 346(1), 96\u2013112 (2005)","journal-title":"Theor. Comput. Sci."},{"key":"28_CR67","doi-asserted-by":"crossref","first-page":"111","DOI":"10.1109\/LICS.1997.614940","volume-title":"Proc. 12th Annual IEEE Symposium on Logic in Computer Science (LICS\u201997)","author":"M. Huth","year":"1997","unstructured":"Huth, M., Kwiatkowska, M.: Quantitative analysis and model checking. In: Proc. 12th Annual IEEE Symposium on Logic in Computer Science (LICS\u201997), pp.\u00a0111\u2013122. IEEE, Piscataway (1997)"},{"issue":"1","key":"28_CR68","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1016\/0890-5401(90)90004-2","volume":"88","author":"A. Itai","year":"1990","unstructured":"Itai, A., Rodeh, M.: Symmetry breaking in distributed networks. Inf. Comput. 88(1), 60\u201387 (1990)","journal-title":"Inf. Comput."},{"key":"28_CR69","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"667","DOI":"10.1007\/BFb0030633","volume-title":"TAPSOFT \u201997: Theory and Practice of Software Development","author":"P. Iyer","year":"1997","unstructured":"Iyer, P., Narasimha, M.: Probabilistic lossy channel systems. In: Bidoit, M., Dauchet, M. (eds.) TAPSOFT \u201997: Theory and Practice of Software Development. LNCS, vol.\u00a01214, pp.\u00a0667\u2013681. Springer, Heidelberg (1997)"},{"key":"28_CR70","unstructured":"Jeannet, B., d\u2019Argenio, P.R., Larsen, K.G.: Rapture: A tool for verifying Markov Decision Processes. In: Tools Day\u201902, Technical Report. Masaryk University, Brno (2002)"},{"key":"28_CR71","doi-asserted-by":"crossref","first-page":"685","DOI":"10.1016\/B978-044482830-9\/50029-1","volume-title":"Handbook of Process Algebra","author":"B. Jonsson","year":"2001","unstructured":"Jonsson, B., Larsen, K., Yi, W.: Probabilistic extensions of process algebras. In: Bergstra, J.A., Pomse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, pp.\u00a0685\u2013710. Elsevier, Amsterdam (2001)"},{"key":"28_CR72","doi-asserted-by":"crossref","DOI":"10.1007\/978-0-8176-4844-2","volume-title":"Linear Programming","author":"H. Karloff","year":"1991","unstructured":"Karloff, H.: Linear Programming. Birkh\u00e4user, Boston (1991)"},{"key":"28_CR73","series-title":"LNCS","first-page":"182","volume-title":"Proc. 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201909)","author":"M. Kattenbelt","year":"2009","unstructured":"Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: Abstraction refinement for probabilistic software. In: Jones, N., M\u00fcller-Olm, M. (eds.) Proc. 10th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI\u201909). LNCS, vol.\u00a05403, pp.\u00a0182\u2013197. Springer, Heidelberg (2009)"},{"issue":"3","key":"28_CR74","doi-asserted-by":"crossref","first-page":"246","DOI":"10.1007\/s10703-010-0097-6","volume":"36","author":"M. Kattenbelt","year":"2010","unstructured":"Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: A game-based abstraction-refinement framework for Markov decision processes. Form. Methods Syst. Des. 36(3), 246\u2013280 (2010)","journal-title":"Form. Methods Syst. Des."},{"key":"28_CR75","volume-title":"Finite Markov Chains","author":"J. Kemeny","year":"1960","unstructured":"Kemeny, J., Snell, J.: Finite Markov Chains. Van Nostrand, Princeton (1960)"},{"key":"28_CR76","series-title":"LNCS","first-page":"235","volume-title":"Automated Technology for Verification and Analysis\u2014Proceedings of the 12th International Symposium, ATVA 2014","author":"Z. Kom\u00e1rkov\u00e1","year":"2014","unstructured":"Kom\u00e1rkov\u00e1, Z., K\u0159et\u00ednsk\u00fd, J.: Rabinizer 3: Safraless translation of LTL to small deterministic automata. In: Cassez, F., Raskin, J. (eds.) Automated Technology for Verification and Analysis\u2014Proceedings of the 12th International Symposium, ATVA 2014, Sydney, NSW, Australia, November 3\u20137, 2014. LNCS, vol.\u00a08837, pp.\u00a0235\u2013241. Springer, Heidelberg (2014)"},{"key":"28_CR77","volume-title":"Modeling and Analysis of Stochastic Systems","author":"V. Kulkarni","year":"1995","unstructured":"Kulkarni, V.: Modeling and Analysis of Stochastic Systems. Chapman & Hall, London (1995)"},{"key":"28_CR78","series-title":"LNCS","first-page":"234","volume-title":"Proc. of the 18th International Conference on Computer Aided Verification (CAV)","author":"M. Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Symmetry reduction for probabilistic model checking. In: Ball, T., Jones, R.B. (eds.) Proc. of the 18th International Conference on Computer Aided Verification (CAV). LNCS, vol.\u00a04144, pp.\u00a0234\u2013248. Springer, Heidelberg (2006)"},{"issue":"4","key":"28_CR79","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/1364644.1364651","volume":"35","author":"M. Kwiatkowska","year":"2008","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Using probabilistic model checking in systems biology. ACM SIGMETRICS Perform. Eval. Rev. 35(4), 14\u201321 (2008)","journal-title":"ACM SIGMETRICS Perform. Eval. Rev."},{"key":"28_CR80","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"212","DOI":"10.1007\/978-3-642-04368-0_17","volume-title":"Proc. 7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS\u201909)","author":"M. Kwiatkowska","year":"2009","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic games for verification of probabilistic timed automata. In: Ouaknine, J., Vaandrager, F.W. (eds.) Proc. 7th International Conference on Formal Modelling and Analysis of Timed Systems (FORMATS\u201909). LNCS, vol.\u00a05813, pp.\u00a0212\u2013227. Springer, Heidelberg (2009)"},{"key":"28_CR81","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Proc. 23rd International Conference on Computer Aided Verification (CAV\u201911)","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.) Proc. 23rd International Conference on Computer Aided Verification (CAV\u201911). LNCS, vol.\u00a06806, pp.\u00a0585\u2013591. Springer, Heidelberg (2011)"},{"key":"28_CR82","series-title":"LNCS","first-page":"23","volume-title":"16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"M. Kwiatkowska","year":"2010","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Assume-guarantee verification for probabilistic systems. In: Esparza, R.M.J. (ed.) 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a06015, pp.\u00a023\u201337 (2010)"},{"key":"28_CR83","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1016\/j.ic.2013.10.001","volume":"232","author":"M. Kwiatkowska","year":"2013","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Compositional probabilistic verification through multi-objective model checking. Inf. Comput. 232, 38\u201365 (2013)","journal-title":"Inf. Comput."},{"key":"28_CR84","doi-asserted-by":"crossref","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. 282, 101\u2013150 (2002)","journal-title":"Theor. Comput. Sci."},{"key":"28_CR85","series-title":"LNCS","first-page":"169","volume-title":"Proc. 2nd Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM\/PROBMIV\u201902)","author":"M. Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Sproston, J.: Probabilistic model checking of the IEEE 802.11 wireless local area network protocol. In: Hermanns, H., Segala, R. (eds.) Proc. 2nd Joint International Workshop on Process Algebra and Probabilistic Methods, Performance Modeling and Verification (PAPM\/PROBMIV\u201902). LNCS, vol.\u00a02399, pp.\u00a0169\u2013187. Springer, Heidelberg (2002)"},{"key":"28_CR86","doi-asserted-by":"crossref","first-page":"359","DOI":"10.1109\/DSN.2011.5958249","volume-title":"Proc. IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN-PDS\u201911)","author":"M. Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Parker, D., Qu, H.: Incremental quantitative verification for Markov decision processes. In: Proc. IEEE\/IFIP International Conference on Dependable Systems and Networks (DSN-PDS\u201911), pp.\u00a0359\u2013370. IEEE, Piscataway (2011)"},{"issue":"1","key":"28_CR87","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K. Larsen","year":"1991","unstructured":"Larsen, K., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1\u201328 (1991)","journal-title":"Inf. Comput."},{"key":"28_CR88","first-page":"213","volume-title":"Lecture Notes in Computer Science","author":"Richard Lassaigne","year":"2002","unstructured":"Lassaigne, R., Peyronnet, S.: Approximate verification of probabilistic systems. In: [62], pp.\u00a0213\u2013214 (2002)"},{"key":"28_CR89","doi-asserted-by":"crossref","first-page":"1314","DOI":"10.1145\/2245276.2231984","volume-title":"Proceedings of the 27th Annual ACM Symposium on Applied Computing, SAC \u201912","author":"R. Lassaigne","year":"2012","unstructured":"Lassaigne, R., Peyronnet, S.: Approximate planning and verification for large Markov decision processes. In: Proceedings of the 27th Annual ACM Symposium on Applied Computing, SAC \u201912, pp.\u00a01314\u20131319. ACM, New York (2012)"},{"key":"28_CR90","volume-title":"Distributed Algorithms","author":"N. Lynch","year":"1996","unstructured":"Lynch, N.: Distributed Algorithms. Morgan Kaufmann, San Francisco (1996)"},{"key":"28_CR91","series-title":"LNCS","first-page":"292","volume-title":"Proc. LPAR 2002","author":"A. McIver","year":"2002","unstructured":"McIver, A., Morgan, C.: Games, probability and the quantitative \u03bc$\\mu$-calculus qM\u03bc$\\mu$. In: Baaz, M., Voronkov, A. (eds.) Proc. LPAR 2002. LNCS, vol.\u00a02514, pp.\u00a0292\u2013310. Springer, Heidelberg (2002)"},{"key":"28_CR92","series-title":"LNCS","first-page":"5","volume-title":"Proc. CMSB 2013","author":"L. Mikeev","year":"2013","unstructured":"Mikeev, L., Sandmann, W., Wolf, V.: Numerical approximation of rare event probabilities in biochemically reacting systems. In: Gupta, A., Henzinger, T.A. (eds.) Proc. CMSB 2013. LNCS, vol.\u00a08130, pp.\u00a05\u201318. Springer, Heidelberg (2013)"},{"issue":"4","key":"28_CR93","first-page":"1","volume":"8","author":"M. Mio","year":"2012","unstructured":"Mio, M.: Probabilistic modal \u03bc$\\mu$-calculus with independent product. Log. Methods Comput. Sci. 8(4), 1\u201336 (2012)","journal-title":"Log. Methods Comput. Sci."},{"key":"28_CR94","first-page":"202","volume-title":"Proc. 3rd Workshop on Automated Verification of Critical Systems (AVoCS\u201903), Technical Report DSSE-TR-2003-2, University of Southampton","author":"G. Norman","year":"2003","unstructured":"Norman, G., Parker, D., Kwiatkowska, M., Shukla, S., Gupta, R.: Using probabilistic model checking for dynamic power management. In: Leuschel, M., Gruner, S., Presti, S.L. (eds.) Proc. 3rd Workshop on Automated Verification of Critical Systems (AVoCS\u201903), Technical Report DSSE-TR-2003-2, University of Southampton, pp.\u00a0202\u2013215 (2003)"},{"issue":"2","key":"28_CR95","doi-asserted-by":"crossref","first-page":"164","DOI":"10.1007\/s10703-012-0177-x","volume":"43","author":"G. Norman","year":"2013","unstructured":"Norman, G., Parker, D., Sproston, J.: Model checking for probabilistic timed automata. Form. Methods Syst. Des. 43(2), 164\u2013190 (2013)","journal-title":"Form. Methods Syst. Des."},{"key":"28_CR96","series-title":"Cambridge Series in Statistical and Probabilistic Mathematics","volume-title":"Markov chains","author":"J.R. Norris","year":"1998","unstructured":"Norris, J.R.: Markov chains. Cambridge Series in Statistical and Probabilistic Mathematics. Cambridge University Press, Cambridge (1998)"},{"key":"28_CR97","first-page":"322","volume-title":"Proc. Annual Symposium on Logic in Computer Science (LICS)","author":"A. Pnueli","year":"1986","unstructured":"Pnueli, A., Zuck, L.: Probabilistic verification by tableaux. In: Proc. Annual Symposium on Logic in Computer Science (LICS), pp.\u00a0322\u2013331. IEEE, Piscataway (1986)"},{"key":"28_CR98","unstructured":"PRISM web site. www.prismmodelchecker.org. Accessed 20 August 2013"},{"key":"28_CR99","doi-asserted-by":"crossref","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"M. Puterman","year":"1994","unstructured":"Puterman, M.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (1994)"},{"key":"28_CR100","volume-title":"Combinatorial Optimization: Polyhedra and Efficiency","author":"A. Schrijver","year":"2003","unstructured":"Schrijver, A.: Combinatorial Optimization: Polyhedra and Efficiency. Springer, Heidelberg (2003)"},{"key":"28_CR101","unstructured":"Segala, R.: Modeling and verification of randomized distributed real-time systems. Ph.D. thesis, Massachusetts Institute of Technology (1995)"},{"key":"28_CR102","series-title":"LNCS","first-page":"481","volume-title":"Proc. CONCUR \u201994","author":"R. Segala","year":"1994","unstructured":"Segala, R., Lynch, N.: Probabilistic simulations for probabilistic processes. In: Jonsson, B., Parrow, J. (eds.) Proc. CONCUR \u201994. LNCS, vol.\u00a0836, pp.\u00a0481\u2013496. Springer, Heidelberg (1994)"},{"key":"28_CR103","series-title":"LNCS","first-page":"394","volume-title":"12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"K. Sen","year":"2006","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Model-checking Markov chains in the presence of uncertainties. In: Hermanns, H., Palsberg, J. (eds.) 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol.\u00a03920, pp.\u00a0394\u2013410. Springer, Heidelberg (2006)"},{"key":"28_CR104","series-title":"LNCS","volume-title":"Computer Aided Verification\u2014Proceedings of the 25th International Conference, CAV 2013","year":"2013","unstructured":"Sharygina, N., Veith, H. (eds.): Computer Aided Verification\u2014Proceedings of the 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13\u201319, 2013. LNCS, vol.\u00a08044. Springer, Heidelberg (2013)"},{"key":"28_CR105","first-page":"327","volume-title":"Proc. 26th IEEE Symposium on Foundations of Computer Science (FOCS)","author":"M.Y. Vardi","year":"1985","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: Proc. 26th IEEE Symposium on Foundations of Computer Science (FOCS), pp.\u00a0327\u2013338. IEEE, Piscataway (1985)"},{"key":"28_CR106","first-page":"332","volume-title":"Symposium on Logic in Computer Science (LICS\u201986)","author":"M.Y. Vardi","year":"1986","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Symposium on Logic in Computer Science (LICS\u201986), pp.\u00a0332\u2013345. IEEE, Piscataway (1986)"},{"issue":"1","key":"28_CR107","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."},{"issue":"3","key":"28_CR108","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1007\/s10009-005-0187-8","volume":"8","author":"H. Younes","year":"2006","unstructured":"Younes, H., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. Int. J. Softw. Tools Technol. Transf. 8(3), 216\u2013228 (2006)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"28_CR109","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1007\/3-540-45657-0_17","volume-title":"Proc. 14th International Conference on Computer Aided Verification (CAV)","author":"H. Younes","year":"2002","unstructured":"Younes, H., Simmons, R.: Probabilistic verification of discrete event systems using acceptance sampling. In: Brinksma, E., Larsen, K.G. (eds.) Proc. 14th International Conference on Computer Aided Verification (CAV). LNCS, vol.\u00a02404, pp.\u00a0223\u2013235. Springer, Heidelberg (2002)"},{"key":"28_CR110","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1007\/978-3-540-75596-8_16","volume-title":"Proc. 5th Int. Symp. Automated Technology for Verification and Analysis (ATVA\u201907)","author":"L. Zhang","year":"2007","unstructured":"Zhang, L., Hermanns, H.: Deciding simulations on probabilistic automata. In: Namjoshi, K., Yoneda, T., Higashino, T., Okamura, Y. (eds.) Proc. 5th Int. Symp. Automated Technology for Verification and Analysis (ATVA\u201907). LNCS, vol.\u00a04762, pp.\u00a0207\u2013222. Springer, Heidelberg (2007)"}],"container-title":["Handbook of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10575-8_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,18]],"date-time":"2019-10-18T01:45:33Z","timestamp":1571363133000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10575-8_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319105741","9783319105758"],"references-count":110,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10575-8_28","relation":{},"subject":[],"published":{"date-parts":[[2018]]}}}