Reachability

Reachabledef

A state is reachable from another when some finite sequence of labelled transitions leads from the first to the second, whatever labels are used along the way.

def LTS.Reachable {State Label : Type*} (lts : LTS State Label) (s t : State) : Prop :=
  Relation.ReflTransGen (fun a b => ∃ μ : Label, lts.Tr a μ b) s t

Builds on

Labelled transition system

From Mathlib

Logic.Relation

import Conjectura.Defs.ComputerScience.Semantics.Reachable · 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

Full credits