Linear temporal logic (LTL) is a specification language for finite sequences (called traces) widely used in program verification, motion planning in robotics, process mining, and many other areas. We consider the problem of learning LTL formulas for classifying traces; despite a growing interest of the research community, existing solutions suffer from two limitations: they do not scale beyond small formulas, and they may exhaust computational resources without returning any result. We introduce a new algorithm addressing both issues: our algorithm is able to construct formulas an order of magnitude larger than previous methods, and it is anytime, meaning that it in most cases successfully outputs a formula, albeit possibly not of minimal size. We evaluate the performances of our algorithm using an open source implementation against publicly available benchmarks.
翻译:线性时间逻辑(LTL)是程序核查、机器人运动规划、工艺采矿和其他许多领域广泛使用的限定序列(所谓痕量)的具体说明语言。我们考虑了学习LTL公式对痕量进行分类的问题;尽管研究界越来越感兴趣,但现有解决方案存在两个局限性:它们的规模不超出小公式,它们可能耗尽计算资源而不产生任何结果。我们引入了一个新的算法,处理这两个问题:我们的算法能够构建比以往方法大得多的层次的公式,而且随时可以,这意味着它在大多数情况下成功地输出出一种公式,尽管可能不是最小的公式。我们用开放源执行来对照公开的基准来评估我们的算法的绩效。