比率目标下具有最优平均情况行为的系统综合
Synthesizing Systems with Optimal Average-Case Behavior for Ratio Objectives
摘要：
我们展示了如何自动构建一个系统，满足给定的逻辑规范，并具有最佳的平均行为与比率成本的规范。当从一个逻辑规范合成一个系统时，经常会有几个不同的系统满足这个规范。在这种情况下，用户通常不容易正式声明她喜欢哪个系统。先前的工作提出通过在规范中添加定量方面来对正确的系统进行排名。期望的偏好关系可以用（i）定量语言来表达，定量语言是为系统的每个可能行为分配值的函数，以及（ii）定义系统的期望的优化标准的环境模型，例如，最坏情况或平均最优情况。在本文中，我们展示了如何合成一个系统，是最佳的（i）定量语言给出的自动机与比率成本函数，和（ii）环境模型给出的标记马尔可夫决策过程。该系统的目标是最小化预期（比率）成本。该解决方案是基于减少马尔可夫决策过程的比率成本函数，不需要在分母的成本是严格的积极的。我们找到一个最佳的策略，这些使用分数线性规划。
英文摘要：
We show how to automatically construct a system that satisfies a given logical specification and has an optimal average behavior with respect to a specification with ratio costs. When synthesizing a system from a logical specification, it is often the case that several different systems satisfy the specification. In this case, it is usually not easy for the user to state formally which system she prefers. Prior work proposed to rank the correct systems by adding a quantitative aspect to the specification. A desired preference relation can be expressed with (i) a quantitative language, which is a function assigning a value to every possible behavior of a system, and (ii) an environment model defining the desired optimization criteria of the system, e.g., worst-case or average-case optimal. In this paper, we show how to synthesize a system that is optimal for (i) a quantitative language given by an automaton with a ratio cost function, and (ii) an environment model given by a labeled Markov decision process. The objective of the system is to minimize the expected (ratio) costs. The solution is based on a reduction to Markov Decision Processes with ratio cost functions which do not require that the costs in the denominator are strictly positive. We find an optimal strategy for these using a fractional linear program.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
