Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic

2021/10/13 by Ritam Raha, Raha, Ritam, Rajarshi Roy +5 · 3 citations
Computer Science · #AI-based Problem Solving and Planning #Artificial Intelligence (cs.AI) #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic, programming, and type systems #Machine Learning (cs.LG)

paper · doi:10.48550/arxiv.2110.06726

openalex publication_date 2021/10/13 · openalex created_date 2022/07/25 · openalex updated_date 2026/07/28

Abstract

Linear temporal logic (LTL) is a specification language for finite sequences (called traces) widely used in program verification, motion planning in robotics, process mining, and many other areas. We consider the problem of learning LTL formulas for classifying traces; despite a growing interest of the research community, existing solutions suffer from two limitations: they do not scale beyond small formulas, and they may exhaust computational resources without returning any result. We introduce a new algorithm addressing both issues: our algorithm is able to construct formulas an order of magnitude larger than previous methods, and it is anytime, meaning that it in most cases successfully outputs a formula, albeit possibly not of minimal size. We evaluate the performances of our algorithm using an open source implementation against publicly available benchmarks.

Cited by

• LTL_f Learning Meets Boolean Set Cover
• Automata Learning of Preferences over Temporal Logic Formulas from Pairwise Comparisons
• Learning Probabilistic Temporal Logic Specifications for Stochastic Systems

Related

• Learning Temporal Logic Properties: an Overview of Two Recent Methods
• Learning temporal formulas from examples is hard
• Learning Linear Temporal Properties
• The Complexity of Learning Linear Temporal Formulas from Examples
• Learning Finite Linear Temporal Logic Specifications with a Specialized Neural Operator