IsSimulation and Similarity

A simulation is a binary relation on the states of two LTSs: if two states s₁ and s2 are related by a simulation, then s2 can mimic all transitions of s₁ in their respective LTSs. Furthermore, the derivatives reaches through these transitions remain related by the simulation.

Similarity is the largest simulation: given an LTS, it relates any two states that are related by a simulation for that LTS.

The module provides abbreviations for the homogeneous case of comparing states in the same LTS.

For an introduction to theory of simulation, we refer to [Sangiorgi2011].

Main definitions

• IsSimulation lts₁ lts₂ r: the relation r on the states of lts₁ and lts₂ is a simulation.
• Similarity lts₁ lts₂ is the binary relation that relates any two states related by some simulation on lts₁ and lts₂.
• SimulationEquiv lts₁ lts₂ is the binary relation on the states of lts₁ and lts₂ that relates any two states similar to each other.

Notations

• s₁ ≤[lts₁, lts₂] s₂: the states s₁ and s2 are similar under lts₁ and lts₂.
• s₁ ≤≥[lts₁, lts₂] s2: the states s₁ and s2 are simulation equivalent under lts₁ and lts₂.

Main statements

• HomSimulationEquiv.eqv: homogeneous simulation equivalence is an equivalence relation.

def Cslib.LTS.IsSimulation {State₁ : Type u_1} {Label : Type u_2} {State₂ : Type u_3} (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) (r : State₁ → State₂ → Prop) : Prop

A relation is a simulation if, whenever it relates two states in an lts, any transition originating from the first state is mimicked by a transition from the second state and the reached derivatives are themselves related.

Equations

• lts₁.IsSimulation lts₂ r = ∀ (s₁ : State₁) (s2 : State₂), r s₁ s2 → ∀ (μ : Label) (s₁' : State₁), lts₁.Tr s₁ μ s₁' → ∃ (s2' : State₂), lts₂.Tr s2 μ s2' ∧ r s₁' s2'

@[reducible, inline]

abbrev Cslib.LTS.IsHomSimulation {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) (r : State → State → Prop) : Prop

A homogeneous simulation is a simulation where the underlying LTSs are the same.

Equations

• lts.IsHomSimulation = lts.IsSimulation lts

def Cslib.LTS.Similarity {State₁ : Type u_1} {Label : Type u_2} {State₂ : Type u_3} (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : State₁ → State₂ → Prop

Two states are similar if they are related by some simulation.

Equations

• lts₁.Similarity lts₂ s₁ s2 = ∃ (r : State₁ → State₂ → Prop), r s₁ s2 ∧ lts₁.IsSimulation lts₂ r

def Cslib.LTS.«term_≤[_,_]_» : Lean.TrailingParserDescr

Notation for similarity.

Differently from standard pen-and-paper presentations, we require the lts to be mentioned explicitly.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Cslib.LTS.HomSimilarity {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) : State → State → Prop

Homogeneous similarity is similarity where the underlying LTSs are the same.

Equations

• lts.HomSimilarity = lts.Similarity lts

def Cslib.LTS.«term_≤[_]_» : Lean.TrailingParserDescr

Notation for homogeneous similarity.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.LTS.HomSimilarity.refl {State : Type u_1} {Label✝ : Type u_2} {lts : LTS State Label✝} (s : State) : lts.HomSimilarity s s

Homogeneous similarity is reflexive.

theorem Cslib.LTS.IsSimulation.comp {State₁ : Type u_1} {State₂ : Type u_2} {State₃ : Type u_3} {Label✝ : Type u_4} {lts₁ : LTS State₁ Label✝} {lts₂ : LTS State₂ Label✝} {lts₃ : LTS State₃ Label✝} (r1 : State₁ → State₂ → Prop) (r2 : State₂ → State₃ → Prop) (h1 : lts₁.IsSimulation lts₂ r1) (h2 : lts₂.IsSimulation lts₃ r2) : lts₁.IsSimulation lts₃ (Relation.Comp r1 r2)

The composition of two simulations is a simulation.

theorem Cslib.LTS.Similarity.trans {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} {s₁ : State✝} {s2 : State✝¹} {State✝² : Type u_4} {lts₃ : LTS State✝² Label✝} {s₃ : State✝²} (h1 : lts₁.Similarity lts₂ s₁ s2) (h2 : lts₂.Similarity lts₃ s2 s₃) : lts₁.Similarity lts₃ s₁ s₃

Similarity is transitive.

def Cslib.LTS.SimulationEquiv {State₁ : Type u_1} {Label : Type u_2} {State₂ : Type u_3} (lts₁ : LTS State₁ Label) (lts₂ : LTS State₂ Label) : State₁ → State₂ → Prop

Simulation equivalence relates all states s₁ and s2 such that s₁ ≤[lts₁ lts₂] s2 and s2 ≤[lts₂ lts₁] s₁.

Equations

• lts₁.SimulationEquiv lts₂ s₁ s2 = (lts₁.Similarity lts₂ s₁ s2 ∧ lts₂.Similarity lts₁ s2 s₁)

def Cslib.LTS.«term_≤≥[_,_]_» : Lean.TrailingParserDescr

Notation for simulation equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev Cslib.LTS.HomSimulationEquiv {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) : State → State → Prop

Homogeneous simulation equivalence.

Equations

• lts.HomSimulationEquiv = lts.SimulationEquiv lts

def Cslib.LTS.«term_≤≥[_]_» : Lean.TrailingParserDescr

Notation for homogeneous simulation equivalence.

Equations

• One or more equations did not get rendered due to their size.

theorem Cslib.LTS.HomSimulationEquiv.refl {State : Type u_1} {Label✝ : Type u_2} {lts : LTS State Label✝} (s : State) : lts.HomSimulationEquiv s s

Homogeneous simulation equivalence is reflexive.

theorem Cslib.LTS.SimulationEquiv.symm {State : Type u_1} {Label✝ : Type u_2} {lts₁ lts₂ : LTS State Label✝} {s₁ s2 : State} (h : lts₁.SimulationEquiv lts₂ s₁ s2) : lts₂.SimulationEquiv lts₁ s2 s₁

Simulation equivalence is symmetric.

theorem Cslib.LTS.SimulationEquiv.trans {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} {s₁ : State✝} {s2 : State✝¹} {State✝² : Type u_4} {lts₃ : LTS State✝² Label✝} {s₃ : State✝²} (h1 : lts₁.SimulationEquiv lts₂ s₁ s2) (h2 : lts₂.SimulationEquiv lts₃ s2 s₃) : lts₁.SimulationEquiv lts₃ s₁ s₃

Simulation equivalence is transitive.

theorem Cslib.LTS.HomSimulationEquiv.eqv {State✝ : Type u_1} {Label✝ : Type u_2} {lts : LTS State✝ Label✝} : Equivalence fun (x1 x2 : State✝) => lts.HomSimulationEquiv x1 x2

Homogeneous simulation equivalence is an equivalence relation.

@[implicit_reducible]

instance Cslib.LTS.instTransSimulationEquiv {State✝ : Type u_1} {Label✝ : Type u_2} {lts₁ : LTS State✝ Label✝} {State✝¹ : Type u_3} {lts₂ : LTS State✝¹ Label✝} {State✝² : Type u_4} {lts₃ : LTS State✝² Label✝} : Trans (lts₁.SimulationEquiv lts₂) (lts₂.SimulationEquiv lts₃) (lts₁.SimulationEquiv lts₃)

calc support for simulation equivalence.

Equations

• Cslib.LTS.instTransSimulationEquiv = { trans := ⋯ }