Simulation and Similarity

A simulation is a binary relation on the states of an LTS: if two states s1 and s2 are related by a simulation, then s2 can mimic all transitions of s1. 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.

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

Main definitions

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

Notations

• s1 ≤[lts] s2: the states s1 and s2 are similar in the LTS lts.
• s1 ≤≥[lts] s2: the states s1 and s2 are simulation equivalent in the LTS lts.

Main statements

• SimulationEquiv.eqv: simulation equivalence is an equivalence relation.

def Cslib.Simulation {State : Type u} {Label : Type v} (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

• Cslib.Simulation lts r = ∀ (s1 s2 : State), r s1 s2 → ∀ (μ : Label) (s1' : State), lts.Tr s1 μ s1' → ∃ (s2' : State), lts.Tr s2 μ s2' ∧ r s1' s2'

def Cslib.Similarity {State : Type u} {Label : Type v} (lts : LTS State Label) : State → State → Prop

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

Equations

• s1 ≤[lts] s2 = ∃ (r : State → State → Prop), r s1 s2 ∧ Cslib.Simulation lts r

def Cslib.«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.

theorem Cslib.Similarity.refl {State : Type u} {Label : Type v} (lts : LTS State Label) (s : State) : s ≤[lts] s

Similarity is reflexive.

theorem Cslib.Simulation.comp {State : Type u} {Label : Type v} (lts : LTS State Label) (r1 r2 : State → State → Prop) (h1 : Simulation lts r1) (h2 : Simulation lts r2) : Simulation lts (Relation.Comp r1 r2)

The composition of two simulations is a simulation.

theorem Cslib.Similarity.trans {State : Type u} {Label : Type v} (lts : LTS State Label) {s1 s2 s3 : State} (h1 : s1 ≤[lts] s2) (h2 : s2 ≤[lts] s3) : s1 ≤[lts] s3

Similarity is transitive.

def Cslib.SimulationEquiv {State : Type u} {Label : Type v} (lts : LTS State Label) : State → State → Prop

Simulation equivalence relates all states s1 and s2 such that s1 ≤[lts] s2 and s2 ≤[lts] s1.

Equations

• s1 ≤≥[lts] s2 = (s1 ≤[lts] s2 ∧ s2 ≤[lts] s1)

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

Notation for simulation equivalence.

Equations

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

theorem Cslib.SimulationEquiv.refl {State : Type u} {Label : Type v} (lts : LTS State Label) (s : State) : s ≤≥[lts] s

Simulation equivalence is reflexive.

theorem Cslib.SimulationEquiv.symm {State : Type u} {Label : Type v} (lts : LTS State Label) {s1 s2 : State} (h : s1 ≤≥[lts] s2) : s2 ≤≥[lts] s1

Simulation equivalence is symmetric.

theorem Cslib.SimulationEquiv.trans {State : Type u} {Label : Type v} (lts : LTS State Label) {s1 s2 s3 : State} (h1 : s1 ≤≥[lts] s2) (h2 : s2 ≤≥[lts] s3) : s1 ≤≥[lts] s3

Simulation equivalence is transitive.

theorem Cslib.SimulationEquiv.eqv {State : Type u} {Label : Type v} (lts : LTS State Label) : Equivalence (SimulationEquiv lts)

Simulation equivalence is an equivalence relation.

instance Cslib.instTransSimulationEquiv {State : Type u} {Label : Type v} (lts : LTS State Label) : Trans (SimulationEquiv lts) (SimulationEquiv lts) (SimulationEquiv lts)

calc support for simulation equivalence.

Equations

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