{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T05:43:29Z","timestamp":1762321409667,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642198342"},{"type":"electronic","value":"9783642198359"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-19835-9_24","type":"book-chapter","created":{"date-parts":[[2011,3,14]],"date-time":"2011-03-14T11:03:16Z","timestamp":1300100596000},"page":"267-271","source":"Crossref","is-referenced-by-count":14,"title":["QUASY: Quantitative Synthesis Tool"],"prefix":"10.1007","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[]},{"given":"Barbara","family":"Jobstmann","sequence":"additional","affiliation":[]},{"given":"Rohit","family":"Singh","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P.: Performance evaluation and model checking join forces. Commun. ACM\u00a053(9) (2010)","DOI":"10.1145\/1810891.1810912"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"Behrmann, G., Bengtsson, J., David, A., Larsen, K.G., Pettersson, P., Yi, W.: Uppaal implementation secrets. In: Formal Techniques in Real-Time and Fault Tolerant Systems (2002)","DOI":"10.1007\/3-540-45739-9_1"},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02658-4_14","volume-title":"Computer Aided Verification","author":"R. Bloem","year":"2009","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 140\u2013156. Springer, Heidelberg (2009)"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Bloem, R., Greimel, K., Henzinger, T.A., Jobstmann, B.: Synthesizing robust systems. In: FMCAD (2009)","DOI":"10.1109\/FMCAD.2009.5351139"},{"key":"24_CR5","doi-asserted-by":"crossref","unstructured":"Brim, L., Chaloupka, J.: Using strategy improvement to stay alive. CoRR, 1006.1405 (2010)","DOI":"10.4204\/EPTCS.25.8"},{"key":"24_CR6","unstructured":"\u010cern\u00fd, P., Chatterjee, K., Henzinger, T., Radhakrishna, A., Singh, R.: Quantitative synthesis for concurrent programs. Technical Report IST-2010-0004, IST Austria (2010)"},{"key":"24_CR7","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":"24_CR8","volume-title":"Handbook of Markov Decision Processes: Methods and Applications","author":"E.A. Feinberg","year":"2001","unstructured":"Feinberg, E.A., Shwartz, A.: Handbook of Markov Decision Processes: Methods and Applications. Springer, Heidelberg (2001)"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"24_CR10","unstructured":"The Scala programming language, \n                    \n                      http:\/\/www.scala-lang.org\/"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Braitling, B., Becker, B., Hahn, E.M., Crouzen, P., Hermanns, H., Dhama, A., Theel, O.: Symblicit calculation of long-run averages for concurrent probabilistic systems. In: QEST (2010)","DOI":"10.1109\/QEST.2010.12"},{"issue":"1-2","key":"24_CR12","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","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-19835-9_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,21]],"date-time":"2019-05-21T07:10:40Z","timestamp":1558422640000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-19835-9_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642198342","9783642198359"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-19835-9_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}