Measuring and synthesizing systems in probabilistic environments LNCS Chatterjee, Krishnendu ; https://orcid.org/0000-0002-4561-241X Henzinger, Thomas A ; https://orcid.org/0000−0002−2985−7724 Jobstmann, Barbara Singh, Rohit Often one has a preference order among the different systems that satisfy a 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 tinder the given input assumption, synthesize a system that optimizes the measured value. For safety specifications and measures that are defined by mean-payoff automata, the optimal-synthesis problem amounts to finding a strategy in a Markov decision process (MDP) that is optimal for a long-run average reward objective, which can be done in polynomial time. For general omega-regular specifications, the solution rests on a new, polynomial-time algorithm for computing optimal strategies in MDPs with mean-payoff parity objectives. We present some experimental results showing optimal systems that were automatically generated in this way. Springer 2010 info:eu-repo/semantics/conferenceObject doc-type:ConferenceObject ConferenceObject http://purl.org/coar/resource_type/c_5794 https://research-explorer.ista.ac.at/record/3864 Chatterjee K, Henzinger TA, Jobstmann B, Singh R. Measuring and synthesizing systems in probabilistic environments. In: Vol 6174. Springer; 2010:380-395. doi:<a href="https://doi.org/10.1007/978-3-642-14295-6_34">10.1007/978-3-642-14295-6_34</a> eng info:eu-repo/semantics/altIdentifier/doi/10.1007/978-3-642-14295-6_34 info:eu-repo/semantics/altIdentifier/arxiv/1004.0739 info:eu-repo/semantics/openAccess