Termination of LTS #
This module relates global execution bounds, well-founded termination, and acyclicity.
theorem Cslib.LTS.Bounded.toTerminating {State : Type u} {Label : Type v} (lts : LTS State Label) (h : lts.Bounded) :
lts.Terminating
Bounded LTSs are terminating.
instance Cslib.LTS.bounded_terminating {State : Type u} {Label : Type v} (lts : LTS State Label) [lts.Bounded] :
lts.Terminating
A bounded LTS is available as a terminating LTS through typeclass inference.
theorem Cslib.LTS.Terminating.toAcyclic {State : Type u} {Label : Type v} (lts : LTS State Label) (h : lts.Terminating) :
lts.Acyclic
Terminating LTSs are acyclic.
instance Cslib.LTS.terminating_acyclic {State : Type u} {Label : Type v} (lts : LTS State Label) [lts.Terminating] :
lts.Acyclic
A terminating LTS is available as an acyclic LTS through typeclass inference.
theorem Cslib.LTS.Acyclic.toBoundedUpTo {State : Type u} {Label : Type v} (lts : LTS State Label) [Finite State] (h : lts.Acyclic) :
lts.BoundedUpTo (Nat.card State)
On a finite state space, an acyclic LTS has execution length strictly less than the number of states.
theorem Cslib.LTS.Acyclic.toTerminating {State : Type u} {Label : Type v} (lts : LTS State Label) [Finite State] (h : lts.Acyclic) :
lts.Terminating
On a finite state space, acyclic LTSs are terminating.
def Cslib.LTS.MayTerminate {State : Type u} {Label : Type v} (lts : LTS State Label) (Terminated : State → Prop) (s : State) :
A state 'may terminate' if it can reach a terminated state. The definition of Terminated
is a parameter.
Equations
- lts.MayTerminate Terminated s = ∃ (s' : State), Terminated s' ∧ lts.CanReach s s'
Instances For
def Cslib.LTS.Stuck {State : Type u} {Label : Type v} (lts : LTS State Label) (Terminated : State → Prop) (s : State) :
A state 'is stuck' if it is not terminated and cannot go forward. The definition of Terminated
is a parameter.