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.

def Cslib.LTS.Example.countdownLTS : LTS ℕ Unit

The countdown LTS takes a natural number to its predecessor.

Equations

• Cslib.LTS.Example.countdownLTS = { Tr := fun (n : ℕ) (x : Unit) (m : ℕ) => n = m + 1 }

instance Cslib.LTS.Example.countdownLTS_terminating : countdownLTS.Terminating

theorem Cslib.LTS.Example.countdownLTS_not_bounded : ¬countdownLTS.Bounded

The countdown LTS is not bounded.

def Cslib.LTS.Example.successorLTS : LTS ℕ Unit

The successor LTS takes each natural number to its successor.

Equations

• Cslib.LTS.Example.successorLTS = { Tr := fun (n : ℕ) (x : Unit) (m : ℕ) => m = n + 1 }

instance Cslib.LTS.Example.successorLTS_acyclic : successorLTS.Acyclic

theorem Cslib.LTS.Example.successorLTS_not_terminating : ¬successorLTS.Terminating

The successor LTS is not terminating.

def Cslib.LTS.Example.selfLoopLTS : LTS Unit Unit

The self-loop LTS has a transition from its unique state to itself.

Equations

• Cslib.LTS.Example.selfLoopLTS = { Tr := fun (x x_1 x_2 : Unit) => True }

theorem Cslib.LTS.Example.selfLoopLTS_not_acyclic : ¬selfLoopLTS.Acyclic

The self-loop LTS is not acyclic.