LeanLTL: A unifying framework for linear temporal logics in Lean
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866908430476771328 |
|---|---|
| author | Vin, Eric Miller, Kyle A. Fremont, Daniel J. |
| author_facet | Vin, Eric Miller, Kyle A. Fremont, Daniel J. |
| contents | We propose LeanLTL, a unifying framework for linear temporal logics in Lean 4. LeanLTL supports reasoning about traces that represent either infinite or finite linear time. The library allows traditional LTL syntax to be combined with arbitrary Lean expressions, making it straightforward to define properties involving numerical or other types. We prove that standard flavors of LTL can be embedded in our framework. The library also provides automation for reasoning about LeanLTL formulas in a way that facilitates using Lean's existing tactics. Finally, we provide examples illustrating the utility of the library in reasoning about systems that come from applications. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_01780 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | LeanLTL: A unifying framework for linear temporal logics in Lean Vin, Eric Miller, Kyle A. Fremont, Daniel J. Logic in Computer Science Programming Languages F.3.1; F.4.1; F.3.3 We propose LeanLTL, a unifying framework for linear temporal logics in Lean 4. LeanLTL supports reasoning about traces that represent either infinite or finite linear time. The library allows traditional LTL syntax to be combined with arbitrary Lean expressions, making it straightforward to define properties involving numerical or other types. We prove that standard flavors of LTL can be embedded in our framework. The library also provides automation for reasoning about LeanLTL formulas in a way that facilitates using Lean's existing tactics. Finally, we provide examples illustrating the utility of the library in reasoning about systems that come from applications. |
| title | LeanLTL: A unifying framework for linear temporal logics in Lean |
| topic | Logic in Computer Science Programming Languages F.3.1; F.4.1; F.3.3 |
| url | https://arxiv.org/abs/2507.01780 |