feat(Logics/LTL): LTL formula type and semantics over omega-words #649
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,107 @@ | ||
| /- | ||
| Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Benjamin Brast-McKie | ||
| -/ | ||
|
|
||
| module | ||
|
|
||
| import Cslib.Init | ||
|
|
||
| /-! # Connective Typeclasses for Propositional and Temporal Logic | ||
|
|
||
| This module defines a typeclass hierarchy for logical connectives. Each formula | ||
| type registers itself as an instance of the appropriate connective class, enabling polymorphic | ||
| axiom definitions and notation that work uniformly across different formula types. | ||
|
|
||
| ## Design | ||
|
|
||
| The hierarchy adopts a hybrid five-primitive propositional signature `{atom, bot, imp, and, or}`, | ||
| following the operator-typeclass direction of fmontesi's PR #607 (one class per operator): | ||
| - **Atomic classes**: `HasBot`, `HasImp`, `HasAnd`, `HasOr`, `HasUntil`, `HasNext` | ||
| - **Bundled classes**: `PropositionalConnectives` (extends `HasBot` and `HasImp`), | ||
| `FutureTemporalConnectives` (extends `PropositionalConnectives` and `HasUntil`), | ||
| `LTLConnectives` (extends `FutureTemporalConnectives` and `HasNext`) | ||
|
|
||
| Conjunction (`HasAnd`) and disjunction (`HasOr`) are treated as independent primitives rather | ||
| than Łukasiewicz-derived connectives. The classical encodings `φ ∧ ψ := ¬(φ → ¬ψ)` and | ||
| `φ ∨ ψ := ¬φ → ψ` are only propositionally equivalent to `∧` and `∨` in classical logic | ||
| ([Wajsberg1938], [McKinsey1939]); they fail in intuitionistic and minimal logic. Making `and` | ||
| and `or` primitive via `HasAnd`/`HasOr` supports all three logic strengths with a single | ||
| typeclass hierarchy. | ||
|
|
||
| Negation and verum stay derived: each concrete formula type defines `neg φ := φ → ⊥` and | ||
| `top := ⊥ → ⊥` as `abbrev`s, which are valid in minimal, intuitionistic, and classical logic | ||
| alike, so no typeclass machinery is needed for them. | ||
|
|
||
| ## References | ||
|
|
||
| * [J. Avigad, *Mathematical Logic and Computation*][Avigad2022] | ||
| * [I. Johansson, *Der Minimalkalkül, ein reduzierter intuitionistischer Formalismus*][Johansson1937] | ||
| * [M. Wajsberg, *Untersuchungen über den Aussagenkalkül von A. Heyting*][Wajsberg1938] | ||
| * [J. C. C. McKinsey, | ||
| *Proof of the Independence of the Primitive Symbols of Heyting's Calculus*][McKinsey1939] | ||
| * [D. Prawitz, *Natural Deduction: A Proof-Theoretical Study*][Prawitz1965] | ||
| * [A. S. Troelstra, D. van Dalen, | ||
| *Constructivism in Mathematics: An Introduction*][TroelstraVanDalen1988] | ||
| * [A. Church, *Introduction to Mathematical Logic*][Church1956] | ||
| * [G. Gentzen, *Untersuchungen über das logische Schließen*][Gentzen1935] | ||
| -/ | ||
|
|
||
| @[expose] public section | ||
|
|
||
| namespace Cslib.Logic | ||
|
|
||
| /-- A type has a falsum (bottom) connective. -/ | ||
| class HasBot (F : Type*) where | ||
| /-- The falsum/bottom connective. -/ | ||
| bot : F | ||
|
|
||
| /-- A type has an implication connective. -/ | ||
| class HasImp (F : Type*) where | ||
| /-- The implication connective. -/ | ||
| imp : F → F → F | ||
|
|
||
| /-- A type has an until temporal operator. -/ | ||
| class HasUntil (F : Type*) where | ||
| /-- The until temporal operator. -/ | ||
| untl : F → F → F | ||
|
|
||
| /-- A type has a next-step temporal operator. -/ | ||
| class HasNext (F : Type*) where | ||
| /-- The next-step temporal operator. -/ | ||
| next : F → F | ||
|
|
||
| /-- A type has a conjunction connective. -/ | ||
| class HasAnd (F : Type*) where | ||
| /-- The conjunction connective. -/ | ||
| and : F → F → F | ||
|
|
||
| /-- A type has a disjunction connective. -/ | ||
| class HasOr (F : Type*) where | ||
| /-- The disjunction connective. -/ | ||
| or : F → F → F | ||
|
|
||
| /-- Propositional connectives: falsum and implication. | ||
|
|
||
| `HasAnd` and `HasOr` are defined as standalone atomic classes in this module. | ||
| When all four connectives are needed, use | ||
| `[PropositionalConnectives F] [HasAnd F] [HasOr F]`. -/ | ||
| class PropositionalConnectives (F : Type*) extends HasBot F, HasImp F | ||
|
|
||
| /-- Future temporal connectives: propositional connectives plus until (no since, no next). | ||
|
|
||
| This bundle is shared by both `LTLConnectives` (which adds `HasNext`) and | ||
| `TemporalConnectives` (which adds `HasSince`). Factoring out the future fragment | ||
| allows code generic over future-only temporal logics without committing to past or | ||
| next-step operators. -/ | ||
| class FutureTemporalConnectives (F : Type*) extends PropositionalConnectives F, HasUntil F | ||
|
|
||
| /-- LTL connectives: future temporal connectives plus a primitive next-step operator. | ||
|
|
||
| Linear Temporal Logic uses `next` as a primitive rather than deriving it from `until` | ||
| (the encoding `next φ = φ U ⊥` does not hold in all models). `FutureTemporalConnectives` | ||
| provides `bot`, `imp`, and `untl`; this bundle adds `next`. -/ | ||
| class LTLConnectives (F : Type*) extends FutureTemporalConnectives F, HasNext F | ||
|
|
||
| end Cslib.Logic |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,64 @@ | ||
| /- | ||
| Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Benjamin Brast-McKie | ||
| -/ | ||
|
|
||
| module | ||
|
|
||
| public import Cslib.Logics.LTL.Syntax.Formula | ||
|
|
||
| /-! # LTL Satisfaction over Omega-Words | ||
|
|
||
| This module defines a basic satisfaction relation for LTL formulas over omega-words. | ||
| An omega-word is represented as a valuation `v : ℕ → (Atom → Prop)`, assigning to | ||
| each time point `i : ℕ` the set of atoms that hold at that point. | ||
|
|
||
| The semantics follow the standard Kripke/Pnueli definition of LTL over ω-sequences. | ||
| Connection to `OmegaExecution` from the LTS library is deferred to future work. | ||
|
|
||
| ## Main definitions | ||
|
|
||
| - `Satisfies v i φ` : formula `φ` holds at time `i` in valuation `v` | ||
| - `Valid v φ` : `φ` holds at all time points in `v` | ||
| - `Satisfiable φ` : `φ` holds at some time point in some valuation | ||
|
|
||
| ## References | ||
|
|
||
| * [A. Pnueli, *The Temporal Logic of Programs*][Pnueli1977] | ||
| * [M. Y. Vardi, P. Wolper, | ||
| *An automata-theoretic approach to automatic program verification*][VardiWolper1986] | ||
| -/ | ||
|
|
||
| @[expose] public section | ||
|
|
||
| namespace Cslib.Logic.LTL | ||
|
|
||
| variable {Atom : Type*} | ||
|
|
||
| /-- Satisfaction relation for LTL over omega-words. | ||
|
|
||
| `Satisfies v i φ` means formula `φ` holds at time point `i` in the omega-word `v`, | ||
| where `v : ℕ → (Atom → Prop)` assigns a set of true atoms to each time point. | ||
|
|
||
| The `untl` case: `φ U ψ` holds at `i` when there exists a future time `j ≥ i` | ||
| where ψ holds (the event), and φ holds at all intermediate points `i ≤ k < j` | ||
| (the guard). -/ | ||
| 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 φ | ||
|
|
||
| /-- A formula holds at all time points in a given omega-word. -/ | ||
| def Valid (v : ℕ → (Atom → Prop)) (φ : Formula Atom) : Prop := | ||
| ∀ i, Satisfies v i φ | ||
|
Comment on lines
+55
to
+56
Collaborator
There was a problem hiding this comment. This definition makes no sense. What needs to be quantified over is |
||
|
|
||
| /-- A formula is satisfiable: it holds at some time point in some omega-word. -/ | ||
| def Satisfiable (φ : Formula Atom) : Prop := | ||
| ∃ (v : ℕ → (Atom → Prop)) (i : ℕ), Satisfies v i φ | ||
|
|
||
| end Cslib.Logic.LTL | ||
|
|
||
| end | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,136 @@ | ||
| /- | ||
| Copyright (c) 2026 Benjamin Brast-McKie. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Benjamin Brast-McKie | ||
| -/ | ||
|
|
||
| module | ||
|
|
||
| public import Cslib.Init | ||
| public import Cslib.Foundations.Logic.Connectives | ||
| public import Mathlib.Order.Notation | ||
|
|
||
| /-! # LTL Formula Type | ||
|
|
||
| This module defines the formula type for Linear Temporal Logic with primitives | ||
| `{atom, bot, imp, next, untl}`. The primitive `next` operator is kept separate from | ||
| `untl`: in full temporal logic, `next φ` is sometimes encoded as `φ U ⊥`, but this | ||
| encoding does not hold in all models (it relies on discreteness and non-triviality). | ||
| An independent primitive `next` avoids this coupling. | ||
|
|
||
| ## Main definitions | ||
|
|
||
| - `Formula` : Inductive type for LTL formulas with constructors | ||
| `atom`, `bot`, `imp`, `next`, `untl` | ||
| - `Formula.someFuture` (◇): `φ U ⊤` — φ holds at some future point | ||
| - `Formula.allFuture` (□): `¬◇¬φ` — φ holds at all future points | ||
| - `Formula.leadsto` (⇝): `□(p → ◇q)` — liveness: every p-state is eventually followed by q | ||
|
|
||
| ## Notation | ||
|
|
||
| Propositional connectives (scoped to `Cslib.Logic.LTL`): | ||
| - `¬` (prefix, 40) : negation (`Formula.neg`) | ||
| - `∧` (infix, 36) : conjunction (`Formula.and`) | ||
| - `∨` (infix, 35) : disjunction (`Formula.or`) | ||
| - `→` (infix, 30) : implication (`Formula.imp`) | ||
| - `↔` (infix, 30) : biconditional (`Formula.iff`) | ||
|
|
||
| Temporal operators (scoped to `Cslib.Logic.LTL`): | ||
| - `𝓤` (infix, 40) : until (`Formula.untl`) | ||
| - `◯` (prefix, 40) : next-step (`Formula.next`) | ||
| - `◇` (prefix, 40) : some future / eventually (`Formula.someFuture`) | ||
| - `□` (prefix, 40) : all future / globally (`Formula.allFuture`) | ||
| - `⇝` (infix, 20) : leads-to, `□(p → ◇q)` (`Formula.leadsto`) | ||
|
|
||
| ## Derived Operators | ||
|
|
||
| In `untl φ ψ`, the first argument `φ` is the **guard** (holds at all intermediate | ||
| points) and the second `ψ` is the **event** (eventually holds at the witness point). | ||
| `someFuture φ` is `⊤ U φ` (⊤ is the trivial guard, φ is the event). | ||
|
|
||
| ## References | ||
|
|
||
| * [A. Pnueli, *The Temporal Logic of Programs*][Pnueli1977] | ||
| * [H. Kamp, *Tense Logic and the Theory of Linear Order*][Kamp1968] | ||
| * [M. Y. Vardi, P. Wolper, | ||
| *An automata-theoretic approach to automatic program verification*][VardiWolper1986] | ||
| -/ | ||
|
|
||
| @[expose] public section | ||
|
|
||
| namespace Cslib.Logic.LTL | ||
|
|
||
| /-- LTL formula type. Primitives: atoms, falsum, implication, next-step, and until. | ||
|
|
||
| `next` is a primitive constructor and is not derived from `untl`. The encoding | ||
| `next φ = φ U ⊥` holds on discrete non-ending sequences but fails in general temporal | ||
| models; keeping `next` primitive supports broader model classes. -/ | ||
| inductive Formula (Atom : Type u) : Type u where | ||
| /-- Atomic proposition. -/ | ||
| | atom (p : Atom) | ||
| /-- Falsum / bottom. -/ | ||
| | bot | ||
| /-- Implication. -/ | ||
| | imp (φ₁ φ₂ : Formula Atom) | ||
| /-- Next-step operator: Xφ holds at t iff φ holds at t+1. -/ | ||
| | next (φ : Formula Atom) | ||
| /-- Until temporal operator: φ₁ U φ₂ (guard U event: φ₁ holds until φ₂). -/ | ||
| | untl (φ₁ φ₂ : Formula Atom) | ||
| deriving DecidableEq, BEq | ||
|
|
||
| /-- Negation: ¬φ := φ → ⊥ -/ | ||
| abbrev Formula.neg (φ : Formula Atom) : Formula Atom := .imp φ .bot | ||
|
|
||
| /-- Verum / top: ⊤ := ⊥ → ⊥ -/ | ||
| abbrev Formula.top : Formula Atom := .imp .bot .bot | ||
|
|
||
| /-- Disjunction: φ₁ ∨ φ₂ := ¬φ₁ → φ₂ -/ | ||
| abbrev Formula.or (φ₁ φ₂ : Formula Atom) : Formula Atom := | ||
| .imp (.imp φ₁ .bot) φ₂ | ||
|
|
||
| /-- Conjunction: φ₁ ∧ φ₂ := ¬(φ₁ → ¬φ₂) -/ | ||
| abbrev Formula.and (φ₁ φ₂ : Formula Atom) : Formula Atom := | ||
| .imp (.imp φ₁ (.imp φ₂ .bot)) .bot | ||
|
|
||
| /-- Biconditional: φ₁ ↔ φ₂ := (φ₁ → φ₂) ∧ (φ₂ → φ₁) -/ | ||
| abbrev Formula.iff (φ₁ φ₂ : Formula Atom) : Formula Atom := | ||
| (φ₁.imp φ₂).and (φ₂.imp φ₁) | ||
|
|
||
| /-- Some future (eventually): ◇φ := ⊤ U φ. | ||
| ⊤ is the trivial guard, φ is the event that eventually holds. -/ | ||
| abbrev Formula.someFuture (φ : Formula Atom) : Formula Atom := | ||
| .untl .top φ | ||
|
|
||
| /-- All future (globally): □φ := ¬◇¬φ -/ | ||
| abbrev Formula.allFuture (φ : Formula Atom) : Formula Atom := | ||
| .neg (.someFuture (.neg φ)) | ||
|
|
||
| /-- Leads-to: p ⇝ q := □(p → ◇q). A liveness property asserting that | ||
| every state satisfying p is eventually followed by a state satisfying q. -/ | ||
| abbrev Formula.leadsto (p q : Formula Atom) : Formula Atom := | ||
| .allFuture (.imp p (.someFuture q)) | ||
|
|
||
| @[inherit_doc] scoped prefix:40 "¬" => Formula.neg | ||
| @[inherit_doc] scoped infix:36 " ∧ " => Formula.and | ||
| @[inherit_doc] scoped infix:35 " ∨ " => Formula.or | ||
| @[inherit_doc] scoped infix:30 " → " => Formula.imp | ||
| @[inherit_doc] scoped infix:30 " ↔ " => Formula.iff | ||
| @[inherit_doc] scoped infix:40 " 𝓤 " => Formula.untl | ||
| @[inherit_doc] scoped prefix:40 "◯" => Formula.next | ||
| @[inherit_doc] scoped prefix:40 "◇" => Formula.someFuture | ||
| @[inherit_doc] scoped prefix:40 "□" => Formula.allFuture | ||
| @[inherit_doc] scoped infix:20 " ⇝ " => Formula.leadsto | ||
|
|
||
| /-- Register `LTL.Formula` as an instance of `LTLConnectives`. -/ | ||
| instance : LTLConnectives (Formula Atom) where | ||
| bot := .bot | ||
| imp := .imp | ||
| untl := .untl | ||
| next := .next | ||
|
|
||
| instance : Bot (Formula Atom) := ⟨.bot⟩ | ||
| instance : Top (Formula Atom) := ⟨.top⟩ | ||
|
|
||
| end Cslib.Logic.LTL | ||
|
|
||
| end |
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Uh oh!
There was an error while loading. Please reload this page.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Several comments:
i, because an LTL formula can only talk about now (which can be identified with time 0) and future.ωSequencedeveloped inCslib.Foundations.Data.OmegaSequence, rather than directly functions of typeℕ → ....Statetype, a valuation functionv : State → Atom → Prop, andSatisfies : (State → Atom → Prop) → ωSequence State → Fomula Atom → Prop. You should be able to work out the details.