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 bisimulation 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 Simulation {State : Type u} {Label : Type v} (lts : LTS State Label) (r : Rel State State) : 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

• 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 Similarity {State : Type u} {Label : Type v} (lts : LTS State Label) : Rel State State

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

Equations

• s1 ≤[lts] s2 = ∃ (r : Rel State State), r s1 s2 ∧ Simulation lts r

def «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 Similarity.refl {State : Type u} {Label : Type v} (lts : LTS State Label) (s : State) : s ≤[lts] s

Similarity is reflexive.

theorem Simulation.comp {State : Type u} {Label : Type v} (lts : LTS State Label) (r1 r2 : Rel State State) (h1 : Simulation lts r1) (h2 : Simulation lts r2) : Simulation lts (r1.comp r2)

The composition of two simulations is a simulation.

theorem 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 SimulationEquiv {State : Type u} {Label : Type v} (lts : LTS State Label) : Rel State State

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 «term_≤≥[_]_» : Lean.TrailingParserDescr

Notation for simulation equivalence.

Equations

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

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

Simulation equivalence is reflexive.

theorem 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 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 SimulationEquiv.eqv {State : Type u} {Label : Type v} (lts : LTS State Label) : Equivalence (SimulationEquiv lts)

Simulation equivalence is an equivalence relation.