We address the problem of inferring descriptions of system behavior using Linear Temporal Logic (LTL) from a finite set of positive and negative examples. Most of the existing approaches for solving such a task rely on predefined templates for guiding the structure of the inferred formula. The approaches that can infer arbitrary LTL formulas, on the other hand, are not robust to noise in the data. To alleviate such limitations, we devise two algorithms for inferring concise LTL formulas even in the presence of noise. Our first algorithm infers minimal LTL formulas by reducing the inference problem to a problem in maximum satisfiability and then using off-the-shelf MaxSAT solvers to find a solution. To the best of our knowledge, we are the first to incorporate the usage of MaxSAT solvers for inferring formulas in LTL. Our second learning algorithm relies on the first algorithm to derive a decision tree over LTL formulas based on a decision tree learning algorithm. We have implemented both our algorithms and verified that our algorithms are efficient in extracting concise LTL descriptions even in the presence of noise.
翻译:我们从一组有限的积极和消极例子中推断出使用线性时空逻辑(LTL)系统行为描述的问题。解决这一任务的现有方法大多依靠预先定义的模板来指导推断公式的结构。另一方面,可以推断任意的LTL公式的方法对数据中的噪音并不有力。为了减轻这种限制,我们设计了两种算法来推断简明的LTL公式。我们的第一种算法通过将推论问题降低到最高可控性的问题,然后使用现成的MaxSAT解答器来寻找解决办法。我们最了解的是,我们首先采用MaxSAT解析法来推断LT的公式。我们的第二个学习算法依靠第一个算法,在决定树学习算法的基础上获得关于LTL公式的决策树。我们实施了我们的算法,并核实了我们的算法在提取简明的LTLT说明方面是有效的,即使存在噪音。