Labelled transition systems with independence (Lanese–Phillips–Ulidowski)

structure LTSI (L : Type u_2) : Type (max u_2 (u_3 + 1))

An LTSI.

• State : Type u_3
• init : self.State
• step : self.State → L → self.State → Prop
• indep : self.State → L → self.State → L → self.State → Prop

structure LTSI.LPV {L : Type u_1} (T : LTSI L) : Prop

LPV axioms for an LTSI.

• indep_step_left {s : T.State} {a : L} {s₁ : T.State} {b : L} {s₂ : T.State} : T.indep s a s₁ b s₂ → T.step s a s₁
• indep_step_right {s : T.State} {a : L} {s₁ : T.State} {b : L} {s₂ : T.State} : T.indep s a s₁ b s₂ → T.step s b s₂
• indep_irrefl {s : T.State} {a : L} {s' : T.State} : ¬T.indep s a s' a s'
• indep_symm {s : T.State} {a : L} {s₁ : T.State} {b : L} {s₂ : T.State} : T.indep s a s₁ b s₂ → T.indep s b s₂ a s₁
• square {s : T.State} {a : L} {s₁ : T.State} {b : L} {s₂ : T.State} : T.indep s a s₁ b s₂ → ∃ (u : T.State), T.step s₁ b u ∧ T.step s₂ a u

structure Bisim {L : Type u_1} (S : LTSI L) (T : LTSI L) (R : S.State → T.State → Prop) : Prop

A (strong) bisimulation between two LTSIs: related initial states and steps matched both ways. Independence is ignored.

• init : R S.init T.init
• forward {s : S.State} {t : T.State} {a : L} {s' : S.State} : R s t → S.step s a s' → ∃ (t' : T.State), T.step t a t' ∧ R s' t'
• backward {s : S.State} {t : T.State} {a : L} {t' : T.State} : R s t → T.step t a t' → ∃ (s' : S.State), S.step s a s' ∧ R s' t'

def Bisimilar {L : Type u_1} (S : LTSI L) (T : LTSI L) : Prop

Existence of a bisimulation.

Equations

• Bisimilar S T = ∃ (R : S.State → T.State → Prop), Bisim S T R

theorem Bisimilar.refl {L : Type u_1} (S : LTSI L) : Bisimilar S S

theorem Bisimilar.symm {L : Type u_1} {S : LTSI L} {T : LTSI L} : Bisimilar S T → Bisimilar T S

inductive DirLabel (L : Type u_2) : Type u_2

A directed label.

• fwd {L : Type u_2} : L → DirLabel L
• bwd {L : Type u_2} : L → DirLabel L

def instDecidableEqDirLabel.decEq {L✝ : Type u_2} [DecidableEq L✝] (x✝ x✝¹ : DirLabel L✝) : Decidable (x✝ = x✝¹)

Equations

• instDecidableEqDirLabel.decEq (DirLabel.fwd a) (DirLabel.fwd b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqDirLabel.decEq (DirLabel.fwd a) (DirLabel.bwd a_1) = isFalse ⋯
• instDecidableEqDirLabel.decEq (DirLabel.bwd a) (DirLabel.fwd a_1) = isFalse ⋯
• instDecidableEqDirLabel.decEq (DirLabel.bwd a) (DirLabel.bwd b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance instDecidableEqDirLabel {L✝ : Type u_2} [DecidableEq L✝] : DecidableEq (DirLabel L✝)

Equations

• instDecidableEqDirLabel = instDecidableEqDirLabel.decEq

def DirLabel.rev {L : Type u_1} : DirLabel L → DirLabel L

Equations

• (DirLabel.fwd a).rev = DirLabel.bwd a
• (DirLabel.bwd a).rev = DirLabel.fwd a

def DirLabel.label {L : Type u_1} : DirLabel L → L

Equations

• (DirLabel.fwd a).label = a
• (DirLabel.bwd a).label = a

def DirLabel.isFwd {L : Type u_1} : DirLabel L → Prop

Equations

• (DirLabel.fwd a).isFwd = True
• (DirLabel.bwd a).isFwd = False

theorem DirLabel.rev_rev {L : Type u_1} (la : DirLabel L) : la.rev.rev = la

Reversal is an involution.

structure RLTSI (L : Type u_2) extends LTSI (DirLabel L) : Type (max u_2 (u_3 + 1))

A reversible LTSI: labels carry direction and forward steps are reversible.

• State : Type u_3
• init : self.State
• step : self.State → DirLabel L → self.State → Prop
• indep : self.State → DirLabel L → self.State → DirLabel L → self.State → Prop
• step_rev {s : self.State} {a : L} {s' : self.State} : self.step s (DirLabel.fwd a) s' ↔ self.step s' (DirLabel.bwd a) s

structure RLTSI.LPV {L : Type u_1} (T : RLTSI L) extends T.LPV : Prop

LPV axioms for a reversible LTSI.

• indep_step_left {s : T.State} {a : DirLabel L} {s₁ : T.State} {b : DirLabel L} {s₂ : T.State} : T.indep s a s₁ b s₂ → T.step s a s₁
• indep_step_right {s : T.State} {a : DirLabel L} {s₁ : T.State} {b : DirLabel L} {s₂ : T.State} : T.indep s a s₁ b s₂ → T.step s b s₂
• indep_irrefl {s : T.State} {a : DirLabel L} {s' : T.State} : ¬T.indep s a s' a s'
• indep_symm {s : T.State} {a : DirLabel L} {s₁ : T.State} {b : DirLabel L} {s₂ : T.State} : T.indep s a s₁ b s₂ → T.indep s b s₂ a s₁
• square {s : T.State} {a : DirLabel L} {s₁ : T.State} {b : DirLabel L} {s₂ : T.State} : T.indep s a s₁ b s₂ → ∃ (u : T.State), T.step s₁ b u ∧ T.step s₂ a u
• BTI {s : T.State} {a : L} {s₁ : T.State} {b : L} {s₂ : T.State} : T.step s (DirLabel.bwd a) s₁ → T.step s (DirLabel.bwd b) s₂ → a ≠ b ∨ s₁ ≠ s₂ → T.indep s (DirLabel.bwd a) s₁ (DirLabel.bwd b) s₂