针对比率目标的具有最优平均行为的系统合成

我们展示了如何自动构造一个系统，该系统满足给定的逻辑规约，并且相对于具有比率成本的规约具有最优的平均行为。当从逻辑规约合成系统时，通常会有多个不同的系统满足该规约。在这种情况下，用户通常不容易形式化地声明她更偏好哪个系统。先前的工作提出通过向规约中添加定量方面来对正确的系统进行排序。期望的偏好关系可以用 表示，其中 是一种为系统的每个可能行为赋值的函数， 是定义系统期望优化标准（例如，最坏情况或平均情况最优）的环境模型。在本文中，我们展示了如何合成一个在以下两方面最优的系统： 具有比率成本函数的自动机给定的定量语言，以及 由标记马尔可夫决策过程给定的环境模型。系统的目标是最小化期望（比率）成本。该解决方案基于向带有比率成本函数的马尔可夫决策过程的归约，该过程不要求分母中的成本严格为正。我们使用分数线性规划为这些过程寻找最优策略。