Learning linear temporal properties from noisy data: a MaxSAT-based approach

DOI10.1007/978-3-030-88885-5_6zbMATH1497.68420OpenAlexW3208221999MaRDI QIDQ2147181FDOQ2147181

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

Publication date 22 June 2022

Full work available at URL https://arxiv.org/abs/2104.15083

zbMATH Keywords

linear temporal logicspecification miningexplainable AI

Mathematics Subject Classification ID

Learning and adaptive systems in artificial intelligence (68T05) Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20) Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Abstract: 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.

Recommendations

• TeLEx: learning signal temporal logic from positive examples using tightness metric
• Temporal logic inference for classification and prediction from data
• Data-driven statistical learning of temporal logic properties
• Learning to verify branching time properties
• A decision tree approach to data classification using signal temporal logic

Cites work

• A decision tree approach to data classification using signal temporal logic
• Interval temporal logic decision tree learning
• Temporal Logics for Learning and Detection of Anomalous Behavior
• Using temporal logics to express search control knowledge for planning

Cited in

(7)

• A decision tree approach to data classification using signal temporal logic
• TeLEx: learning signal temporal logic from positive examples using tightness metric
• Communicating safety of planned paths via optimally-simple explanations
• Temporal logic inference for classification and prediction from data
• Scalable anytime algorithms for learning fragments of linear temporal logic
• Data-driven statistical learning of temporal logic properties
• Survey on mining signal temporal logic specifications

Describes a project that uses

Uses Software

• z3

This page was built for publication: Learning linear temporal properties from noisy data: a MaxSAT-based approach

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2147181)