{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,30]],"date-time":"2026-03-30T02:27:08Z","timestamp":1774837628883,"version":"3.50.1"},"reference-count":58,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2015,3,2]],"date-time":"2015-03-02T00:00:00Z","timestamp":1425254400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"ERC Start","award":["279307: Graph Games"],"award-info":[{"award-number":["279307: Graph Games"]}]},{"name":"Austrian Science Fund (FWF) project S11402-N23 (RiSE), FWF","award":["P23499-N23"],"award-info":[{"award-number":["P23499-N23"]}]},{"name":"FWF NFN","award":["S11407-N23 (RiSE)"],"award-info":[{"award-number":["S11407-N23 (RiSE)"]}]},{"name":"European Research Council (ERC)","award":["267989 (QUAREM)"],"award-info":[{"award-number":["267989 (QUAREM)"]}]},{"name":"Microsoft faculty fellows award"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2015,3,2]]},"abstract":"<jats:p>The traditional synthesis question given a specification asks for the automatic construction of a system that satisfies the specification, whereas often there exists a preference order among the different systems that satisfy the given specification. Under a probabilistic assumption about the possible inputs, such a preference order is naturally expressed by a weighted automaton, which assigns to each word a value, such that a system is preferred if it generates a higher expected value. We solve the following optimal synthesis problem: given an omega-regular specification, a Markov chain that describes the distribution of inputs, and a weighted automaton that measures how well a system satisfies the given specification under the input assumption, synthesize a system that optimizes the measured value.<\/jats:p>\n          <jats:p>For safety specifications and quantitative measures that are defined by mean-payoff automata, the optimal synthesis problem reduces to finding a strategy in a Markov decision process (MDP) that is optimal for a long-run average reward objective, which can be achieved in polynomial time. For general omega-regular specifications along with mean-payoff automata, the solution rests on a new, polynomial-time algorithm for computing optimal strategies in MDPs with mean-payoff parity objectives. Our algorithm constructs optimal strategies that consist of two memoryless strategies and a counter. The counter is in general not bounded. To obtain a finite-state system, we show how to construct an \u03f5-optimal strategy with a bounded counter, for all \u03f5 &gt; 0. Furthermore, we show how to decide in polynomial time if it is possible to construct an optimal finite-state system (i.e., a system without a counter) for a given specification.<\/jats:p>\n          <jats:p>We have implemented our approach and the underlying algorithms in a tool that takes qualitative and quantitative specifications and automatically constructs a system that satisfies the qualitative specification and optimizes the quantitative specification, if such a system exists. We present some experimental results showing optimal systems that were automatically generated in this way.<\/jats:p>","DOI":"10.1145\/2699430","type":"journal-article","created":{"date-parts":[[2015,3,3]],"date-time":"2015-03-03T14:08:19Z","timestamp":1425391699000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":13,"title":["Measuring and Synthesizing Systems in Probabilistic Environments"],"prefix":"10.1145","volume":"62","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[{"name":"Institute of Science and Technology Austria (IST Austria), Klosterneuburg, Austria"}]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[{"name":"Institute of Science and Technology Austria (IST Austria), Klosterneuburg, Austria"}]},{"given":"Barbara","family":"Jobstmann","sequence":"additional","affiliation":[{"name":"\u00c9cole Polytechnique F\u00e9d\u00e9ral de Lausanne (EPFL), Gieres, France"}]},{"given":"Rohit","family":"Singh","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology (MIT), Cambridge, MA"}]}],"member":"320","published-online":{"date-parts":[[2015,3,2]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00596-1_24"},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of IFIP TCS. Kluwer, 493--506","author":"Baier C.","unstructured":"C. Baier , M. Gr\u00f6sser , M. Leucker , B. Bollig , and F. Ciesinski . 2004. Controller synthesis for probabilistic systems . In Proceedings of IFIP TCS. Kluwer, 493--506 . C. Baier, M. Gr\u00f6sser, M. Leucker, B. Bollig, and F. Ciesinski. 2004. Controller synthesis for probabilistic systems. In Proceedings of IFIP TCS. Kluwer, 493--506."},{"key":"e_1_2_1_3_1","volume-title":"Principles of Model Checking (Representation and Mind Series)","author":"Baier C.","unstructured":"C. Baier and J.-P. Katoen . 2008. Principles of Model Checking (Representation and Mind Series) . MIT Press . C. Baier and J.-P. Katoen. 2008. Principles of Model Checking (Representation and Mind Series). MIT Press."},{"key":"e_1_2_1_4_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of FSTTCS 95","author":"Bianco A.","unstructured":"A. Bianco and L. de Alfaro . 1995. Model checking of probabilistic and nondeterministic systems . In Proceedings of FSTTCS 95 . Lecture Notes in Computer Science , vol. 1026 , Springer , 499--513. A. Bianco and L. de Alfaro. 1995. Model checking of probabilistic and nondeterministic systems. In Proceedings of FSTTCS 95. Lecture Notes in Computer Science, vol. 1026, Springer, 499--513."},{"key":"e_1_2_1_5_1","volume-title":"1995. Probability and Measure","author":"Billingsley P.","unstructured":"P. Billingsley , Ed. 1995. Probability and Measure . Wiley-Interscience . P. Billingsley, Ed. 1995. Probability and Measure. Wiley-Interscience."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_14"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of FMCAD. IEEE, 85--92","author":"Bloem R.","unstructured":"R. Bloem , K. Greimel , T. Henzinger , and B. Jobstmann . 2009b. Synthesizing robust systems . In Proceedings of FMCAD. IEEE, 85--92 . R. Bloem, K. Greimel, T. Henzinger, and B. Jobstmann. 2009b. Synthesizing robust systems. In Proceedings of FMCAD. IEEE, 85--92."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11560548_7"},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of EMSOFT. Lecture Notes in Computer Science","volume":"2855","author":"Chakrabarti A.","unstructured":"A. Chakrabarti , L. de Alfaro , T. Henzinger , and M. Stoelinga . 2003. Resource interfaces . In Proceedings of EMSOFT. Lecture Notes in Computer Science , vol. 2855 . Springer, 117--133. A. Chakrabarti, L. de Alfaro, T. Henzinger, and M. Stoelinga. 2003. Resource interfaces. In Proceedings of EMSOFT. Lecture Notes in Computer Science, vol. 2855. Springer, 117--133."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2006.11"},{"key":"e_1_2_1_11_1","volume-title":"Proceedings of MFCS. 206--218","author":"Chatterjee K.","unstructured":"K. Chatterjee and L. Doyen . 2011a. Energy and mean-payoff parity Markov decision processes . In Proceedings of MFCS. 206--218 . K. Chatterjee and L. Doyen. 2011a. Energy and mean-payoff parity Markov decision processes. In Proceedings of MFCS. 206--218."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25929-6_3"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of FoSSaCS. 210--225","author":"Chatterjee K.","unstructured":"K. Chatterjee , L. Doyen , H. Gimbert , and Y. Oualhadj . 2014. Perfect-information stochastic mean-payoff parity games . In Proceedings of FoSSaCS. 210--225 . K. Chatterjee, L. Doyen, H. Gimbert, and Y. Oualhadj. 2014. Perfect-information stochastic mean-payoff parity games. In Proceedings of FoSSaCS. 210--225."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-6(3:10)2010"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1805950.1805953"},{"key":"e_1_2_1_16_1","volume-title":"Proceedings of SODA. ACM-SIAM, 1318--1336","author":"Chatterjee K.","unstructured":"K. Chatterjee and M. Henzinger . 2011. Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification . In Proceedings of SODA. ACM-SIAM, 1318--1336 . K. Chatterjee and M. Henzinger. 2011. Faster and dynamic algorithms for maximal end-component decomposition and related graph problems in probabilistic verification. In Proceedings of SODA. ACM-SIAM, 1318--1336."},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of SODA. ACM-SIAM, 1386--1399","author":"Chatterjee K.","unstructured":"K. Chatterjee and M. Henzinger . 2012. An O(n2) algorithm for alternating B\u00fcchi games . In Proceedings of SODA. ACM-SIAM, 1386--1399 . K. Chatterjee and M. Henzinger. 2012. An O(n2) algorithm for alternating B\u00fcchi games. In Proceedings of SODA. ACM-SIAM, 1386--1399."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2597631"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0180-2"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.26"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_34"},{"key":"e_1_2_1_22_1","series-title":"Lecture Notes in Computer Science","volume-title":"Quasy: Quantitative synthesis tool. In Proceedings of TACAS","author":"Chatterjee K.","year":"2011","unstructured":"K. Chatterjee , T. A. Henzinger , B. Jobstmann , and R. Singh . 2011 . Quasy: Quantitative synthesis tool. In Proceedings of TACAS . Lecture Notes in Computer Science , vol. 6605 , Springer , 267--271. K. Chatterjee, T. A. Henzinger, B. Jobstmann, and R. Singh. 2011. Quasy: Quantitative synthesis tool. In Proceedings of TACAS. Lecture Notes in Computer Science, vol. 6605, Springer, 267--271."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45220-1_11"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of SODA. ACM-SIAM, 121--130","author":"Chatterjee K.","unstructured":"K. Chatterjee , M. Jurdzi\u0144ski , and T. Henzinger . 2004. Quantitative stochastic parity games . In Proceedings of SODA. ACM-SIAM, 121--130 . K. Chatterjee, M. Jurdzi\u0144ski, and T. Henzinger. 2004. Quantitative stochastic parity games. In Proceedings of SODA. ACM-SIAM, 121--130."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39799-8_36"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_46"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the International Mathematical Congress.","author":"Church A.","year":"1962","unstructured":"A. Church . 1962 . Logic, arithmetic and automata . In Proceedings of the International Mathematical Congress. A. Church. 1962. Logic, arithmetic and automata. In Proceedings of the International Mathematical Congress."},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the Workshop on Logic of Programs. 52--71","author":"Clarke E. M.","unstructured":"E. M. Clarke and E. A. Emerson . 1981. Design and synthesis of synchronization skeletons using branching-time temporal logic . In Proceedings of the Workshop on Logic of Programs. 52--71 . E. M. Clarke and E. A. Emerson. 1981. Design and synthesis of synchronization skeletons using branching-time temporal logic. In Proceedings of the Workshop on Logic of Programs. 52--71."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/210332.210339"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_1_31_1","series-title":"Lecture Notes in Economics and Mathematical Systems","volume-title":"Minimax Algebra","author":"Cuninghame-Green R.","unstructured":"R. Cuninghame-Green . 1979. Minimax Algebra . In Lecture Notes in Economics and Mathematical Systems , vol. 166 . Springer-Verlag . R. Cuninghame-Green. 1979. Minimax Algebra. In Lecture Notes in Economics and Mathematical Systems, vol. 166. Springer-Verlag."},{"key":"e_1_2_1_33_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of STACS'97","author":"de Alfaro L.","unstructured":"L. de Alfaro . 1997b. Temporal logics for the specification of performance and reliability . In Proceedings of STACS'97 . Lecture Notes in Computer Science , vol. 1200 , Springer , 165--176. L. de Alfaro. 1997b. Temporal logics for the specification of performance and reliability. In Proceedings of STACS'97. Lecture Notes in Computer Science, vol. 1200, Springer, 165--176."},{"key":"e_1_2_1_34_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of CONCUR","author":"de Alfaro L.","unstructured":"L. de Alfaro . 1998. Stochastic transition systems . In Proceedings of CONCUR . Lecture Notes in Computer Science , vol. 1466 , Springer , 423--438. L. de Alfaro. 1998. Stochastic transition systems. In Proceedings of CONCUR. Lecture Notes in Computer Science, vol. 1466, Springer, 423--438."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/1759210.1759309"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.22"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/646734.701458"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.02.055"},{"key":"e_1_2_1_39_1","first-page":"305","article-title":"Multi-valued MSO logics over words and trees","volume":"84","author":"Droste M.","year":"2008","unstructured":"M. Droste , W. Kuich , and G. Rahonis . 2008 . Multi-valued MSO logics over words and trees . Fund. Inf. 84 , 305 -- 327 . M. Droste, W. Kuich, and G. Rahonis. 2008. Multi-valued MSO logics over words and trees. Fund. Inf. 84, 305--327.","journal-title":"Fund. Inf."},{"key":"e_1_2_1_40_1","doi-asserted-by":"crossref","unstructured":"M. Droste W. Kuich and H. Vogler. 2009. Handbook of Weighted Automata. Springer.   M. Droste W. Kuich and H. Vogler. 2009. Handbook of Weighted Automata. Springer.","DOI":"10.1007\/978-3-642-01492-5"},{"key":"e_1_2_1_41_1","doi-asserted-by":"crossref","unstructured":"J. Filar and K. Vrieze. 1996. Competitive Markov Decision Processes. Springer.   J. Filar and K. Vrieze. 1996. Competitive Markov Decision Processes. Springer.","DOI":"10.1007\/978-1-4612-4054-9"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90009-2"},{"key":"e_1_2_1_43_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of STACS","author":"Gaubert S.","unstructured":"S. Gaubert . 1997. Methods and applications of (max, +) linear algebra . In Proceedings of STACS . Lecture Notes in Computer Science , vol. 1200 , Springer , 261--282. S. Gaubert. 1997. Methods and applications of (max, +) linear algebra. In Proceedings of STACS. Lecture Notes in Computer Science, vol. 1200, Springer, 261--282."},{"key":"e_1_2_1_44_1","unstructured":"GLPK. GLPK (gnu linear programming kit). http:\/\/www.gnu.org\/software\/glpk\/.  GLPK. GLPK (gnu linear programming kit). http:\/\/www.gnu.org\/software\/glpk\/."},{"key":"e_1_2_1_45_1","volume-title":"Performance of Computer Communication Systems: A Model-Based Approach","author":"Haverkort B. R.","unstructured":"B. R. Haverkort . 1998. Performance of Computer Communication Systems: A Model-Based Approach . John Wiley & amp; Sons, Inc., New York, NY, USA. B. R. Haverkort. 1998. Performance of Computer Communication Systems: A Model-Based Approach. John Wiley &amp; Sons, Inc., New York, NY, USA."},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_36"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/646793.704696"},{"key":"e_1_2_1_48_1","volume-title":"Proceedings of VMCAI. Lecture Notes in Computer Science","volume":"4349","author":"Kupferman O.","unstructured":"O. Kupferman and Y. Lustig . 2007. Lattice automata . In Proceedings of VMCAI. Lecture Notes in Computer Science , vol. 4349 . Springer, 199--213. O. Kupferman and Y. Lustig. 2007. Lattice automata. In Proceedings of VMCAI. Lecture Notes in Computer Science, vol. 4349. Springer, 199--213."},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1530873.1530882"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_48"},{"key":"e_1_2_1_51_1","volume-title":"Proceedings of NIPS. MIT Press, 1043--1049","author":"Parr R.","unstructured":"R. Parr and S. Russell . 1997. Reinforcement learning with hierarchies of machines . In Proceedings of NIPS. MIT Press, 1043--1049 . R. Parr and S. Russell. 1997. Reinforcement learning with hierarchies of machines. In Proceedings of NIPS. MIT Press, 1043--1049."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"e_1_2_1_54_1","volume-title":"Markov Decision Processes","author":"Puterman M.","unstructured":"M. Puterman . 1994. Markov Decision Processes . John Wiley & amp; Sons, Inc. New York, NY. M. Puterman. 1994. Markov Decision Processes. John Wiley &amp; Sons, Inc. New York, NY."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.5555\/647325.721668"},{"key":"e_1_2_1_56_1","first-page":"81","article-title":"The control of discrete event systems","volume":"77","author":"Ramadge P. J. G.","year":"1989","unstructured":"P. J. G. Ramadge and W. M. Wonham . 1989 . The control of discrete event systems . IEEE Trans. Cont. Theory 77 , 81 -- 98 . P. J. G. Ramadge and W. M. Wonham. 1989. The control of discrete event systems. IEEE Trans. Cont. Theory 77, 81--98.","journal-title":"IEEE Trans. Cont. Theory"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1988.21948"},{"key":"e_1_2_1_58_1","volume-title":"Proceedings of LICS. IEEE, 322--331","author":"Vardi M.","unstructured":"M. Vardi and P. Wolper . 1986. An automata-theoretic approach to automatic program verification . In Proceedings of LICS. IEEE, 322--331 . M. Vardi and P. Wolper. 1986. An automata-theoretic approach to automatic program verification. In Proceedings of LICS. IEEE, 322--331."},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2010.12"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2699430","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2699430","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:16:58Z","timestamp":1750227418000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2699430"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,3,2]]},"references-count":58,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,3,2]]}},"alternative-id":["10.1145\/2699430"],"URL":"https:\/\/doi.org\/10.1145\/2699430","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,3,2]]},"assertion":[{"value":"2011-04-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-03-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}