LTL$_f$ Learning Meets Boolean Set Cover
Fuente:
arXiv
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911370987962368 |
|---|---|
| author | Bathie, Gabriel Fijalkow, Nathanaël Matricon, Théo Mouillon, Baptiste Vandenhove, Pierre |
| author_facet | Bathie, Gabriel Fijalkow, Nathanaël Matricon, Théo Mouillon, Baptiste Vandenhove, Pierre |
| contents | Learning formulas in Linear Temporal Logic (LTLf) from finite traces is a fundamental research problem which has found applications in artificial intelligence, software engineering, programming languages, formal methods, control of cyber-physical systems, and robotics. We implement a new CPU tool called Bolt improving over the state of the art by learning formulas more than 100x faster over 70% of the benchmarks, with smaller or equal formulas in 98% of the cases. Our key insight is to leverage a problem called Boolean Set Cover as a subroutine to combine existing formulas using Boolean connectives. Thanks to the Boolean Set Cover component, our approach offers a novel trade-off between efficiency and formula size. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2509_24616 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | LTL$_f$ Learning Meets Boolean Set Cover Bathie, Gabriel Fijalkow, Nathanaël Matricon, Théo Mouillon, Baptiste Vandenhove, Pierre Artificial Intelligence Formal Languages and Automata Theory Logic in Computer Science Learning formulas in Linear Temporal Logic (LTLf) from finite traces is a fundamental research problem which has found applications in artificial intelligence, software engineering, programming languages, formal methods, control of cyber-physical systems, and robotics. We implement a new CPU tool called Bolt improving over the state of the art by learning formulas more than 100x faster over 70% of the benchmarks, with smaller or equal formulas in 98% of the cases. Our key insight is to leverage a problem called Boolean Set Cover as a subroutine to combine existing formulas using Boolean connectives. Thanks to the Boolean Set Cover component, our approach offers a novel trade-off between efficiency and formula size. |
| title | LTL$_f$ Learning Meets Boolean Set Cover |
| topic | Artificial Intelligence Formal Languages and Automata Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2509.24616 |