LeanLTL: A Unifying Framework for Linear Temporal Logics in Lean

Linear temporal logic (LTL) [25, 24] has long been used in the verification community to specify the behaviors of systems over time. LTL has achieved such longevity by striking a balance between expressivity – for example being able to express convenient properties such as “CarAtDestination will eventually be true forever” and “GateOpen is always eventually true” – and simplicity, being a decidable logic [24] with practical tools for satisfiability checking, model checking, and synthesis (e.g. [16, 12, 13, 18]). LTL has been repeatedly used to great effect in real-world applications such as communication protocols [5], hardware synthesis [3], security [21], and planning [8].

Applications of LTL often require variations on or extensions to the core logic. For example, in runtime monitoring [2] one needs to describe system behaviors over time periods of finite extent, rather than the infinite traces used in LTL. The logic LTLf [6] accommodates this need; like LTL, it is decidable [6] and efficiently solvable with existing tools [12].

Basic LTL only supports propositional (boolean) variables, but, more generally, system specifications often involve predicates over integers, real numbers, arrays, and other data types. For example, in LTL the property “Eventually, ” would be encoded as $\mathrm{F}p$ with $p$ an atomic proposition defined outside of LTL itself to be true at exactly those timesteps where . The LTL encoding does not represent the relationship between the proposition $p$ and the underlying attribute of the system DistanceToCar, meaning that some valid deductions cannot be carried out within LTL. For example, if we know that DistanceToCar is either zero or decreases by at least 1 in each timestep of an infinite trace, then the property above would hold; but LTL cannot encode the conditions on DistanceToCar more precisely than as independent, opaque propositions. LTL Modulo Theories (LTLMT) [27] and LTLf Modulo Theories (LTLfMT) [10] address this shortcoming by replacing propositions with atoms from a given theory in the vein of Satisfiability Modulo Theories (SMT) [1]. Commonly-used theories include linear integer arithmetic (LIA, a.k.a. Presburger arithmetic), bitvectors (BV), and nonlinear real arithmetic (NRA). When the underlying theory is decidable, there is a semi-decision procedure for LTLMT [10], with certain theories supporting a full decision procedure [11]. Returning to our previous example, we could represent and solve the implication “(DistanceToCar is $0$ or decreases by at least $1$) implies (Eventually, )” by encoding it as an LTLMT problem that utilizes the decidable theory of Linear Real Arithmetic [1].

Prior work on increasing the expressivity of linear temporal logics has largely attempted to stay within the realm of (semi-)decidability, to ensure that tools for the new logics can be fully automatic. However, such approaches rule out the use of many useful undecidable theories, such as nonlinear real arithmetic with exponents or trigonometric functions (often needed for modeling cyber-physical systems). Another limitation is that decision procedures for LTLMT are not available for all decidable theories [11]. Finally, even in decidable cases, the complexity of the decision procedure can render realistic problems intractable in practice. The above problems arise primarily in the context of automated tools, but with interactive theorem provers one may permit undecidable theories, as users may provide proofs for what is not in the purview of decision procedures.

With this goal in mind, we propose LeanLTL¹¹1Available at: https://github.com/UCSCFormalMethods/LeanLTL. The exact version presented in this paper is tagged vITP25., a unified framework for reasoning about linear temporal properties of systems in Lean 4 [19]. Its key features include:

• $\mathrm{■}$

  Core types for modeling temporal properties across both infinite and finite traces, with support for arbitrary Lean expressions inside these formulas. Proofs using these types can make use of the full power of existing Lean tactics, as illustrated in Figure 1.

• $\mathrm{■}$

  Convenient syntax for creating LeanLTL formulas with the appropriate semantics represented directly in Lean, with embedded Lean propositions.

• $\mathrm{■}$

  Basic automation and tools to simplify reasoning about LeanLTL formulas.

• $\mathrm{■}$

  Formalized proofs that LTL and LTLf can be embedded into LeanLTL.

In the rest of the paper, we describe these features and present real-world-inspired examples that illustrate the utility of LeanLTL. Our library, examples, and proofs are included in the project repository.

In this section we summarize the syntax and semantics of LTL and some of its extensions.

A full definition of the syntax and semantics of LTL can be found in [24]. LTL includes the standard propositional operators NOT ($\neg$), AND ($\wedge$), and OR ($\vee$), and the constant True ($\top$), in addition to several temporal operators:

• $\mathrm{■}$

  Next: $\mathrm{X}p$ (or $○p$) is true if and only if $p$ is true in the next timestep.

• $\mathrm{■}$

  Until: $p𝒰q$ is true iff $p$ is true at least until $q$ is true, and $q$ must eventually be true.

• $\mathrm{■}$

  Release: $pℛq$ is true iff $p$ is true up until and including the point where $q$ is true. If $q$ never becomes true, $p$ must be true forever.

• $\mathrm{■}$

  Finally: $\mathrm{F}p$ (or $\mathrm{◆}p$) is true iff $p$ is true in some future timestep, equivalent to $\top 𝒰p$.

• $\mathrm{■}$

  Globally: $\mathrm{G}p$ (or $\mathrm{\square }p$) is true iff $p$ is true in all future timesteps, equivalent to $\neg \mathrm{F}\neg p$.

LTLf, whose full syntax and semantics can be found in [6], modifies the semantics of $\mathrm{X}$ to account for the possibility that the next value does not exist due to being at the end of a finite trace. The two resulting operators are strong next, with ${\mathrm{X}}^{\mathrm{s}}p$ ($○p$ in [6]) evaluating to false at the end of a finite trace, and weak next, with ${\mathrm{X}}^{\mathrm{w}}p$ (originally $\begin{array}{c}\sim \hfill \\ ○\hfill \end{array}p$) evaluating to true at the end of a finite trace; it is equivalent to $({\mathrm{X}}^{\mathrm{s}}p)\vee \neg {\mathrm{X}}^{\mathrm{s}}\top$.

LTLfMT expands these semantics further by replacing propositions with atomic formulas from an underlying theory, allowing ${\mathrm{X}}^{\mathrm{s}}$ and ${\mathrm{X}}^{\mathrm{w}}$ to be applied to terms inside those formulas. A full definition of its syntax and semantics can be found in [10].

In this section we describe the key components of LeanLTL: types for traces and formulas, a macro enabling the use of traditional LTL syntax, and automation for proofs involving LTL.

In this section, we illustrate the expressivity of LeanLTL and its ability to help prove useful properties about real-world systems. For the former, we provide Lean proofs that LTL and LTLf can be embedded into LeanLTL. The embedding proof first provides an inductive syntax for each logic and an evaluation function giving its semantics. We then define a function translating the logic to LeanLTL. Finally, we show that the evaluation function applied to the original syntax is equisatisfiable with our LeanLTL translation and the LeanLTL semantics. An abbreviated version of the LTL embedding proof can be found in Figure 2, and the complete Lean proofs are included in the project repository.

To illustrate the application of LeanLTL to non-trivial real-world scenarios, we provide an abbreviated example applying the library to a system consisting of two traffic lights at an intersection, with which we demonstrate how LeanLTL can be used to model a system, its environment, and its specifications, and prove that a specification is satisfied for any given trace. The full example can be found in the supplemental materials.

To begin, we declare the state of the system at each timestep, shown in the first part of Figure 3. The state consists of whether each of the two lights is green, as well as the numbers of cars arriving, leaving, or waiting at each light.

Next we define properties that we assume about the system. In our example these properties are assumed to be derived from external specifications, but they could also include a Lean function representing a part of the system used directly in a LeanLTL formula. The second part of Figure 3 shows a selection of these properties: for example, TL1ToTL2Green states that when light 1 is green and has no cars waiting, in the next timestep it turns red and light 2 turns green. Note the use of arithmetic here and in TL1QueueNext.

In the last part of the figure, we state the properties that we wish to prove our system satisfies: G_OneLightGreen states that exactly one of the traffic lights is green at any given time, and G_F_Green states that each light will turn green infinitely often.

Finally, we prove that our desired properties hold for all traces satisfying the assumed properties. Complete proofs can be found in the project repository.

In this paper we presented our initial prototype of LeanLTL, a unifying framework for linear temporal logics in Lean. We described the core features of the library and illustrated how they can be used to encode and prove temporal properties of systems in Lean. In future work we plan to develop further automation, including integrations with decision procedures, as well as embedding proofs for LTLMT and LTLfMT. We also plan to consider adding support for other LTL variants, including past-time and bounded-time operators.