Learning linear temporal logic (LTL) formulas from examples labeled as positive or negative has found applications in inferring descriptions of system behavior. We summarize two methods to learn LTL formulas from examples in two different problem settings. The first method assumes noise in the labeling of the examples. For that, they define the problem of inferring an LTL formula that must be consistent with most but not all of the examples. The second method considers the other problem of inferring meaningful LTL formulas in the case where only positive examples are given. Hence, the first method addresses the robustness to noise, and the second method addresses the balance between conciseness and specificity (i.e., language minimality) of the inferred formula. The summarized methods propose different algorithms to solve the aforementioned problems, as well as to infer other descriptions of temporal properties, such as signal temporal logic or deterministic finite automata.
翻译:从被标为正或负的示例中学习线性时间逻辑(LTL)公式发现,在推断系统行为描述时,应用了两种方法。我们从两个不同的问题设置中从示例中总结了两种方法来学习LTL公式。第一种方法在标注示例时假定噪音。为此,它们界定了计算一个必须符合大多数但并非所有实例的LTL公式的问题。第二种方法考虑了在只给出肯定示例的情况下推断有意义的LT公式的另一个问题。因此,第一种方法处理噪音的稳健性,第二种方法处理推断公式的简洁性和具体性(即语言最小性)之间的平衡。所总结的方法提出了解决上述问题的不同算法,并推断出其他时间属性的描述,例如信号时间逻辑或确定性限制的自动数据。