概率环境中的系统测量与综合
Measuring and Synthesizing Systems in Probabilistic Environments
摘要：
通常人们在满足给定规范的不同系统中有一个优先顺序。在关于可能输入的概率假设下，这样的偏好顺序自然地由加权自动机表示，该加权自动机为每个词分配一个值，使得如果系统生成更高的期望值，则系统是优选的。我们解决了以下最优合成问题：给定一个ω-正则规范，一个描述输入分布的马尔可夫链，以及一个衡量系统在给定输入假设下满足给定规范的加权自动机，合成一个优化测量值的系统。对于由平均支付自动机给出的安全规范和措施，最优合成问题相当于在马尔可夫决策过程（MDP）中找到一个策略，该策略对于长期平均奖励目标是最优的，这可以在多项式时间内完成。对于一般的ω-正规规范，解决方案依赖于一个新的，多项式时间的算法计算最优策略的MDP平均回报奇偶性目标。我们的算法生成的最优策略包括两个无记忆策略和一个计数器。该计数器通常没有边界。为了得到一个有限状态系统，我们展示了如何构造一个ε-最优策略，对于任何ε>0，都有一个有界计数器。我们还展示了如何在多项式时间内决定我们是否可以构造一个最优的有限状态系统（即，没有计数器的系统）。我们已经实现了我们的方法，在一个工具，采取定性和定量的规格，并自动构建一个系统，满足定性规格和优化的定量规格，如果这样的系统存在。我们呈现的实验结果显示了以这种方式生成的最佳系统。
英文摘要：
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 under the given input assumption, synthesize a system that optimizes the measured value. For safety specifications and measures given 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. Our algorithm generates optimal strategies consisting of two memoryless strategies and a counter. This counter is in general not bounded. To obtain a finite-state system, we show how to construct an ε-optimal strategy with a bounded counter for any ε>0. We also show how to decide in polynomial time if we can construct an optimal finite-state system (i.e., a system without a counter) for a given specification. We have implemented our approach 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 experimental results showing optimal systems that were generated in this way.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
