Trace Equivalence #
Definitions and results on trace equivalence for LTS
s.
Main definitions #
LTS.traces
: the set of traces of a state.TraceEq s1 s2
:s1
ands2
are trace equivalent, i.e., they have the same sets of traces.
Notations #
s1 ~tr[lts] s2
: the statess1
ands2
are trace equivalent inlts
.
Main statements #
TraceEq.eqv
: trace equivalence is an equivalence relation (seeEquivalence
).TraceEq.deterministic_sim
: in any deterministicLTS
, trace equivalence is a simulation.
The traces of a state s
is the set of all lists of labels μs
such that there is a multi-step
transition labelled by μs
originating from s
.
Instances For
Notation for trace equivalence.
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.
Instances For
theorem
TraceEq.eqv
{State : Type u}
{Label : Type v}
(lts : LTS State Label)
:
Equivalence (TraceEq lts)
Bisimilarity is an equivalence relation.
theorem
TraceEq.deterministic_sim
{State : Type u}
{Label : Type v}
(lts : LTS State Label)
(hdet : lts.Deterministic)
(s1 s2 : State)
(h : s1 ~tr[lts] s2)
(μ : Label)
(s1' : State)
:
In a deterministic LTS, trace equivalence is a simulation.