Learning Linear Temporal Properties from Noisy Data: A MaxSAT Approach
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Fuzzy Maximum Satisfiability
In this paper, we extend the Maximum Satisfiability (MaxSAT) problem to {\L}ukasiewicz logic. The MaxSAT problem for a set of formulae {\Phi} is the problem of finding an assignment to the variables in {\Phi} that satisf…
HyperSAT: Unsupervised Hypergraph Neural Networks for Weighted MaxSAT Problems
Graph neural networks (GNNs) have shown promising performance in solving both Boolean satisfiability (SAT) and Maximum Satisfiability (MaxSAT) problems due to their ability to efficiently model and capture the structural…
Can LLMs Build a MaxSAT Solver from Papers? The CoreForge Experience
We report on CoreForge, an experience in using large language models (LLMs) to build an unweighted MaxSAT solver from research papers rather than from an existing solver codebase. The project focuses on unsatisfiability-…
DPMS: An ADD-Based Symbolic Approach for Generalized MaxSAT Solving
Boolean MaxSAT, as well as generalized formulations such as Min-MaxSAT and Max-hybrid-SAT, are fundamental optimization problems in Boolean reasoning. Existing methods for MaxSAT have been successful in solving benchmark…
BandMaxSAT: A Local Search MaxSAT Solver with Multi-armed Bandit
We address Partial MaxSAT (PMS) and Weighted PMS (WPMS), two practical generalizations of the MaxSAT problem, and propose a local search algorithm for these problems, called BandMaxSAT, that applies a multi-armed bandit …