在随机博弈中学习最优策略用于时间任务
Learning Optimal Strategies for Temporal Tasks in Stochastic Games
AI总结：
本文提出一种无需环境模型的强化学习方法，通过确定性奇数自动机构建产品博弈，利用折扣奖励优化策略以满足LTL规范，解决大规模颜色问题并验证方法有效性。
摘要：
从线性时序逻辑（LTL）规范合成提供保证的控制器，用于在随机和潜在对抗性环境中运行的系统。然而，自动合成工具需要环境模型来构建控制器。本文引入一种无模型强化学习（RL）方法，从给定的LTL规范中推导控制器，即使环境完全未知。我们将问题建模为控制器与对抗性环境之间的随机博弈；然后学习最优控制策略，以最大化满足LTL规范的最坏情况概率。我们首先构建一个产品博弈，使用从给定LTL规范转换得到的确定性奇数自动机（DPA）。通过从DPA的接受条件中推导出不同的奖励和折扣因子，我们将最大化满足LTL规范的最坏情况概率转化为产品博弈中的折扣奖励目标；这使得可以使用无模型RL算法来学习最优控制器策略。为了处理当定义接受条件的DPA的集合数量（通常称为颜色）较大时的常见可扩展性问题，我们提出了一种惰性颜色生成方法，仅在需要时使用不同的奖励和折扣因子，并提出一种近似方法，其中控制器最终只关注一个颜色。在多个案例研究中，我们展示了我们的方法能扩展到广泛的LTL公式，并显著优于现有方法，在随机博弈中学习控制器。
英文摘要：
Synthesis from linear temporal logic (LTL) specifications provides assured controllers for systems operating in stochastic and potentially adversarial environments. Automatic synthesis tools, however, require a model of the environment to construct controllers. In this work, we introduce a model-free reinforcement learning (RL) approach to derive controllers from given LTL specifications even when the environment is completely unknown. We model the problem as a stochastic game (SG) between the controller and the adversarial environment; we then learn optimal control strategies that maximize the probability of satisfying the LTL specifications against the worst-case environment behavior. We first construct a product game using the deterministic parity automaton (DPA) translated from the given LTL specification. By deriving distinct rewards and discount factors from the acceptance condition of the DPA, we reduce the maximization of the worst-case probability of satisfying the LTL specification into the maximization of a discounted reward objective in the product game; this enables the use of model-free RL algorithms to learn an optimal controller strategy. To deal with the common scalability problems when the number of sets defining the acceptance condition of the DPA (usually referred as colors), is large, we propose a lazy color generation method where distinct rewards and discount factors are utilized only when needed, and an approximate method where the controller eventually focuses on only one color. In several case studies, we show that our approach is scalable to a wide range of LTL formulas, significantly outperforming existing methods for learning controllers from LTL specifications in SGs.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
