{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T18:13:45Z","timestamp":1725732825265},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642387081"},{"type":"electronic","value":"9783642387098"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-662-44602-7_17","type":"book-chapter","created":{"date-parts":[[2014,8,22]],"date-time":"2014-08-22T21:18:40Z","timestamp":1408742320000},"page":"207-221","source":"Crossref","is-referenced-by-count":3,"title":["Parametric LTL on Markov Chains"],"prefix":"10.1007","author":[{"given":"Souymodip","family":"Chakraborty","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","doi-asserted-by":"crossref","unstructured":"Vardi, M.Y.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS, pp. 327\u2013338. IEEE Computer Society (1985)","DOI":"10.1109\/SFCS.1985.12"},{"issue":"4","key":"17_CR2","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. J. ACM\u00a042(4), 857\u2013907 (1995)","journal-title":"J. ACM"},{"key":"17_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"361","DOI":"10.1007\/978-3-540-39813-4_26","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"J.M. Couvreur","year":"2003","unstructured":"Couvreur, J.M., Saheb, N., Sutre, G.: An optimal automata approach to LTL model checking of probabilistic systems. In: Vardi, M.Y., Voronkov, A. (eds.) LPAR 2003. LNCS, vol.\u00a02850, pp. 361\u2013375. Springer, Heidelberg (2003)"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"559","DOI":"10.1007\/978-3-642-39799-8_37","volume-title":"Computer Aided Verification","author":"K. Chatterjee","year":"2013","unstructured":"Chatterjee, K., Gaiser, A., Kret\u00ednsk\u00fd, J.: Automata with generalized Rabin pairs for probabilistic model checking and LTL synthesis. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol.\u00a08044, pp. 559\u2013575. Springer, Heidelberg (2013)"},{"issue":"3","key":"17_CR5","doi-asserted-by":"publisher","first-page":"388","DOI":"10.1145\/377978.377990","volume":"2","author":"R. Alur","year":"2001","unstructured":"Alur, R., Etessami, K., La Torre, S., Peled, D.: Parametric temporal logic for \u201dmodel measuring\u201d. ACM Trans. Comput. Log.\u00a02(3), 388\u2013407 (2001)","journal-title":"ACM Trans. Comput. Log."},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"Han, T., Katoen, J.P., Mereacre, A.: Approximate parameter synthesis for probabilistic time-bounded reachability. In: IEEE Real-Time Systems Symposium (RTSS), pp. 173\u2013182. IEEE Computer Society (2008)","DOI":"10.1109\/RTSS.2008.19"},{"key":"17_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-20398-5_12","volume-title":"NASA Formal Methods","author":"E.M. Hahn","year":"2011","unstructured":"Hahn, E.M., Han, T., Zhang, L.: Synthesis for PCTL in parametric markov decision processes. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol.\u00a06617, pp. 146\u2013161. Springer, Heidelberg (2011)"},{"key":"17_CR8","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":"17_CR9","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. LNCS, vol.\u00a07795, pp. 32\u201346. Springer, Heidelberg (2013)"},{"issue":"1","key":"17_CR10","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"E.M. Hahn","year":"2011","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. STTT\u00a013(1), 3\u201319 (2011)","journal-title":"STTT"},{"key":"17_CR11","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)"},{"key":"17_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/978-3-642-15769-1_24","volume-title":"Static Analysis","author":"J.P. Katoen","year":"2010","unstructured":"Katoen, J.P., McIver, A., Meinicke, L., Morgan, C.C.: Linear-invariant generation for probabilistic programs: In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 390\u2013406. Springer, Heidelberg (2010)"},{"key":"17_CR13","doi-asserted-by":"crossref","unstructured":"Benedikt, M., Lenhardt, R., Worrell, J.: Two variable vs. linear temporal logic in model checking and games. Logical Methods in Computer Science\u00a09(2) (2013)","DOI":"10.2168\/LMCS-9(2:4)2013"},{"key":"17_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-642-37075-5_23","volume-title":"Foundations of Software Science and Computation Structures","author":"M. Ummels","year":"2013","unstructured":"Ummels, M., Baier, C.: Computing quantiles in Markov reward models. In: Pfenning, F. (ed.) FOSSACS 2013. LNCS, vol.\u00a07794, pp. 353\u2013368. Springer, Heidelberg (2013)"},{"issue":"1","key":"17_CR15","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/963927.963928","volume":"5","author":"R. Alur","year":"2004","unstructured":"Alur, R., La Torre, S.: Deterministic generators and games for LTL fragments. ACM Trans. Comput. Log.\u00a05(1), 1\u201325 (2004)","journal-title":"ACM Trans. Comput. Log."},{"key":"17_CR16","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press (2008)"},{"key":"17_CR17","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1016\/j.tcs.2012.07.039","volume":"493","author":"M. Zimmermann","year":"2013","unstructured":"Zimmermann, M.: Optimal bounds in parametric LTL games. Theor. Comput. Sci.\u00a0493, 30\u201345 (2013)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/3-540-60915-6_6","volume-title":"Logics for Concurrency","author":"M.Y. Vardi","year":"1996","unstructured":"Vardi, M.Y.: An automata-theoretic approach to linear temporal logic. In: Moller, F., Birtwistle, G. (eds.) Logics for Concurrency. LNCS, vol.\u00a01043, pp. 238\u2013266. Springer, Heidelberg (1996)"},{"key":"17_CR19","doi-asserted-by":"publisher","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. Information and Computation\u00a0115, 1\u201337 (1994)","journal-title":"Information and Computation"}],"container-title":["Lecture Notes in Computer Science","Advanced Information Systems Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-44602-7_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,14]],"date-time":"2019-08-14T02:36:16Z","timestamp":1565750176000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-44602-7_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642387081","9783642387098"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-44602-7_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}