论文标题
概率系统上的LTLF合成
LTLf Synthesis on Probabilistic Systems
论文作者
论文摘要
许多系统自然地建模为马尔可夫决策过程（MDP），结合了概率和战略行动。给定系统模型作为MDP和系统行为的某些逻辑规范，综合的目的是找到一种策略，以最大程度地提高实现此行为的可能性。 定义行为的流行选择是线性时间逻辑（LTL）。对LTL中指定的属性的MDPS的策略综合已经进行了充分的研究。但是，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.
