{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,1,6]],"date-time":"2023-01-06T03:36:24Z","timestamp":1672976184232},"reference-count":47,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2016,2,1]],"date-time":"2016-02-01T00:00:00Z","timestamp":1454284800000},"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":[[2017,9]]},"DOI":"10.1007\/s00236-016-0255-4","type":"journal-article","created":{"date-parts":[[2016,2,1]],"date-time":"2016-02-01T04:58:29Z","timestamp":1454302709000},"page":"545-587","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Symblicit algorithms for mean-payoff and shortest path in monotonic Markov decision processes"],"prefix":"10.1007","volume":"54","author":[{"given":"Aaron","family":"Bohy","sequence":"first","affiliation":[]},{"given":"V\u00e9ronique","family":"Bruy\u00e8re","sequence":"additional","affiliation":[]},{"given":"Jean-Fran\u00e7ois","family":"Raskin","sequence":"additional","affiliation":[]},{"given":"Nathalie","family":"Bertrand","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,2,1]]},"reference":[{"issue":"2","key":"255_CR1","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1006\/inco.1996.0053","volume":"127","author":"PA Abdulla","year":"1996","unstructured":"Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Inf. Comput. 127(2), 91\u2013101 (1996)","journal-title":"Inf. Comput."},{"key":"255_CR2","doi-asserted-by":"crossref","unstructured":"Baier, C., Bertrand, N., Schnoebelen, P.: Symbolic verification of communicating systems with probabilistic message losses: liveness and fairness. In: Najm, E., Pradat-Peyre, J., Donzeau-Gouge, V. (eds.) FORTE, volume 4229 of Lecture Notes in Computer Science, pp. 212\u2013227. Springer (2006)","DOI":"10.1007\/11888116_17"},{"key":"255_CR3","doi-asserted-by":"crossref","unstructured":"Baier, C., Bertrand, N., Schnoebelen, P.: Verifying nondeterministic probabilistic channel systems against $$\\omega $$ \u03c9 -regular linear-time properties. ACM Trans. Comput. Log. 9(1), Article No. 5 (2007)","DOI":"10.1145\/1297658.1297663"},{"key":"255_CR4","volume-title":"Principles of model checking","author":"C Baier","year":"2008","unstructured":"Baier, C.: Principles of model checking. MIT Press, Cambridge (2008)"},{"issue":"2","key":"255_CR5","doi-asserted-by":"crossref","first-page":"149","DOI":"10.1016\/j.ic.2005.03.001","volume":"200","author":"C Baier","year":"2005","unstructured":"Baier, C., Katoen, J.-P., Hermanns, H., Wolf, V.: Comparative branching-time semantics for Markov chains. Inf. Comput. 200(2), 149\u2013214 (2005)","journal-title":"Inf. Comput."},{"issue":"2","key":"255_CR6","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/s10703-012-0168-y","volume":"43","author":"N Bertrand","year":"2013","unstructured":"Bertrand, N., Schnoebelen, P.: Computable fixpoints in well-structured symbolic model checking. Form. Methods Syst. Des. 43(2), 233\u2013267 (2013)","journal-title":"Form. Methods Syst. Des."},{"key":"255_CR7","volume-title":"Neuro-dynamic programming","author":"DP Bertsekas","year":"1996","unstructured":"Bertsekas, D.P., Tsitsiklis, J.: Neuro-dynamic programming. Athena Scientific, Anthropological Field Studies, Belmont (1996)"},{"issue":"3","key":"255_CR8","doi-asserted-by":"crossref","first-page":"580","DOI":"10.1287\/moor.16.3.580","volume":"16","author":"DP Bertsekas","year":"1991","unstructured":"Bertsekas, D.P., Tsitsiklis, J.N.: An analysis of stochastic shortest path problems. Math. Oper. Res. 16(3), 580\u2013595 (1991)","journal-title":"Math. Oper. Res."},{"key":"255_CR9","doi-asserted-by":"crossref","unstructured":"Blum, A.L., Langford, J.C.: Probabilistic planning in the graphplan framework. In: Biundo, S., Fox, M. (eds.) Recent Advances in AI Planning, pp. 319\u2013332. Springer (2000)","DOI":"10.1007\/10720246_25"},{"key":"255_CR10","doi-asserted-by":"crossref","unstructured":"Bohy, A., Bruy\u00e8re, V., Filiot, E., Jin, N., Raskin, J.-F.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) CAV, volume 7358 of Lecture Notes in Computer Science, pp. 652\u2013657. Springer (2012)","DOI":"10.1007\/978-3-642-31424-7_45"},{"key":"255_CR11","doi-asserted-by":"crossref","unstructured":"Bohy, A., Bruy\u00e8re, V., Filiot, E., Raskin, J.-F.: Synthesis from LTL specifications with mean-payoff objectives. CoRR, abs\/1210.3539 (2012)","DOI":"10.1007\/978-3-642-36742-7_12"},{"key":"255_CR12","doi-asserted-by":"crossref","unstructured":"Bohy, A., Bruy\u00e8re, V., Filiot, E., Raskin, J.-F.: Synthesis from LTL specifications with mean-payoff objectives. In: Piterman, N., Smolka, S.A. (eds.) TACAS, volume 7795 of Lecture Notes in Computer Science, pp. 169\u2013184. Springer (2013)","DOI":"10.1007\/978-3-642-36742-7_12"},{"key":"255_CR13","doi-asserted-by":"crossref","unstructured":"Bohy, A., Bruy\u00e8re, V., Raskin, J.: Symblicit algorithms for optimal strategy synthesis in monotonic markov decision processes. In: Chatterjee, K., Ehlers, R., Jha, S. (eds.) SYNT, volume 157 of EPTCS, pp. 51\u201367 (2014)","DOI":"10.4204\/EPTCS.157.8"},{"issue":"8","key":"255_CR14","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":"1","key":"255_CR15","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1017\/S0021900200107338","volume":"31","author":"P Buchholz","year":"1994","unstructured":"Buchholz, P.: Exact and ordinary lumpability in finite Markov chains. J. Appl. Probab. 31(1), 59\u201375 (1994)","journal-title":"J. Appl. Probab."},{"issue":"2","key":"255_CR16","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":"255_CR17","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Henzinger, T.A., Jobstmann, B., Singh, R.: In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS, volume 6605 of Lecture Notes in Computer Science. Lecture Notes in Computer Science, pp. 267\u2013271. Springer (2011)","DOI":"10.1007\/978-3-642-19835-9_24"},{"key":"255_CR18","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logic of Programs, volume 131 of Lecture Notes in Computer Science, pp. 52\u201371. Springer (1981)","DOI":"10.1007\/BFb0025774"},{"key":"255_CR19","doi-asserted-by":"crossref","unstructured":"de Alfaro, L.: Computing minimum and maximum reachability times in probabilistic systems. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR, volume 1664 of Lecture Notes in Computer Science, pp. 66\u201381. Springer (1999)","DOI":"10.1007\/3-540-48320-9_7"},{"issue":"6","key":"255_CR20","doi-asserted-by":"crossref","first-page":"309","DOI":"10.1016\/S0020-0190(03)00343-0","volume":"87","author":"S Derisavi","year":"2003","unstructured":"Derisavi, S., Hermanns, H., Sanders, W.H.: Optimal state-space lumping in Markov chains. Inf. Process. Lett. 87(6), 309\u2013315 (2003)","journal-title":"Inf. Process. Lett."},{"key":"255_CR21","doi-asserted-by":"crossref","unstructured":"Doyen, L., Raskin, J.-F.: Improved algorithms for the automata-based approach to model-checking. In: Grumberg, O., Huth, M. (eds.) TACAS, volume 4424 of Lecture Notes in Computer Science, pp. 451\u2013465. Springer (2007)","DOI":"10.1007\/978-3-540-71209-1_34"},{"issue":"3","key":"255_CR22","first-page":"189","volume":"2","author":"RE Fikes","year":"1972","unstructured":"Fikes, R.E., Nilsson, N.J.: STRIPS:a new approach to the application of theorem proving to problem solving. Artif. Intell. 2(3), 189\u2013208 (1972)","journal-title":"Artif. Intell."},{"key":"255_CR23","volume-title":"Competitive Markov Decision Processes","author":"J Filar","year":"1997","unstructured":"Filar, J., Vrieze, K.: Competitive Markov Decision Processes. Springer, Berlin (1997)"},{"issue":"3","key":"255_CR24","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/s10703-011-0115-3","volume":"39","author":"E Filiot","year":"2011","unstructured":"Filiot, E., Jin, N., Raskin, J.-F.: Antichains and compositional algorithms for LTL synthesis. Form. Methods Syst. Des. 39(3), 261\u2013296 (2011)","journal-title":"Form. Methods Syst. Des."},{"issue":"3","key":"255_CR25","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1007\/BF02277857","volume":"7","author":"A Finkel","year":"1994","unstructured":"Finkel, A.: Decidability of the termination problem for completely specified protocols. Distrib. Comput. 7(3), 129\u2013135 (1994)","journal-title":"Distrib. Comput."},{"key":"255_CR26","doi-asserted-by":"crossref","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere!. Theor. Comput. Sci. 256(1\u20132), 63\u201392 (2001)","DOI":"10.1016\/S0304-3975(00)00102-X"},{"issue":"2\/3","key":"255_CR27","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. 10(2\/3), 149\u2013169 (1997)","journal-title":"Form. Methods Syst. Des."},{"issue":"5","key":"255_CR28","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Form. Asp. Comput. 6(5), 512\u2013535 (1994)","journal-title":"Form. Asp. Comput."},{"key":"255_CR29","unstructured":"Hartmanns, A.: Modest: a unified language for quantitative models. In: FDL, IEEE, pp. 44\u201351 (2012)"},{"issue":"2","key":"255_CR30","doi-asserted-by":"crossref","first-page":"326","DOI":"10.1112\/plms\/s3-2.1.326","volume":"3","author":"G Higman","year":"1952","unstructured":"Higman, G.: Ordering by divisibility in abstract algebras. Proc. Lond. Math. Soc. 3(2), 326\u2013336 (1952)","journal-title":"Proc. Lond. Math. Soc."},{"key":"255_CR31","volume-title":"Dynamic Programming and Markov Processes","author":"RA Howard","year":"1960","unstructured":"Howard, R.A.: Dynamic Programming and Markov Processes. Wiley, New Jersey (1960)"},{"key":"255_CR32","doi-asserted-by":"crossref","unstructured":"Jansen, D.N., Katoen, J.-P., Oldenkamp, M., Stoelinga, M., Zapreev, I.S.: How fast and fat is your probabilistic model checker? an experimental performance comparison. In: Yorav, K. (ed.) Haifa Verification Conference, volume 4899 of Lecture Notes in Computer Science, pp. 69\u201385. Springer (2007)","DOI":"10.1007\/978-3-540-77966-7_9"},{"issue":"2","key":"255_CR33","doi-asserted-by":"crossref","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","volume":"68","author":"J-P Katoen","year":"2011","unstructured":"Katoen, J.-P., Zapreev, I.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68(2), 90\u2013104 (2011)","journal-title":"Perform. Eval."},{"key":"255_CR34","volume-title":"Finite Markov Chains","author":"JG Kemeny","year":"1960","unstructured":"Kemeny, J.G., Snell, J.L.: Finite Markov Chains. Van Nostrand Company, Inc, New York (1960)"},{"key":"255_CR35","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV, volume 6806 of Lecture Notes in Computer Science, pp. 585\u2013591. Springer (2011)","DOI":"10.1007\/978-3-642-22110-1_47"},{"issue":"1","key":"255_CR36","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"KG Larsen","year":"1991","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1\u201328 (1991)","journal-title":"Inf. Comput."},{"key":"255_CR37","first-page":"86","volume-title":"AIPS","author":"SM Majercik","year":"1998","unstructured":"Majercik, S.M., Littman, M.L.: Maxplan: a new approach to probabilistic planning. In: Simmons, R.G., Veloso, M.M., Smith, S.F. (eds.) AIPS, pp. 86\u201393. AAAI, Palo Alto (1998)"},{"key":"255_CR38","unstructured":"Pachl, J.K.: Protocol description and analysis based on a state transition model with channel expressions. In: Rudin, H., West, C.H. (eds.) PSTV, Proceedings of the IFIP WG6.1, pp. 207\u2013219. North-Holland (1987)"},{"issue":"6","key":"255_CR39","doi-asserted-by":"crossref","first-page":"973","DOI":"10.1137\/0216062","volume":"16","author":"R Paige","year":"1987","unstructured":"Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973\u2013989 (1987)","journal-title":"SIAM J. Comput."},{"key":"255_CR40","doi-asserted-by":"crossref","unstructured":"Parker, D.: Personal communication, 2013-11-20","DOI":"10.7748\/nm2013.10.20.6.11.s15"},{"key":"255_CR41","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, New Jersey (1994)"},{"key":"255_CR42","volume-title":"Artificial Intelligence: A Modern Approach","author":"SJ Russell","year":"1995","unstructured":"Russell, S.J., Norvig, P.: Artificial Intelligence: A Modern Approach. Prentice Hall, Englewood Cliffs (1995)"},{"key":"255_CR43","doi-asserted-by":"crossref","unstructured":"Veinott, A.F.: On finding optimal policies in discrete dynamic programming with no discounting. Ann. Math. Stat. 37(5), 1284\u20131294 (1966)","DOI":"10.1214\/aoms\/1177699272"},{"key":"255_CR44","unstructured":"Von Essen, C.: Personal communication, 2013-11-20"},{"key":"255_CR45","doi-asserted-by":"crossref","unstructured":"Von Essen, C., Jobstmann, B.: Synthesizing efficient controllers. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI, volume 7148 of Lecture Notes in Computer Science, pp. 428\u2013444. Springer (2012)","DOI":"10.1007\/978-3-642-27940-9_28"},{"key":"255_CR46","doi-asserted-by":"crossref","unstructured":"Wimmer, R., Braitling, B., Becker, B., Hahn, E.M., Crouzen, P., Hermanns, H., Dhama, A., Theel, O.E.: Symblicit calculation of long-run averages for concurrent probabilistic systems. In: QEST, IEEE Computer Society, pp. 27\u201336 (2010)","DOI":"10.1109\/QEST.2010.12"},{"key":"255_CR47","doi-asserted-by":"crossref","unstructured":"Wulf, M.D., Doyen, L., Henzinger, T.A., Raskin, J.-F.: Antichains: a new algorithm for checking universality of finite automata. In: Ball, T., Jones, R.B. (eds.) CAV, volume 4144 of Lecture Notes in Computer Science, pp. 17\u201330. Springer (2006)","DOI":"10.1007\/11817963_5"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-016-0255-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0255-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0255-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-016-0255-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,4]],"date-time":"2019-09-04T00:54:59Z","timestamp":1567558499000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-016-0255-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,2,1]]},"references-count":47,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2017,9]]}},"alternative-id":["255"],"URL":"https:\/\/doi.org\/10.1007\/s00236-016-0255-4","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,2,1]]}}}