MaxSAT-based temporal logic inference from noisy data

Jean Raphaël Gaglione, Daniel Neider, Rajarshi Roy, Ufuk Topcu, Zhe Xu

Research output: Contribution to journalArticlepeer-review

3 Scopus citations


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 (LTLf) 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 LTLf 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.

Original languageEnglish (US)
Pages (from-to)427-442
Number of pages16
JournalInnovations in Systems and Software Engineering
Issue number3
StatePublished - Sep 2022


  • Decision tree
  • Explainable AI
  • Linear Temporal Logic
  • Signal Temporal Logic
  • Specification mining

ASJC Scopus subject areas

  • Software


Dive into the research topics of 'MaxSAT-based temporal logic inference from noisy data'. Together they form a unique fingerprint.

Cite this