{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:33:13Z","timestamp":1759638793446},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642401831"},{"type":"electronic","value":"9783642401848"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40184-8_20","type":"book-chapter","created":{"date-parts":[[2013,7,23]],"date-time":"2013-07-23T01:50:56Z","timestamp":1374544256000},"page":"273-287","source":"Crossref","is-referenced-by-count":16,"title":["From Model Checking to Model Measuring"],"prefix":"10.1007","author":[{"given":"Thomas A.","family":"Henzinger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Otop","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"20_CR1","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/s10817-010-9181-2","volume":"45","author":"F. Baader","year":"2010","unstructured":"Baader, F., Pe\u00f1aloza, R.: Automata-based axiom pinpointing. J. Autom. Reasoning\u00a045(2), 91\u2013129 (2010)","journal-title":"J. Autom. Reasoning"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Boker, U., Chatterjee, K., Henzinger, T.A., Kupferman, O.: Temporal specifications with accumulative values. In: LICS, pp. 43\u201352. IEEE Computer Society (2011)","DOI":"10.1109\/LICS.2011.33"},{"issue":"1","key":"20_CR3","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1016\/j.tcs.2011.08.002","volume":"413","author":"P. Cern\u00fd","year":"2012","unstructured":"Cern\u00fd, P., Henzinger, T.A., Radhakrishna, A.: Simulation distances. Theor. Comput. Sci.\u00a0413(1), 21\u201335 (2012)","journal-title":"Theor. Comput. Sci."},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Doyen, L.: Energy parity games. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010, Part II. LNCS, vol.\u00a06199, pp. 599\u2013610. Springer, Heidelberg (2010)","DOI":"10.1007\/978-3-642-14162-1_50"},{"key":"20_CR5","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Doyen, L., Edelsbrunner, H., Henzinger, T.A., Rannou, P.: Mean-payoff automaton expressions. CoRR, abs\/1006.1492 (2010)","DOI":"10.1007\/978-3-642-15375-4_19"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative languages. In: CSL, pp. 385\u2013400 (2008)","DOI":"10.1007\/978-3-540-87531-4_28"},{"key":"20_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-03409-1_2","volume-title":"Fundamentals of Computation Theory","author":"K. Chatterjee","year":"2009","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A.: Alternating weighted automata. In: Kuty\u0142owski, M., Charatonik, W., G\u0119bala, M. (eds.) FCT 2009. LNCS, vol.\u00a05699, pp. 3\u201313. Springer, Heidelberg (2009)"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"380","DOI":"10.1007\/978-3-642-14295-6_34","volume-title":"Computer Aided Verification","author":"K. Chatterjee","year":"2010","unstructured":"Chatterjee, K., Henzinger, T.A., Jobstmann, B., Singh, R.: Measuring and synthesizing systems in probabilistic environments. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 380\u2013395. Springer, Heidelberg (2010)"},{"key":"20_CR9","unstructured":"Chatterjee, K., Henzinger, T.A., Jurdzinski, M.: Mean-payoff parity games. In: LICS, pp. 178\u2013187. IEEE Computer Society (2005)"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"528","DOI":"10.1007\/3-540-45319-9_36","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H. Chockler","year":"2001","unstructured":"Chockler, H., Kupferman, O., Vardi, M.Y.: Coverage metrics for temporal logic model checking. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol.\u00a02031, pp. 528\u2013542. Springer, Heidelberg (2001)"},{"key":"20_CR11","unstructured":"Das, S., Banerjee, A., Basu, P., Dasgupta, P., Chakrabarti, P.P., Mohan, C.R., Fix, L.: Formal methods for analyzing the completeness of an assertion suite against a high-level fault model. In: VLSI Design, pp. 201\u2013206. IEEE Computer Society (2005)"},{"key":"20_CR12","first-page":"350","volume-title":"FOCS 1981","author":"D. Dolev","year":"1981","unstructured":"Dolev, D., Yao, A.C.: On the security of public key protocols. In: FOCS 1981, pp. 350\u2013357. IEEE Computer Society, Washington, DC (1981)"},{"key":"20_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4054-9","volume-title":"Competitive Markov decision processes","author":"J. Filar","year":"1996","unstructured":"Filar, J., Vrieze, K.: Competitive Markov decision processes. Springer-Verlag New York, Inc., New York (1996)"},{"key":"20_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-54430-5_93","volume-title":"CONCUR \u201991","author":"O. Grumberg","year":"1991","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. In: Groote, J.F., Baeten, J.C.M. (eds.) CONCUR 1991. LNCS, vol.\u00a0527, pp. 250\u2013265. Springer, Heidelberg (1991)"},{"key":"20_CR15","first-page":"157","volume-title":"POPL 2010","author":"T.A. Henzinger","year":"2010","unstructured":"Henzinger, T.A.: From boolean to quantitative notions of correctness. In: POPL 2010, pp. 157\u2013158. ACM, New York (2010)"},{"issue":"2","key":"20_CR16","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1002\/rnc.4590010204","volume":"1","author":"D. Hinrichsen","year":"1991","unstructured":"Hinrichsen, D., Son, N.K.: Stability radii of linear discrete-time systems and symplectic pencils. Int. J. of Robust and Nonlinear Control\u00a01(2), 79\u201397 (1991)","journal-title":"Int. J. of Robust and Nonlinear Control"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Kupferman, O., Li, W., Seshia, S.A.: A theory of mutations with applications to vacuity, coverage, and fault tolerance. In: FMCAD, pp. 1\u20139. IEEE (2008)","DOI":"10.1109\/FMCAD.2008.ECP.29"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/3-540-48320-9_27","volume-title":"CONCUR\u201999. Concurrency Theory","author":"O. Kupferman","year":"1999","unstructured":"Kupferman, O., Vardi, M.Y.: Robust satisfaction. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 383\u2013398. Springer, Heidelberg (1999)"},{"issue":"2","key":"20_CR19","doi-asserted-by":"publisher","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O. Kupferman","year":"2003","unstructured":"Kupferman, O., Vardi, M.Y.: Vacuity detection in temporal model checking. STTT\u00a04(2), 224\u2013233 (2003)","journal-title":"STTT"},{"issue":"2","key":"20_CR20","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. J. ACM\u00a047(2), 312\u2013360 (2000)","journal-title":"J. ACM"},{"issue":"1","key":"20_CR21","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1016\/0304-3975(91)90321-R","volume":"81","author":"H. Leung","year":"1991","unstructured":"Leung, H.: Limitedness theorem on finite automata with distance functions: an algebraic proof. Theor. Comput. Sci.\u00a081(1), 137\u2013145 (1991)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"20_CR22","first-page":"321","volume":"7","author":"M. Mohri","year":"2002","unstructured":"Mohri, M.: Semiring frameworks and algorithms for shortest-distance problems. Journal of Automata, Languages and Combinatorics\u00a07(3), 321\u2013350 (2002)","journal-title":"Journal of Automata, Languages and Combinatorics"},{"issue":"1&2","key":"20_CR23","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1016\/0304-3975(95)00188-3","volume":"158","author":"U. Zwick","year":"1996","unstructured":"Zwick, U., Paterson, M.: The complexity of mean payoff games on graphs. Theor. Comput. Sci.\u00a0158(1&2), 343\u2013359 (1996)","journal-title":"Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","CONCUR 2013 \u2013 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40184-8_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,19]],"date-time":"2019-07-19T03:41:14Z","timestamp":1563507674000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40184-8_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642401831","9783642401848"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40184-8_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}