Deterministic system
Deterministicdef
An LTS is deterministic when each state has at most one successor per label, so the label alone determines what happens next.
def LTS.Deterministic {State Label : Type*} (lts : LTS State Label) : Prop :=
∀ s μ s₁ s₂, lts.Tr s μ s₁ → lts.Tr s μ s₂ → s₁ = s₂Builds on
import Conjectura.Defs.ComputerScience.Semantics.Deterministic · maintainer — open · raw source
Adapted for Conjectura from cslib, 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