MaxSAT-based temporal logic inference from noisy data

We address the problem of inferring descriptions of system behavior using temporal logic from a finite set of positive and negative examples. In this paper, we consider two formalisms of temporal logic that describe linear time properties: Linear Temporal Logic over finite horizon (LTL_f) and Signal Temporal Logic (STL). For inferring formulas in either of the formalism, most of the existing approaches rely on predefined templates that guide the structure of the inferred formula. On the other hand, the approaches that can infer arbitrary formulas are not robust to noise in the data. To alleviate such limitations, we devise two algorithms for inferring concise formulas even in the presence of noise. Our first approach to infer minimal formulas involves reducing the inference problem to a problem in maximum satisfiability and then using off-the-shelf solvers to find a solution. To the best of our knowledge, we are the first to incorporate the usage of MaxSAT/MaxSMT solvers for inferring formulas in LTL_f and STL. Our second approach relies on the first approach to derive a decision tree over temporal formulas exploiting standard decision tree learning algorithm. We have implemented our approaches and verified their efficacy in learning concise descriptions in the presence of noise.