{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T15:26:55Z","timestamp":1742916415750,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642279393"},{"type":"electronic","value":"9783642279409"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"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":[[2012]]},"DOI":"10.1007\/978-3-642-27940-9_28","type":"book-chapter","created":{"date-parts":[[2012,1,19]],"date-time":"2012-01-19T02:29:29Z","timestamp":1326940169000},"page":"428-444","source":"Crossref","is-referenced-by-count":7,"title":["Synthesizing Efficient Controllers"],"prefix":"10.1007","author":[{"given":"Christian","family":"von Essen","sequence":"first","affiliation":[]},{"given":"Barbara","family":"Jobstmann","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"28_CR1","unstructured":"Baier, C., Katoen, J.-P.: Principles of model checking. MIT Press (2008)"},{"key":"28_CR2","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":"28_CR3","doi-asserted-by":"crossref","unstructured":"Bloem, R., Greimel, K., Henzinger, T.A., Jobstmann, B.: Synthesizing robust systems. In: FMCAD, pp. 85\u201392. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351139"},{"key":"28_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/978-3-540-87531-4_28","volume-title":"Computer Science Logic","author":"K. Chatterjee","year":"2008","unstructured":"Chatterjee, K., Doyen, L., Henzinger, T.A.: Quantitative Languages. In: Kaminski, M., Martini, S. (eds.) CSL 2008. LNCS, vol.\u00a05213, pp. 385\u2013400. Springer, Heidelberg (2008)"},{"key":"28_CR5","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":"28_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/BFb0032043","volume-title":"Automata, Languages and Programming","author":"C. Courcoubetis","year":"1990","unstructured":"Courcoubetis, C., Yannakakis, M.: Markov Decision Processes and Regular Events (Extended Abstract). In: Paterson, M. (ed.) ICALP 1990. LNCS, vol.\u00a0443, pp. 336\u2013349. Springer, Heidelberg (1990)"},{"key":"28_CR7","unstructured":"de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford University (1997)"},{"issue":"1","key":"28_CR8","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1287\/mnsc.9.1.16","volume":"9","author":"C. Derman","year":"1962","unstructured":"Derman, C.: On sequential decisions and markov chains. Management Science\u00a09(1), 16\u201324 (1962)","journal-title":"Management Science"},{"key":"28_CR9","doi-asserted-by":"crossref","unstructured":"Haverkort, B.R.: Performance of computer communication systems - a model-based approach. Wiley (1998)","DOI":"10.1002\/0470841923"},{"issue":"4","key":"28_CR10","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1145\/1530873.1530882","volume":"36","author":"D.P.M.Z. Kwiatkowska","year":"2009","unstructured":"Kwiatkowska, D.P.M.Z., Norman, G.: PRISM: probabilistic model checking for performance and reliability analysis. SIGMETRICS Performance Evaluation Review\u00a036(4), 40\u201345 (2009)","journal-title":"SIGMETRICS Performance Evaluation Review"},{"key":"28_CR11","unstructured":"Parr, R., Russell, S.J.: Reinforcement learning with hierarchies of machines. In: Jordan, M.I., Kearns, M.J., Solla, S.A. (eds.) NIPS. The MIT Press (1997)"},{"key":"28_CR12","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"28_CR13","doi-asserted-by":"crossref","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley-Interscience (April 1994)","DOI":"10.1002\/9780470316887"},{"key":"28_CR14","doi-asserted-by":"crossref","unstructured":"von Essen, C., Jobstmann, B.: Synthesizing systems with optimal average-case behavior for ratio objectives. In: Reich, J., Finkbeiner, B. (eds.) iWIGP. EPTCS, vol.\u00a050, pp. 17\u201332 (2011)","DOI":"10.4204\/EPTCS.50.2"},{"key":"28_CR15","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, pp. 27\u201336. IEEE Computer Society (2010)","DOI":"10.1109\/QEST.2010.12"},{"key":"28_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-12104-3_10","volume-title":"Measurement, Modelling, and Evaluation of Computing Systems and Dependability and Fault Tolerance","author":"H. Yue","year":"2010","unstructured":"Yue, H., Bohnenkamp, H., Katoen, J.-P.: Analyzing Energy Consumption in a Gossiping MAC Protocol. In: M\u00fcller-Clostermann, B., Echtle, K., Rathgeb, E.P. (eds.) MMB&DFT 2010. LNCS, vol.\u00a05987, pp. 107\u2013119. Springer, Heidelberg (2010)"},{"key":"28_CR17","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal verification of reactive systems - safety","author":"A.P.Z. Manna","year":"1995","unstructured":"Manna, A.P.Z.: Temporal verification of reactive systems - safety. Springer, Heidelberg (1995)"},{"issue":"1&2","key":"28_CR18","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","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-27940-9_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,24]],"date-time":"2019-04-24T22:53:48Z","timestamp":1556146428000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-27940-9_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642279393","9783642279409"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-27940-9_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}