Learning Linear Temporal Properties from Noisy Data: A MaxSAT-Based Approach

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

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.

Original languageEnglish (US)
Title of host publicationAutomated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Proceedings
EditorsZhe Hou, Vijay Ganesh
PublisherSpringer Science and Business Media Deutschland GmbH
Pages74-90
Number of pages17
ISBN (Print)9783030888848
DOIs
StatePublished - 2021
Externally publishedYes
Event19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021 - Virtual, Online
Duration: Oct 18 2021Oct 22 2021

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12971 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference19th International Symposium on Automated Technology for Verification and Analysis, ATVA 2021
CityVirtual, Online
Period10/18/2110/22/21

Keywords

  • Explainable AI
  • Linear temporal logic
  • Specification mining

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Learning Linear Temporal Properties from Noisy Data: A MaxSAT-Based Approach'. Together they form a unique fingerprint.

Cite this