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.