feat(Logics/LTL): LTL formula type and semantics over omega-words

[benbrastmckie]

This PR adds Linear Temporal Logic (LTL) to CSLib.

The original PR included both LTL and Temporal (past+future). Per reviewer request, this PR contains LTL only. The Temporal formula type (with since/past operators) is deferred to a follow-up PR.

Files Changed

Cslib/Foundations/Logic/Connectives.lean (modified)

Adds the LTL-relevant typeclass hierarchy on top of PropositionalConnectives:

PropositionalConnectives
      (HasBot + HasImp)
               |
   FutureTemporalConnectives
       (+ HasUntil)
               |
        LTLConnectives
         (+ HasNext)

New classes: HasUntil, HasNext, FutureTemporalConnectives, LTLConnectives.

FutureTemporalConnectives is factored out because Temporal will branch from it to add HasSince, from which the past+future operators are definable. HasSince and TemporalConnectives are not included here (deferred to the Temporal PR).

Cslib/Logics/LTL/Syntax/Formula.lean (new file)

Defines the LTL formula inductive type with primitives {atom, bot, imp, next, untl}:

• Formula.someFuture (◇): ⊤ U φ — φ holds at some future point
• Formula.allFuture (□): ¬◇¬φ — φ holds at all future points
• Formula.leadsto (⇝): □(p → ◇q) — every p-state is eventually followed by a q-state

Notation uses standard LTL unicode symbols per reviewer request:

Operator	Notation	Unicode	VSCode name
next	◯	U+25EF	\bigcirc
until	𝓤	U+1D4E4	\MCU
eventually	◇	U+25C7	\Diamond
globally	□	U+25A1	\Box
leads-to	⇝	U+21DD	\leadsto

Note: □ is scoped to Cslib.Logic.LTL; within that scope it means "globally". The modal □ (box/necessity) is scoped to the modal logic namespace and does not conflict.

LTLConnectives instance registered so Formula can be used polymorphically in axiom schemas.

Cslib/Logics/LTL/Semantics/Satisfies.lean (new file)

Defines LTL satisfaction over omega-words:

def Satisfies (v : ℕ → (Atom → Prop)) (i : ℕ) : Formula Atom → Prop
  | .atom p => v i p
  | .bot => False
  | .imp φ ψ => Satisfies v i φ → Satisfies v i ψ
  | .next φ => Satisfies v (i + 1) φ
  | .untl φ ψ => ∃ j ≥ i, Satisfies v j ψ ∧ ∀ k, i ≤ k → k < j → Satisfies v k φ

φ U ψ holds at i when ψ eventually holds at some future j ≥ i (the event) and φ holds at all intermediate points (the guard).

Also defines Valid (holds at all time points) and Satisfiable (holds at some time point in some omega-word). Connection to OmegaExecution from the LTS library is deferred to future work.

references.bib (modified)

Adds LTL-relevant references:

• Kamp1968 — historical foundation (tense logic)
• Pnueli1977 — seminal LTL paper
• VardiWolper1986 — automata-theoretic approach

Removes GPSS1980 (fairness and past-time operators; belongs in the Temporal PR).

Cslib.lean (modified)

Adds Cslib.Logics.LTL.Syntax.Formula and Cslib.Logics.LTL.Semantics.Satisfies.

---

AI Disclosure

This PR was revised with assistance from Claude (Anthropic). Specifically:

• The notation changes (◯, 𝓤, ◇, □, ⇝) were implemented by Claude
• The leadsto abbreviation and notation were added by Claude
• The Satisfies.lean file was adapted from main branch content with Claude assistance
• All generated code was reviewed and verified to build cleanly

[ctchou]

General comments:

• We should start with a temporal logic with only future-time temporal operators. Past-time temporal operators are not very useful in deductive program verification and complicate the semantics.
• I would like to have a temporal logic that can talk about the (omega-)executions of LTS, not just a sequence of states.
• Also, we should be able to talk about LTS transitions.
• I don't understand what Encodable/Countable/Infinite/Denumerable instances are doing there. They seem to be completely irrelevant.

[benbrastmckie]

Thanks for the comments. The latest push addresses these points:

1. Future-only temporal operators. FutureTemporalConnectives (propositional + until) is now a shared base class. LTL.Formula instantiates LTLConnectives (future + next) with only future-time primitives. Temporal.Formula instantiates TemporalConnectives (future + past) for tense logic.

2. Omega-executions of LTS, not just state sequences. LTL.Satisfies is removed from this PR. Connection to LTS.OmegaExecution — which already carries both ss : ωSequence State and μs : ωSequence Label — is the right approach. A follow-up PR can define satisfaction directly over OmegaExecution pairs rather than bare state sequences.

3. Büchi automata and ω-regular languages. A natural follow-up is to prove the LTL-to-Büchi translation theorem, connecting LTL.Satisfies to ωLanguage.IsRegular via the existing boolean closure results.

4. Encodable/Countable/Infinite/Denumerable. Removed. Deferred to a completeness PR where they are actually needed.

[ctchou]

Since this PR depends on #648, can you rebase it on top of #648? Currently it is a single commit on top of main, which makes it hard to figure out what changes it makes relative to #648.

Also, many of the changed files don't seem to have anything to do with this PR, such as Data/HasFresh, LTS/Notation, CCS/Semantics, all the LambdaCalculus files, all the Logics/Modal files, etc. Can you remove those changes from this PR?

[ctchou]

What exactly is the difference between LTS/Syntax/Formula.lean and Temporal/Syntax/Formula.lean?

[benbrastmckie]

What exactly is the difference between LTS/Syntax/Formula.lean and Temporal/Syntax/Formula.lean?

Temporal/ is bidirectional and does not presume discreteness, admitting a base logic for all linear orders where that logic has discrete, dense, and continuous extensions. I have the completeness proofs for the base and dense extension, and have nearly completed the others (though the proof for the discrete extension has been very tricky). The semantics for snce and untl are strict (excluding the present) since this provides greater expressive power, making the corresponding weak operators definable. The other tense operators F, P, G, and H are all definable as well, where next and prev are definable in the discrete extension (these definitions return bot in dense orders). The Temporal/ logics are sound and complete over the different classes of linear orders, providing a basis from which to introduce a wide range of expressive resources for temporal reasoning.

LTL/ includes untl and next, assuming a weak (reflexive) semantics for untl. This makes the language less expressive but elegant in its simplicity, with a natural range of applications for discrete systems. LTL/ currently imports Temporal/ at the syntax level in order to define a toTemporal embedding that maps weak untl to reflexiveUntl (a derived operator) and next to phi U bot (which forces the witness to the immediate successor). Both mappings are semantically faithful on omega-sequences. It would make sense to separate this embedding into LTL/Embedding.lean so that LTL/ is self-contained and does not transitively depend on Temporal/. By establishing completeness for both systems, I aim to show that the discrete extension of Temporal/ is a conservative extension of LTL/.

[ctchou]

Can we separate LTL and Temporal into two different PRs? The former is far more important than the latter in computer science applications.

Regarding LTL, I'd like to see the following notational changes (where "..." is a unicode name in VScode's Lean mode):
"F" -> "\Diamond`
"G" -> "\Box"
"X" -> "\bigcirc"
"U" -> "\MCU"
These symbols are pretty standard. For example, see the first table of:
https://en.wikipedia.org/wiki/Linear_temporal_logic#Semantics

Another useful notation is "p \leadsto q", which is an abbreviation of "G (p -> F q)".