LTLf Synthesis on Probabilistic Systems
LTLf Synthesis on Probabilistic Systems
复制标题
DOI：
10.4204/eptcs.326.11
复制
发表时间：
2020-09
期刊：
影响因子：
--
通讯作者：
Andrew M. Wells;Morteza Lahijanian;L. Kavraki;Moshe Y. Vardi
中科院分区：
文献类型：
--
作者：
Andrew M. Wells;Morteza Lahijanian;L. Kavraki;Moshe Y. Vardi
许多系统自然地被建模为马尔可夫决策过程（MDP），结合了概率和战略行动。给定一个作为MDP的系统模型和一些系统行为的逻辑规范，综合的目标是找到一个最大化实现这种行为的概率的策略。定义行为的一个流行选择是线性时态逻辑（LTL）。关于LTL中规定的特性的MDP政策综合已得到充分研究。然而，LTL是在无限迹上定义的，而许多感兴趣的属性本质上是有限的。有限迹上的线性时序逻辑（LTLf）已被用来表达这样的属性，但没有工具存在，以解决策略合成MDP行为的有限迹属性。我们提出了两种算法来解决这个合成问题：第一个通过减少LTLf到LTL和第二个使用本地工具的LTLf。我们比较了这两种方法的可扩展性的合成，并表明，本机的方法提供了更好的可扩展性相比，现有的自动机生成工具的LTL。
Many systems are naturally modeled as Markov Decision Processes (MDPs), combining probabilities and strategic actions. Given a model of a system as an MDP and some logical specification of system behavior, the goal of synthesis is to find a policy that maximizes the probability of achieving this behavior. A popular choice for defining behaviors is Linear Temporal Logic (LTL). Policy synthesis on MDPs for properties specified in LTL has been well studied. LTL, however, is defined over infinite traces, while many properties of interest are inherently finite. Linear Temporal Logic over finite traces (LTLf) has been used to express such properties, but no tools exist to solve policy synthesis for MDP behaviors given finite-trace properties. We present two algorithms for solving this synthesis problem: the first via reduction of LTLf to LTL and the second using native tools for LTLf. We compare the scalability of these two approaches for synthesis and show that the native approach offers better scalability compared to existing automaton generation tools for LTL.