LTLf Synthesis under Partial Observability: From Theory to Practice
LTLf Synthesis under Partial Observability: From Theory to Practice
复制标题
DOI：
10.4204/eptcs.326.1
复制
发表时间：
2020-09
期刊：
影响因子：
--
通讯作者：
L. M. Tabajara;Moshe Y. Vardi
中科院分区：
文献类型：
--
作者：
L. M. Tabajara;Moshe Y. Vardi
LTL综合是从线性时序逻辑的形式规格说明中综合反应系统的问题。允许部分可观测性的扩展，其中系统不能直接访问关于环境的所有相关信息，允许将这个问题推广到更广泛的现实世界应用，但在实践中实现这种扩展的困难意味着它仍然停留在理论领域。最近，它已被证明，限制LTL合成有限的执行系统，通过使用LTL有限时域语义（LTLf）允许在实践中显着简单的实现。由于LTLf概念上的简单性，它第一次有可能在实践中探索部分可观测性等扩展。以前的工作从理论上分析了部分可观测下的LTLf综合问题，并提出了两种可能的算法，一种是3EXPTIME，另一种是2EXPTIME复杂度。在这项工作中，我们首先证明了一个复杂性下界在早期的工作中所提出的。然后，我们补充的理论分析，展示了如何在实践中将这两种算法集成到一个既定的框架LTLf合成。我们还确定了第三个，基于MSO的，这个框架启用的方法。我们的实验评估揭示了与理论似乎建议的结果非常不同的结果，3EXPTIME算法通常优于2EXPTIME方法。此外，只要能够克服初始内存瓶颈，基于MSO的方法通常可以优于其他方法。
LTL synthesis is the problem of synthesizing a reactive system from a formal specification in Linear Temporal Logic. The extension of allowing for partial observability, where the system does not have direct access to all relevant information about the environment, allows generalizing this problem to a wider set of real-world applications, but the difficulty of implementing such an extension in practice means that it has remained in the realm of theory. Recently, it has been demonstrated that restricting LTL synthesis to systems with finite executions by using LTL with finite-horizon semantics (LTLf) allows for significantly simpler implementations in practice. With the conceptual simplicity of LTLf, it becomes possible to explore extensions such as partial observability in practice for the first time. Previous work has analyzed the problem of LTLf synthesis under partial observability theoretically and suggested two possible algorithms, one with 3EXPTIME and another with 2EXPTIME complexity. In this work, we first prove a complexity lower bound conjectured in earlier work. Then, we complement the theoretical analysis by showing how the two algorithms can be integrated in practice into an established framework for LTLf synthesis. We furthermore identify a third, MSO-based, approach enabled by this framework. Our experimental evaluation reveals very different results from what the theory seems to suggest, with the 3EXPTIME algorithm often outperforming the 2EXPTIME approach. Furthermore, as long as it is able to overcome an initial memory bottleneck, the MSO-based approach can often outperforms the others.