{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,6]],"date-time":"2025-05-06T04:03:28Z","timestamp":1746504208994,"version":"3.40.4"},"publisher-location":"Cham","reference-count":31,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319119359"},{"type":"electronic","value":"9783319119366"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-11936-6_26","type":"book-chapter","created":{"date-parts":[[2014,10,24]],"date-time":"2014-10-24T19:12:03Z","timestamp":1414177923000},"page":"364-379","source":"Crossref","is-referenced-by-count":5,"title":["Nested Reachability Approximation for Discrete-Time Markov Chains with Univariate Parameters"],"prefix":"10.1007","author":[{"given":"Guoxin","family":"Su","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David S.","family":"Rosenblum","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1007\/11691372_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","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.) TACAS 2006. LNCS, vol.\u00a03920, pp. 394\u2013410. Springer, Heidelberg (2006)"},{"key":"26_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-540-78499-9_22","volume-title":"Foundations of Software Science and Computational Structures","author":"K. Chatterjee","year":"2008","unstructured":"Chatterjee, K., Sen, K., Henzinger, T.A.: Model-checking \u03c9-regular properties of interval markov chains. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol.\u00a04962, pp. 302\u2013317. Springer, Heidelberg (2008)"},{"key":"26_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-642-39799-8_35","volume-title":"Computer Aided Verification","author":"A. Puggelli","year":"2013","unstructured":"Puggelli, A., Li, W., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: Polynomial-time verification of PCTL properties of mDPs with convex uncertainties. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 527\u2013542. Springer, Heidelberg (2013)"},{"key":"26_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-36742-7_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Benedikt","year":"2013","unstructured":"Benedikt, M., Lenhardt, R., Worrell, J.: LTL model checking of interval markov chains. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol.\u00a07795, pp. 32\u201346. Springer, Heidelberg (2013)"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-31862-0_21","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"C. Daws","year":"2005","unstructured":"Daws, C.: Symbolic and parametric model checking of discrete-time markov chains. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol.\u00a03407, pp. 280\u2013294. Springer, Heidelberg (2005)"},{"issue":"1","key":"26_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"E. Hahn","year":"2011","unstructured":"Hahn, E., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. International Journal on Software Tools for Technology Transfer\u00a013(1), 3\u201319 (2011)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"1","key":"26_CR7","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s00165-006-0015-2","volume":"19","author":"R. Lanotte","year":"2007","unstructured":"Lanotte, R., Maggiolo-Schettini, A., Troina, A.: Parametric probabilistic transition systems for system design and analysis. Formal Aspects of Computing\u00a019(1), 93\u2013109 (2007)","journal-title":"Formal Aspects of Computing"},{"key":"26_CR8","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects of Computing\u00a06, 102\u2013111 (1994)","journal-title":"Formal Aspects of Computing"},{"issue":"7","key":"26_CR9","doi-asserted-by":"publisher","first-page":"210","DOI":"10.1016\/j.ipl.2013.01.004","volume":"113","author":"T. Chen","year":"2013","unstructured":"Chen, T., Han, T., Kwiatkowska, M.Z.: On the complexity of model checking interval-valued discrete time markov chains. Inf. Process. Lett.\u00a0113(7), 210\u2013216 (2013)","journal-title":"Inf. Process. Lett."},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-642-41202-8_20","volume-title":"Formal Methods and Software Engineering","author":"G. Su","year":"2013","unstructured":"Su, G., Rosenblum, D.S.: Asymptotic bounds for quantitative verification of perturbed probabilistic systems. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol.\u00a08144, pp. 297\u2013312. Springer, Heidelberg (2013)"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Su, G., Rosenblum, D.S.: Perturbation analysis of stochastic systems with empirical distribution parameters. In: Proceeding of the 36th International Conference on Software Engineering, ICSE 2014 (2014)","DOI":"10.1145\/2568225.2568256"},{"key":"26_CR12","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: The PRISM benchmark suite. In: Proc. 9th International Conference on Quantitative Evaluation of SysTems (QEST 2012), pp. 203\u2013204. IEEE CS Press (2012)","DOI":"10.1109\/QEST.2012.14"},{"key":"26_CR13","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press (2008)"},{"key":"26_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"218","DOI":"10.1007\/978-3-662-44584-6_16","volume-title":"CONCUR 2014 \u2013 Concurrency Theory","author":"T. Chen","year":"2014","unstructured":"Chen, T., Feng, Y., Rosenblum, D.S., Su, G.: Perturbation analysis in verification of discrete-time markov chains. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol.\u00a08704, pp. 218\u2013233. Springer, Heidelberg (2014)"},{"issue":"10","key":"26_CR15","doi-asserted-by":"publisher","first-page":"1629","DOI":"10.1109\/TCAD.2005.852033","volume":"24","author":"G. Norman","year":"2005","unstructured":"Norman, G., Parker, D., Kwiatkowska, M., Shukla, S.: Evaluating the reliability of NAND multiplexing with PRISM. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a024(10), 1629\u20131637 (2005)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"26_CR16","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":"26_CR17","unstructured":"MATLAB: version 8.0. The MathWorks Inc., Natick, Massachusetts (R2012b)"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"Hahn, E.M., Han, T., Zhang, L.: Synthesis for PCTL in parametric Markov decision processes. In: NASA Formal Methods, pp. 146\u2013161 (2011)","DOI":"10.1007\/978-3-642-20398-5_12"},{"key":"26_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-319-10696-0_31","volume-title":"Quantitative Evaluation of Systems","author":"N. Jansen","year":"2014","unstructured":"Jansen, N., Corzilius, F., Volk, M., Wimmer, R., \u00c1brah\u00e1m, E., Katoen, J.-P., Becker, B.: Accelerating parametric probabilistic verification. In: Norman, G., Sanders, W. (eds.) QEST 2014. LNCS, vol.\u00a08657, pp. 404\u2013420. Springer, Heidelberg (2014)"},{"key":"26_CR20","first-page":"341","volume-title":"Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011","author":"A. Filieri","year":"2011","unstructured":"Filieri, A., Ghezzi, C., Tamburrelli, G.: Run-time efficient probabilistic model checking. In: Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, pp. 341\u2013350. ACM, New York (2011)"},{"issue":"2","key":"26_CR21","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1023\/A:1014745904458","volume":"8","author":"I. Kozine","year":"2002","unstructured":"Kozine, I., Utkin, L.V.: Interval-valued finite markov chains. Reliable Computing\u00a08(2), 97\u2013113 (2002)","journal-title":"Reliable Computing"},{"key":"26_CR22","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: International conference on Logics in Computer Science (LICS), pp. 266\u2013277 (1991)","DOI":"10.1109\/LICS.1991.151651"},{"key":"26_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-33512-9_10","volume-title":"Reachability Problems","author":"K. Ghorbal","year":"2012","unstructured":"Ghorbal, K., Duggirala, P.S., Kahlon, V., Ivan\u010di\u0107, F., Gupta, A.: Efficient probabilistic model checking of systems with ranged probabilities. In: Finkel, A., Leroux, J., Potapov, I. (eds.) RP 2012. LNCS, vol.\u00a07550, pp. 107\u2013120. Springer, Heidelberg (2012)"},{"issue":"2","key":"26_CR24","doi-asserted-by":"publisher","first-page":"401","DOI":"10.2307\/3212261","volume":"5","author":"P.J. Schweitzer","year":"1968","unstructured":"Schweitzer, P.J.: Perturbation theory and finite Markov chains. Journal of Applied Probability\u00a05(2), 401\u2013413 (1968)","journal-title":"Journal of Applied Probability"},{"key":"26_CR25","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/S0024-3795(01)00320-2","volume":"335","author":"G.E. Cho","year":"2000","unstructured":"Cho, G.E., Meyer, C.D.: Comparison of perturbation bounds for the stationary distribution of a Markov chain. Linear Algebra Appl.\u00a0335, 137\u2013150 (2000)","journal-title":"Linear Algebra Appl."},{"issue":"1","key":"26_CR26","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1239\/jap\/1044476830","volume":"40","author":"E. Solan","year":"2003","unstructured":"Solan, E., Vieille, N.: Perturbed Markov chains. J. Applied Prob.\u00a040(1), 107\u2013122 (2003)","journal-title":"J. Applied Prob."},{"key":"26_CR27","doi-asserted-by":"crossref","unstructured":"Heidergott, B.: Perturbation analysis of Markov chains. In: 9th International Workshop on Discrete Event Systems, WODES 2008, pp. 99\u2013104 (2008)","DOI":"10.1109\/WODES.2008.4605929"},{"key":"26_CR28","unstructured":"Murdock, J.A.: Perturbation: Theory and Method. John Wiley & Sons, Inc. (1991)"},{"key":"26_CR29","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J.E. Hopcroft","year":"2006","unstructured":"Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation, 3rd edn. Addison-Wesley Longman Publishing Co., Inc, Boston (2006)","edition":"3"},{"key":"26_CR30","unstructured":"Verification, Model Checking, and Abstract Interpretation (2004)"},{"key":"26_CR31","doi-asserted-by":"crossref","unstructured":"Agrawal, M., Akshay, S., Genest, B., Thiagarajan, P.S.: Approximate verification of the symbolic dynamics of markov chains. In: International conference on Logics in Computer Science (LICS), pp. 55\u201364 (2012)","DOI":"10.1109\/LICS.2012.17"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-11936-6_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,5]],"date-time":"2025-05-05T13:09:07Z","timestamp":1746450547000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-11936-6_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319119359","9783319119366"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-11936-6_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}