LeanLTL: A unifying framework for linear temporal logics in Lean
Eric Vin, Kyle A. Miller, and Daniel J. Fremont
TL;DR
LeanLTL is a flexible framework in Lean 4 that unifies various linear temporal logics, enabling reasoning about both finite and infinite traces with customizable properties and automation support.
Contribution
It introduces a unifying framework for linear temporal logics in Lean 4, supporting arbitrary expressions and embedding standard LTL flavors.
Findings
Supports reasoning about finite and infinite traces.
Allows combining LTL syntax with Lean expressions.
Provides automation for reasoning about LTL formulas.
Abstract
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, Reasoning, and Knowledge · Model-Driven Software Engineering Techniques