{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T10:52:12Z","timestamp":1672570332289},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2015,5,13]],"date-time":"2015-05-13T00:00:00Z","timestamp":1431475200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2016,6]]},"DOI":"10.1007\/s00236-015-0237-y","type":"journal-article","created":{"date-parts":[[2015,5,12]],"date-time":"2015-05-12T01:18:07Z","timestamp":1431393487000},"page":"425-457","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Synthesizing efficient systems in probabilistic environments"],"prefix":"10.1007","volume":"53","author":[{"given":"Christian","family":"von Essen","sequence":"first","affiliation":[]},{"given":"Barbara","family":"Jobstmann","sequence":"additional","affiliation":[]},{"given":"David","family":"Parker","sequence":"additional","affiliation":[]},{"given":"Rahul","family":"Varshneya","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,5,13]]},"reference":[{"issue":"2\/3","key":"237_CR1","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1023\/A:1008699807402","volume":"10","author":"I Bahar","year":"1997","unstructured":"Bahar, I., Frohm, E., Gaona, C., Hachtel, G., Macii, E., Pardo, A., Somenzi, F.: Algebraic decision diagrams and their applications. Form. Methods Syst. Des. 10(2\/3), 171\u2013206 (1997)","journal-title":"Form. Methods Syst. Des."},{"key":"237_CR2","doi-asserted-by":"crossref","unstructured":"Baier, C., Clarke, E., Hartonas-Garmhausen, V., Kwiatkowska, M., Ryan, M.: Symbolic model checking for probabilistic processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) Proceedings of 24th International Colloquium on Automata, Languages and Programming (ICALP\u201997), volume 1256 of LNCS, pp. 430\u2013440. Springer, New York (1997)","DOI":"10.1007\/3-540-63165-8_199"},{"key":"237_CR3","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press, Berlin (2008)"},{"key":"237_CR4","first-page":"140","volume-title":"CAV, volume 5643 of LNCS","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, volume 5643 of LNCS, pp. 140\u2013156. Springer, Berlin (2009)"},{"key":"237_CR5","doi-asserted-by":"crossref","unstructured":"Bloem, R., Gabow, H., Somenzi, F.: An algorithm for strongly connected component analysis in n log n symbolic steps. In: Proceedings of 3rd International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201900), pp. 37\u201354 (2000)","DOI":"10.1007\/3-540-40922-X_4"},{"key":"237_CR6","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":"237_CR7","doi-asserted-by":"crossref","unstructured":"Br\u00e1zdil, T., Bro\u017eek, V., Chatterjee, K., Forejt, V.Ku\u010dera, A.: Two views on multiple mean-payoff objectives inMarkov decision processes. In: LICS, pp. 33\u201342. IEEE ComputerSociety (2011)","DOI":"10.1109\/LICS.2011.10"},{"issue":"8","key":"237_CR8","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"issue":"2","key":"237_CR9","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: $$10^{20}$$ 10 20 states and beyond. Inf. Comput. 98(2), 142\u2013170 (1992)","journal-title":"Inf. Comput."},{"key":"237_CR10","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, M.: Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In: Proceedings of 22nd Annual ACM-SIAM Symposium on Discrete Algorithms (SODA\u201911), pp. 1318\u20131336 (2011)","DOI":"10.1137\/1.9781611973082.101"},{"key":"237_CR11","first-page":"380","volume-title":"CAV, volume 6174 of LNCS","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, volume 6174 of LNCS, pp. 380\u2013395. Springer, Berlin (2010)"},{"key":"237_CR12","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Majumdar, R., Henzinger, T.: Markov decision processes with multiple objectives. In: Proceedings of 23rd International Symposium on Theoretical Aspects of Computer Science (STACS\u201906), volume 3884 of LNCS, pp. 325\u2013336. Springer (2006)","DOI":"10.1007\/11672142_26"},{"key":"237_CR13","unstructured":"de Alfaro, L.: Formal Verification of Probabilistic Systems. PhD thesis, Stanford University (1997)"},{"issue":"1","key":"237_CR14","doi-asserted-by":"crossref","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. Manage. Sci. 9(1), 16\u201324 (1962)","journal-title":"Manage. Sci."},{"key":"237_CR15","doi-asserted-by":"crossref","unstructured":"Etessami, K., Kwiatkowska, M., Vardi, M., Yannakakis, M.: Multi-objective model checking of Markov decision processes. In: Proceedings of 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201907), volume 4424 of LNCS, pp. 50\u201365. Springer (2007)","DOI":"10.1007\/978-3-540-71209-1_6"},{"key":"237_CR16","first-page":"112","volume-title":"TACAS, volume 6605 of LNCS","author":"V Forejt","year":"2011","unstructured":"Forejt, V., Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Quantitative multi-objective verification for probabilistic systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS, volume 6605 of LNCS, pp. 112\u2013127. Springer, Berlin (2011)"},{"issue":"2\/3","key":"237_CR17","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1023\/A:1008647823331","volume":"10","author":"M Fujita","year":"1997","unstructured":"Fujita, M., Mcgeer, P.C., Yang, J.C.Y.: Multi-terminal binary decision diagrams: an efficient data structure for matrix representation. Form. Methods Syst. Des. V 10(2\/3), 149\u2013169 (1997)","journal-title":"Form. Methods Syst. Des. V"},{"key":"237_CR18","doi-asserted-by":"crossref","unstructured":"Gimbert, H.: Pure stationary optimal strategies in Markov decision processes. In: STACS\u201907, pp. 200\u2013211. Springer (2007)","DOI":"10.1007\/978-3-540-70918-3_18"},{"issue":"12","key":"237_CR19","doi-asserted-by":"crossref","first-page":"1479","DOI":"10.1109\/43.552081","volume":"15","author":"G Hachtel","year":"1996","unstructured":"Hachtel, G., Macii, E., Pardo, A., Somenzi, F.: Markovian analysis of large finite state machines. Comput. Aided Des. Integr. Circuits Syst. IEEE Trans. 15(12), 1479\u20131493 (1996)","journal-title":"Comput. Aided Des. Integr. Circuits Syst. IEEE Trans."},{"key":"237_CR20","doi-asserted-by":"crossref","DOI":"10.1002\/0470841923","volume-title":"Performance of Computer Communication Systems\u2014A Model-Based Approach","author":"BR Haverkort","year":"1998","unstructured":"Haverkort, B.R.: Performance of Computer Communication Systems\u2014A Model-Based Approach. Wiley, New York (1998)"},{"key":"237_CR21","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1002\/nav.3800030108","volume":"3","author":"JR Isbell","year":"1956","unstructured":"Isbell, J.R., Marlow, W.H.: Attrition games. Nav. Res. Logist. Q. 3, 71\u201394 (1956)","journal-title":"Nav. Res. Logist. Q."},{"key":"237_CR22","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-9455-6","volume-title":"Denumerable Markov Chains","author":"J Kemeny","year":"1976","unstructured":"Kemeny, J., Snell, J., Knapp, A.: Denumerable Markov Chains, 2nd edn. Springer, New York (1976)","edition":"2"},{"key":"237_CR23","first-page":"52","volume-title":"TACAS, volume 2280 of LNCS","author":"M Kwiatkowska","year":"2002","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: a hybrid approach. In: Katoen, J.-P., Stevens, P. (eds.) TACAS, volume 2280 of LNCS, pp. 52\u201366. Springer, Berlin (2002)"},{"key":"237_CR24","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of probabilistic real-time systems. In: Proceedings of 23rd International Conference on Computer Aided Verification (CAV\u201911), volume 6806 of LNCS, pp. 585\u2013591. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"key":"237_CR25","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker. D.: The PRISM benchmark suite. In: Proceedings of 9th International Conference on Quantitative Evaluation of Systems (QEST\u201912), pp. 203\u2013204. IEEE CS Press (2012)","DOI":"10.1109\/QEST.2012.14"},{"issue":"1","key":"237_CR26","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/s10703-006-0005-2","volume":"29","author":"M Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Form. Methods Syst. Des. 29(1), 33\u201378 (2006)","journal-title":"Form. Methods Syst. Des."},{"key":"237_CR27","doi-asserted-by":"crossref","unstructured":"Lehmann, D.J., Rabin, M. O.: On the advantages of free choice: a symmetric and fully distributed solution to the dining philosophers problem. In: POPL (1981)","DOI":"10.1145\/567532.567547"},{"key":"237_CR28","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems\u2014Safety","author":"Z Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems\u2014Safety. Springer, Berlin (1995)"},{"issue":"2","key":"237_CR29","doi-asserted-by":"crossref","first-page":"160","DOI":"10.1007\/s00165-005-0062-0","volume":"17","author":"G Norman","year":"2005","unstructured":"Norman, G., Parker, D., Kwiatkowska, M., Shukla, S.K., Gupta, R.: Using probabilistic model checking for dynamic power management. Formal Asp. Comput. 17(2), 160\u2013176 (2005)","journal-title":"Formal Asp. Comput."},{"key":"237_CR30","volume-title":"Markov Chains","author":"J Norris","year":"2003","unstructured":"Norris, J.: Markov Chains. Cambridge University Press, Cambridge (2003)"},{"key":"237_CR31","unstructured":"Parker, D.: Implementation of Symbolic Model Checking for Probabilistic Systems. PhD thesis, University of Birmingham (2002)"},{"key":"237_CR32","volume-title":"NIPS","author":"R Parr","year":"1997","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, Cambridge (1997)"},{"key":"237_CR33","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":"237_CR34","doi-asserted-by":"crossref","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"ML Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley-Interscience, Chichester (1994)"},{"issue":"1","key":"237_CR35","doi-asserted-by":"crossref","first-page":"66","DOI":"10.1016\/0022-0000(82)90010-1","volume":"25","author":"MO Rabin","year":"1982","unstructured":"Rabin, M.O.: N-process mutual exclusion with bounded waiting by 4 $$log_2 n$$ l o g 2 n -valued shared variable. J. Comput. Syst. Sci. 25(1), 66\u201375 (1982)","journal-title":"J. Comput. Syst. Sci."},{"key":"237_CR36","doi-asserted-by":"crossref","DOI":"10.1002\/047001363X","volume-title":"A First Course in Stochastic Models","author":"HC Tijms","year":"2003","unstructured":"Tijms, H.C.: A First Course in Stochastic Models. Wiley, Chichester (2003)"},{"key":"237_CR37","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.) Proceedings International Workshop on Interactions, Games and Protocols, iWIGP 2011, Saarbr\u00fccke, Germany, 27th March 2011. EPTCS, vol. 50, pp. 17\u201332 (2011)","DOI":"10.4204\/EPTCS.50.2"},{"key":"237_CR38","doi-asserted-by":"crossref","unstructured":"von Essen, C., Jobstmann, B.: Synthesizing efficient controllers. In: International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), pp. 428\u2013444 (2012)","DOI":"10.1007\/978-3-642-27940-9_28"},{"key":"237_CR39","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":"237_CR40","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. IEEE Computer Society (2008)","DOI":"10.1109\/QEST.2008.14"},{"key":"237_CR41","doi-asserted-by":"crossref","unstructured":"Yue, H., Bohnenkamp, H.C., Katoen, J.-P.: Analyzing energy consumption in a gossiping MAC protocol. In: M\u00fcller-Clostermann, B., Echtle, K., Rathgeb, E.P. (eds.) MMB\/DFT, volume 5987 of LNCS, pp. 107\u2013119. Springer (2010)","DOI":"10.1007\/978-3-642-12104-3_10"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0237-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-015-0237-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-015-0237-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,24]],"date-time":"2019-08-24T19:52:33Z","timestamp":1566676353000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-015-0237-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5,13]]},"references-count":41,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2016,6]]}},"alternative-id":["237"],"URL":"https:\/\/doi.org\/10.1007\/s00236-015-0237-y","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,5,13]]}}}