Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic - Archive ouverte HAL Access content directly
Conference Papers Year : 2022

Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic

, , (1) ,
1
Ritam Raha
Rajarshi Roy
Daniel Neider

Abstract

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 formulas in fragments of LTL without the $$\mathbf {U}$$ U -operator 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.

Dates and versions

hal-03775030 , version 1 (12-09-2022)

Identifiers

Cite

Ritam Raha, Rajarshi Roy, Nathanaël Fijalkow, Daniel Neider. Scalable Anytime Algorithms for Learning Fragments of Linear Temporal Logic. Tools and Algorithms for the Construction and Analysis of Systems, Apr 2022, Munich, Germany. pp.263-280, ⟨10.1007/978-3-030-99524-9_14⟩. ⟨hal-03775030⟩

Collections

CNRS
11 View
0 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More