{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,30]],"date-time":"2026-08-30T01:07:23Z","timestamp":1788052043503,"version":"build-2784847793"},"reference-count":32,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2010,4,7]],"date-time":"2010-04-07T00:00:00Z","timestamp":1270598400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2011,1]]},"DOI":"10.1007\/s10009-010-0146-x","type":"journal-article","created":{"date-parts":[[2010,4,7]],"date-time":"2010-04-07T03:06:56Z","timestamp":1270609616000},"page":"3-19","source":"Crossref","is-referenced-by-count":128,"title":["Probabilistic reachability for parametric Markov models"],"prefix":"10.1007","volume":"13","author":[{"given":"Ernst Moritz","family":"Hahn","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Holger","family":"Hermanns","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lijun","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2010,4,7]]},"reference":[{"key":"146_CR1","doi-asserted-by":"crossref","unstructured":"Abbott, J.: The design of CoCoALib. In: ICMS, pp. 205\u2013215 (2006)","DOI":"10.1007\/11832225_18"},{"issue":"4","key":"146_CR2","doi-asserted-by":"crossref","first-page":"22","DOI":"10.1145\/1059816.1059821","volume":"32","author":"C. Baier","year":"2005","unstructured":"Baier C., Ciesinski F., Gr\u00f6\u00dfer M.: ProbMela and verification of Markov decision processes. SIGMETRICS 32(4), 22\u201327 (2005)","journal-title":"SIGMETRICS"},{"key":"146_CR3","doi-asserted-by":"crossref","unstructured":"Baier, C., Hermanns, H.: Weak bisimulation for fully probabilistic processes. In: CAV, pp. 119\u2013130 (1997)","DOI":"10.1007\/3-540-63166-6_14"},{"issue":"2","key":"146_CR4","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/j.ic.2005.03.001","volume":"200","author":"C. Baier","year":"2005","unstructured":"Baier C., Katoen J.-P., Hermanns H., Wolf V.: Comparative branching-time semantics for Markov chains. Inf. Comput. 200(2), 149\u2013214 (2005)","journal-title":"Inf. Comput."},{"key":"146_CR5","first-page":"499","volume":"15","author":"A. Bianco","year":"1995","unstructured":"Bianco A., de Alfaro L.: Model checking of probabilistic and nondeterministic systems. FSTTCS 15, 499\u2013513 (1995)","journal-title":"FSTTCS"},{"key":"146_CR6","doi-asserted-by":"crossref","unstructured":"Bohnenkamp, H.C., van der Stok, P., Hermanns, H., Vaandrager, F.W.: Cost-optimization of the IPv4 zeroconf protocol. In: DSN, pp. 531\u2013540 (2003)","DOI":"10.1109\/DSN.2003.1209963"},{"key":"146_CR7","doi-asserted-by":"crossref","first-page":"67","DOI":"10.1109\/PGEC.1963.263416","volume":"12","author":"J.A. Brzozowski","year":"1963","unstructured":"Brzozowski J.A., Mccluskey E.J.: Signal flow graph techniques for sequential circuit state diagrams. IEEE Trans. Electron. Comp. EC 12, 67\u201376 (1963)","journal-title":"IEEE Trans. Electron. Comp. EC"},{"key":"146_CR8","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T., Sen, K.: Model-checking omega-regular properties of interval Markov chains. In: FoSSaCS, pp. 302\u2013317 (2008)","DOI":"10.1007\/978-3-540-78499-9_22"},{"key":"146_CR9","doi-asserted-by":"crossref","unstructured":"Damman, B., Han, T., Katoen, J.-P.: Regular expressions for PCTL counterexamples. In: QEST (2008)","DOI":"10.1109\/QEST.2008.11"},{"key":"146_CR10","doi-asserted-by":"crossref","unstructured":"Daws, C.: Symbolic and parametric model checking of discrete-time Markov Chains. In: ICTAC, pp. 280\u2013294 (2004)","DOI":"10.1007\/978-3-540-31862-0_21"},{"issue":"6","key":"146_CR11","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1016\/S0020-0190(03)00343-0","volume":"87","author":"S. Derisavi","year":"2003","unstructured":"Derisavi S., Hermanns H., Sanders W.H.: Optimal state-space lumping in Markov chains. Inf. Process. Lett. 87(6), 309\u2013315 (2003)","journal-title":"Inf. Process. Lett."},{"key":"146_CR12","doi-asserted-by":"crossref","unstructured":"Fecher, H., Leucker, M., Wolf, V.: Don\u2019t know in probabilistic Systems. In: SPIN, pp. 71\u201388 (2006)","DOI":"10.1007\/11691617_5"},{"key":"146_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/b102438","volume-title":"Algorithms for Computer Algebra","author":"K.O. Geddes","year":"1992","unstructured":"Geddes K.O., Czapor S.R., Labahn G.: Algorithms for Computer Algebra. Kluwer, Dordrecht (1992)"},{"key":"146_CR14","doi-asserted-by":"crossref","unstructured":"Gruber, H., Johannsen, J.: Optimal lower bounds on regular expression size using communication complexity. In: FoSSaCS, pp. 273\u2013286 (2008)","DOI":"10.1007\/978-3-540-78499-9_20"},{"key":"146_CR15","doi-asserted-by":"crossref","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PARAM: a model checker for parametric Markov models. In: CAV, 2010 (to appear)","DOI":"10.1007\/978-3-642-14295-6_56"},{"key":"146_CR16","doi-asserted-by":"crossref","unstructured":"Han, T., Katoen, J.-P., Mereacre, A.: Approximate parameter synthesis for probabilistic time-bounded reachability. In: RTSS, pp. 173\u2013182 (2008)","DOI":"10.1109\/RTSS.2008.19"},{"issue":"5","key":"146_CR17","first-page":"512","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson H., Jonsson B.: A logic for reasoning about time and reliability. FAC 6(5), 512\u2013535 (1994)","journal-title":"FAC"},{"key":"146_CR18","doi-asserted-by":"crossref","unstructured":"Helmink, L., Sellink, A., Vaandrager, F.W.: Proof-checking a data link protocol. In: TYPES, vol. 806, pp. 127\u2013165. Springer, Heidelberg (1994)","DOI":"10.1007\/3-540-58085-9_75"},{"key":"146_CR19","doi-asserted-by":"crossref","unstructured":"Hinton, A., Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM: a tool for automatic verification of probabilistic systems. In: TACAS, pp. 441\u2013444 (2006)","DOI":"10.1007\/11691372_29"},{"issue":"1","key":"146_CR20","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1145\/568438.568455","volume":"32","author":"J.E. Hopcroft","year":"2001","unstructured":"Hopcroft J.E., Motwani R., Ullman J.D.: Introduction to automata theory, languages, and computation, 2nd edn. SIGACT News 32(1), 60\u201365 (2001)","journal-title":"SIGACT News"},{"issue":"53","key":"146_CR21","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/S1567-8326(02)00037-1","volume":"52","author":"T. Hune","year":"2002","unstructured":"Hune T., Romijn J., Stoelinga M., Vaandrager F.W.: Linear parametric model checking of timed automata. J. Log. Algebra Program. 52(53), 183\u2013220 (2002)","journal-title":"J. Log. Algebra Program."},{"issue":"9","key":"146_CR22","doi-asserted-by":"crossref","first-page":"1649","DOI":"10.1109\/49.62852","volume":"8","author":"O.C. Ibe","year":"1990","unstructured":"Ibe O.C., Trivedi K.S.: Stochastic petri net models of polling systems. IEEE J. Selected Areas Commun. 8(9), 1649\u20131657 (1990)","journal-title":"IEEE J. Selected Areas Commun."},{"key":"146_CR23","doi-asserted-by":"crossref","unstructured":"Jonsson, B., Larsen, K.G.: Specification and refinement of probabilistic processes. In: LICS, pp. 266\u2013277. IEEE Computer Society, New York (1991)","DOI":"10.1109\/LICS.1991.151651"},{"key":"146_CR24","doi-asserted-by":"crossref","unstructured":"Katoen, J.-P., Klink, D., Leucker, M., Wolf, V.: Three-valued abstraction for continuous-time markov chains. In: CAV, vol. 4590, pp. 311\u2013324. Springer, Heidelberg (2007)","DOI":"10.1007\/978-3-540-73368-3_37"},{"issue":"2","key":"146_CR25","doi-asserted-by":"crossref","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 Comput. 8(2), 97\u2013113 (2002)","journal-title":"Reliable Comput."},{"key":"146_CR26","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Stochastic model checking. In: SFM, pp. 220\u2013270 (2007)","DOI":"10.1007\/978-3-540-72522-0_6"},{"issue":"1","key":"146_CR27","first-page":"93","volume":"19","author":"R. Lanotte","year":"2007","unstructured":"Lanotte R., Maggiolo-Schettini A., Troina A.: Parametric probabilistic transition systems for system design and analysis. FAC 19(1), 93\u2013109 (2007)","journal-title":"FAC"},{"issue":"1","key":"146_CR28","doi-asserted-by":"crossref","first-page":"53","DOI":"10.1007\/BF01843570","volume":"1","author":"A. Pnueli","year":"1986","unstructured":"Pnueli A., Zuck L.: Verification of multiprocess probabilistic protocols. Distrib. Comput. 1(1), 53\u201372 (1986)","journal-title":"Distrib. Comput."},{"issue":"1","key":"146_CR29","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1145\/290163.290168","volume":"1","author":"M.K. Reiter","year":"1998","unstructured":"Reiter M.K., Rubin A.D.: Crowds: anonymity for web transactions. ACM Trans. Inf. Syst. Secur. 1(1), 66\u201392 (1998)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"146_CR30","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Model-checking Markov chains in the presence of uncertainties. In: TACAS, pp. 394\u2013410 (2006)","DOI":"10.1007\/11691372_26"},{"key":"146_CR31","volume-title":"Introduction to the Numerical Solution of Markov Chains","author":"W.J. Stewart","year":"1994","unstructured":"Stewart W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton University Press, Princeton (1994)"},{"key":"146_CR32","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Derisavi, S., Hermanns, H.: Symbolic partition refinement with dynamic balancing of time and space. In: QEST, pp. 65\u201374 (2008)","DOI":"10.1109\/QEST.2008.14"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0146-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-010-0146-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-010-0146-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T07:25:26Z","timestamp":1559114726000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-010-0146-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,4,7]]},"references-count":32,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,1]]}},"alternative-id":["146"],"URL":"https:\/\/doi.org\/10.1007\/s10009-010-0146-x","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,4,7]]}}}