leanprover · fmontesi · Aug 2, 2026 · Jul 25, 2026 · Jul 30, 2026 · Jul 30, 2026
@@ -93,6 +93,7 @@ public import Cslib.Foundations.Semantics.FLTS.Prod
 public import Cslib.Foundations.Semantics.LTS.Basic
 public import Cslib.Foundations.Semantics.LTS.Bisimulation
 public import Cslib.Foundations.Semantics.LTS.Divergence
+public import Cslib.Foundations.Semantics.LTS.ExampleTermination
 public import Cslib.Foundations.Semantics.LTS.Execution
 public import Cslib.Foundations.Semantics.LTS.HasTau
 public import Cslib.Foundations.Semantics.LTS.LTSCat.Basic

@@ -196,6 +196,10 @@ theorem Terminating.toTransGen (ht : Terminating r) : Terminating (TransGen r) :
   simp_rw [iff_forall_sn, SN.iff_transGen] at ht ⊢
   exact ht
 
+/-- A terminating relation is acyclic. -/
+theorem Terminating.toAcyclic (ht : Terminating r) : Acyclic r :=
+  ⟨fun x hx => ht.toTransGen.irrefl.irrefl x hx⟩
+
 theorem Terminating.ofTransGen : Terminating (TransGen r) → Terminating r := by
   simp_rw [iff_forall_sn, SN.iff_transGen]
   exact id

@@ -89,6 +89,10 @@ abbrev Normalizing (r : α → α → Prop) : Prop :=
 the inverse of `r`. -/
 abbrev SN (r : α → α → Prop) := Acc (fun a b => r b a)
 
+/-- A relation is acyclic if its transitive closure is irreflexive, equivalently if it admits no
+nonempty cycle. -/
+abbrev Acyclic (r : α → α → Prop) := Std.Irrefl (TransGen r)
+
 /-- A relation is terminating when the inverse of its transitive closure is well-founded.
   Note that this is also called Noetherian or strongly normalizing in the literature. -/
 abbrev Terminating (r : α → α → Prop) := WellFounded (fun a b => r b a)

@@ -6,7 +6,7 @@ Authors: Fabrizio Montesi
 
 module
 
-public import Cslib.Init
+public import Cslib.Foundations.Relation.Defs
 public import Mathlib.Data.Set.Finite.Basic
 public import Mathlib.Order.SetNotation
 
@@ -25,8 +25,12 @@ relation `Tr` between states. We follow the style and conventions in [Sangiorgi2
 - `LTS.MTr` extends the transition relation of any LTS to a multistep transition relation,
 formalising the inference system and admissible rules for such relations in [Montesi2023].
 
+- `LTS.BoundedUpTo` records an explicit global execution-length bound. `LTS.Bounded`,
+`LTS.Terminating`, and `LTS.Acyclic` distinguish globally bounded execution length, absence of
+infinite executions, and absence of nonempty cycles.
+
 - Definitions for all the common classes of LTSs: image-finite, finitely branching, finite-state,
-finite, and deterministic.
+and deterministic.
 
 ## Main statements
 
@@ -63,6 +67,10 @@ structure LTS (State : Type u) (Label : Type v) where
 
 namespace LTS
 
+/-- The unlabelled transition relation underlying an LTS. -/
+def UnlabelledTr (lts : LTS State Label) : State → State → Prop :=
+  fun s1 s2 => ∃ μ, lts.Tr s1 μ s2
+
 section MultiStep
 
 /-! ## Multistep transitions and executions with finite traces
@@ -356,15 +364,25 @@ attribute [instance] FinitelyBranching.image_finite FinitelyBranching.finite_sta
 /-- Every LTS with finite types for states and labels is also finitely branching. -/
 instance FinitelyBranching.of_finite [Finite State] [Finite Label] : lts.FinitelyBranching where
 
-/-- An LTS is acyclic if there are no infinite multistep transitions. -/
-class Acyclic (lts : LTS State Label) where
-  acyclic : ∃ n, ∀ s1 μs s2, lts.MTr s1 μs s2 → μs.length < n
+/-- An LTS is bounded up to `n` if every finite execution has length strictly less than `n`. -/
+def BoundedUpTo (lts : LTS State Label) (n : ℕ) : Prop :=
+  ∀ s1 μs s2, lts.MTr s1 μs s2 → μs.length < n
 
-/-- An LTS is finite if it is finite-state and acyclic.
+/-- An LTS is bounded if there is a global bound on the length of all of its finite executions. -/
+class Bounded (lts : LTS State Label) where
+  bounded : ∃ n, lts.BoundedUpTo n
+
+/-- An LTS is terminating if its underlying unlabelled transition relation is terminating,
+equivalently if it admits no infinite execution. -/
+class Terminating (lts : LTS State Label) where
+  terminating : Relation.Terminating lts.UnlabelledTr
+
+/-- An LTS is acyclic if its underlying unlabelled transition relation contains no nonempty
+cycle. -/
+class Acyclic (lts : LTS State Label) where
+  [acyclic : Relation.Acyclic lts.UnlabelledTr]
 
-We call this `FiniteLTS` instead of just `Finite` to avoid confusion with the standard `Finite`
-class. -/
-class FiniteLTS [Finite State] (lts : LTS State Label) extends lts.Acyclic
+attribute [instance] Acyclic.acyclic
 
 end Classes
 

@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+
+public import Cslib.Foundations.Semantics.LTS.Termination
+public import Mathlib.Order.WellFounded
+
+/-!
+# Examples separating boundedness, termination, and acyclicity
+
+On infinite state spaces, boundedness, termination, and acyclicity are distinct properties.
+This file gives concrete LTSs witnessing that the converses in
+`Bounded → Terminating → Acyclic` do not hold in general.
+-/
+
+@[expose] public section
+
+namespace Cslib.LTS.Example
+
+/-- The countdown LTS takes a natural number to its predecessor. -/
+def countdownLTS : LTS ℕ Unit where
+  Tr n _ m := n = m + 1
+
+instance countdownLTS_terminating : countdownLTS.Terminating where
+  terminating := by
+    apply Subrelation.wf _ Nat.lt_wfRel.wf
+    rintro s2 s1 ⟨_, rfl⟩
+    exact Nat.lt_succ_self s2
+
+example : countdownLTS.Acyclic := inferInstance
+example : Relation.Acyclic countdownLTS.UnlabelledTr := inferInstance
+
+private theorem countdownLTS_mTr (n : ℕ) :
+    countdownLTS.MTr n (List.replicate n ()) 0 := by
+  induction n with
+  | zero => exact .refl
+  | succ n ih =>
+      simpa [List.replicate_succ] using MTr.stepL (by simp [countdownLTS]) ih
+
+/-- The countdown LTS is not bounded. -/
+theorem countdownLTS_not_bounded : ¬ countdownLTS.Bounded := by
+  rintro ⟨bound, hbound⟩
+  simpa using hbound bound (List.replicate bound ()) 0 (countdownLTS_mTr bound)
+
+/-- The successor LTS takes each natural number to its successor. -/
+def successorLTS : LTS ℕ Unit where
+  Tr n _ m := m = n + 1
+
+private theorem successorLTS_transGen_lt {n m : ℕ}
+    (h : Relation.TransGen successorLTS.UnlabelledTr n m) : n < m := by
+  apply Relation.transGen_minimal (r' := (· < ·)) at h
+  · exact h
+  · rintro n m ⟨μ, htr⟩
+    simp only [successorLTS] at htr
+    omega
+
+instance successorLTS_acyclic : successorLTS.Acyclic where
+  acyclic := ⟨fun n h => (Nat.lt_irrefl n) (successorLTS_transGen_lt h)⟩
+
+/-- The successor LTS is not terminating. -/
+theorem successorLTS_not_terminating : ¬ successorLTS.Terminating := by
+  intro h
+  exact (Relation.Terminating.iff_isEmpty_chain.mp h.terminating).false
+    ⟨fun n => n, fun n => ⟨(), by simp [successorLTS]⟩⟩
+
+/-- The self-loop LTS has a transition from its unique state to itself. -/
+def selfLoopLTS : LTS Unit Unit where
+  Tr _ _ _ := True
+
+/-- The self-loop LTS is not acyclic. -/
+theorem selfLoopLTS_not_acyclic : ¬ selfLoopLTS.Acyclic :=
+  fun h => h.acyclic.irrefl () (.single ⟨(), trivial⟩)
+
+end Cslib.LTS.Example
@@ -84,6 +84,11 @@ theorem Execution.to_mTr (hexec : lts.Execution s1 μs s2 ss) :
         apply this
       · grind
 
+/-- The states visited by an execution form a chain in the underlying unlabelled relation. -/
+theorem Execution.isChain (hexec : lts.Execution s1 μs s2 ss) :
+    ss.IsChain lts.UnlabelledTr := by
+  grind [Execution, List.isChain_iff_getElem, UnlabelledTr]
+
 open scoped Execution
 /-- Correspondence of multistep transitions and executions. -/
 @[scoped grind =]

@@ -32,6 +32,61 @@ labels `μs`. -/
 def MTr.toRelation (lts : LTS State Label) (μs : List Label) : State → State → Prop :=
   fun s1 s2 => lts.MTr s1 μs s2
 
+section UnlabelledPaths
+
+variable (lts : LTS State Label)
+
+/-- A multistep transition induces a reflexive-transitive path in the underlying unlabelled
+transition relation. -/
+theorem MTr.toReflTransGen (h : lts.MTr s1 μs s2) :
+    Relation.ReflTransGen lts.UnlabelledTr s1 s2 := by
+  induction h with
+  | refl => exact .refl
+  | stepL htr _ ih => exact ih.head ⟨_, htr⟩
+
+/-- A nonempty multistep transition induces a nonempty path in the underlying unlabelled
+transition relation. -/
+theorem MTr.toTransGen (h : lts.MTr s1 μs s2) (hne : μs ≠ []) :
+    Relation.TransGen lts.UnlabelledTr s1 s2 := by
+  cases h with
+  | refl => contradiction
+  | stepL htr hmtr => exact Relation.TransGen.head' ⟨_, htr⟩ (hmtr.toReflTransGen lts)
+
+/-- The reflexive-transitive closure of the underlying unlabelled transition relation is exactly
+reachability in the LTS. -/
+theorem reflTransGen_unlabelledTr_iff :
+    Relation.ReflTransGen lts.UnlabelledTr s1 s2 ↔ lts.CanReach s1 s2 := by
+  constructor
+  · intro h
+    induction h with
+    | refl => exact ⟨[], .refl⟩
+    | tail _ htr ih =>
+        obtain ⟨μs, hmtr⟩ := ih
+        obtain ⟨μ, htr⟩ := htr
+        exact ⟨μs ++ [μ], hmtr.stepR lts htr⟩
+  · rintro ⟨μs, hmtr⟩
+    exact hmtr.toReflTransGen lts
+
+/-- The transitive closure of the underlying unlabelled transition relation is exactly the
+nonempty multistep transitions of the LTS. -/
+theorem transGen_unlabelledTr_iff :
+    Relation.TransGen lts.UnlabelledTr s1 s2 ↔
+      ∃ μs, μs ≠ [] ∧ lts.MTr s1 μs s2 := by
+  constructor
+  · intro h
+    induction h with
+    | single htr =>
+        obtain ⟨μ, htr⟩ := htr
+        exact ⟨[μ], by simp, MTr.single lts htr⟩
+    | tail _ htr ih =>
+        obtain ⟨μs, hne, hmtr⟩ := ih
+        obtain ⟨μ, htr⟩ := htr
+        exact ⟨μs ++ [μ], by simp, hmtr.stepR lts htr⟩
+  · rintro ⟨μs, hne, hmtr⟩
+    exact hmtr.toTransGen lts hne
+
+end UnlabelledPaths
+
 /-! ### Calc tactic support for MTr -/
 
 /-- Transitions can be chained. -/

@@ -6,10 +6,16 @@ Authors: Fabrizio Montesi
 
 module
 
-public import Cslib.Foundations.Semantics.LTS.Basic
+public import Cslib.Foundations.Relation.Confluence
+public import Cslib.Foundations.Semantics.LTS.Execution
+public import Mathlib.Data.Fintype.Card
+public import Mathlib.Data.List.Chain
+public import Mathlib.SetTheory.Cardinal.Finite
 
 /-!
 # Termination of LTS
+
+This module relates global execution bounds, well-founded termination, and acyclicity.
 -/
 
 @[expose] public section
@@ -20,6 +26,61 @@ universe u v
 
 variable {State : Type u} {Label : Type v} (lts : LTS State Label) (Terminated : State → Prop)
 
+/-- Bounded LTSs are terminating. -/
+theorem Bounded.toTerminating (h : lts.Bounded) : lts.Terminating := by
+  constructor
+  rw [Relation.Terminating.iff_isEmpty_chain]
+  constructor
+  rintro ⟨f, hf⟩
+  change ∀ n, lts.UnlabelledTr (f n) (f (n + 1)) at hf
+  obtain ⟨bound, hbound⟩ := h.bounded
+  have hpaths : ∀ n, ∃ μs, μs.length = n ∧ lts.MTr (f 0) μs (f n) := by
+    intro n
+    induction n with
+    | zero => exact ⟨[], rfl, .refl⟩
+    | succ n ih =>
+        obtain ⟨μs, hlength, hmtr⟩ := ih
+        obtain ⟨μ, htr⟩ := hf n
+        exact ⟨μs ++ [μ], by simp [hlength], hmtr.stepR lts htr⟩
+  obtain ⟨μs, hlength, hmtr⟩ := hpaths bound
+  have := hbound (f 0) μs (f bound) hmtr
+  omega
+
+/-- A bounded LTS is available as a terminating LTS through typeclass inference. -/
+instance bounded_terminating [lts.Bounded] : lts.Terminating :=
+  (inferInstance : lts.Bounded).toTerminating
+
+/-- Terminating LTSs are acyclic. -/
+theorem Terminating.toAcyclic (h : lts.Terminating) : lts.Acyclic where
+  acyclic := h.terminating.toAcyclic
+
+/-- A terminating LTS is available as an acyclic LTS through typeclass inference. -/
+instance terminating_acyclic [lts.Terminating] : lts.Acyclic :=
+  (inferInstance : lts.Terminating).toAcyclic
+
+/-- On a finite state space, an acyclic LTS has execution length strictly less than the number of
+states. -/
+theorem Acyclic.toBoundedUpTo [Finite State] (h : lts.Acyclic) :
+    lts.BoundedUpTo (Nat.card State) := by
+  classical
+  letI := Fintype.ofFinite State
+  rw [Nat.card_eq_fintype_card]
+  intro s1 μs s2 hmtr
+  obtain ⟨states, hexec⟩ := Execution.of_mTr hmtr
+  have hchain : states.IsChain (Relation.TransGen lts.UnlabelledTr) :=
+    hexec.isChain.imp_of_mem_imp fun _ _ _ _ htr => .single htr
+  letI : Std.Irrefl (Relation.TransGen lts.UnlabelledTr) := h.acyclic
+  have hcard := hchain.pairwise.nodup.length_le_card
+  grind [Execution]
+
+/-- On a finite state space, acyclic LTSs are bounded. -/
+theorem Acyclic.toBounded [Finite State] (h : lts.Acyclic) : lts.Bounded :=
+  ⟨Nat.card State, h.toBoundedUpTo⟩
+
+/-- On a finite state space, acyclic LTSs are terminating. -/
+theorem Acyclic.toTerminating [Finite State] (h : lts.Acyclic) : lts.Terminating :=
+  h.toBounded.toTerminating
+
 /-- A state 'may terminate' if it can reach a terminated state. The definition of `Terminated`
 is a parameter. -/
 def MayTerminate (s : State) : Prop := ∃ s', Terminated s' ∧ lts.CanReach s s'