Simulation

IsSimulationdef

A relation is a simulation when, whenever it relates two states, every transition of the first can be matched by the second with the results still related — the second system can do everything the first can.

def IsSimulation {S₁ S₂ Label : Type*}
    (lts₁ : LTS S₁ Label) (lts₂ : LTS S₂ Label) (r : S₁ → S₂ → Prop) : Prop :=
  ∀ ⦃s₁ s₂⦄, r s₁ s₂ → ∀ μ, ∀ t₁, lts₁.Tr s₁ μ t₁ → ∃ t₂, lts₂.Tr s₂ μ t₂ ∧ r t₁ t₂

Builds on

Labelled transition system

Used by

Bisimulation

import Conjectura.Defs.ComputerScience.Semantics.Simulation · maintainer — open · raw source

Adapted for Conjectura from cslib, `Cslib/Foundations/Semantics/Lts/Simulation.lean`, split into one concept per module. Released by its authors under Apache 2.0.

Copyright (c) 2025 Fabrizio Montesi. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Fabrizio Montesi

Full credits