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

Abstract

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)
JournalInnovations in Systems and Software Engineering
DOIs
StateAccepted/In press - 2022
Externally publishedYes

Keywords

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

ASJC Scopus subject areas

  • Software

Fingerprint

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

Cite this