Observational congruence

DefinitionRooted weak transition#✓fully proved

In a labelled transition system whose labels include a silent label \(\tau\), there is a rooted weak transition from \(s\) to \(t\) with label \(\mu\) when there are states \(s_1\) and \(s_2\) such that \(s\) reaches \(s_1\) by zero or more \(\tau\)-transitions, \(s_1 \xrightarrow{\mu} s_2\) is a transition, and \(s_2\) reaches \(t\) by zero or more \(\tau\)-transitions. In particular, a rooted weak transition with label \(\tau\) contains at least one actual \(\tau\)-transition.

def RootedWeakStep (source : State) (label : Label) (target : State) : Prop :=
  ∃ before after,
    lts.τSTr source before ∧
    lts.Tr before label after ∧
    lts.τSTr after target

Used by 12

Used byCertificate checks give rooted observation congruence · Observation congruence matches rooted weak transitions · Observation congruence is an equivalence relation · Strong bisimilarity implies observation congruence · Transitions are rooted weak transitions · Silent steps before a rooted weak transition · Rooted observation congruence · Observation congruence implies weak bisimilarity · Rooted weak transitions are weak transitions · Transitivity of rooted observational congruence · A rooted silent step followed by a weak transition is rooted · Appending silent steps to a rooted weak transition

TheoremTransitions are rooted weak transitions#✓fully proved

In a labelled transition system with a silent label \(\tau\), every transition \(s \xrightarrow{\mu} t\) is a rooted weak transition from \(s\) to \(t\) with label \(\mu\).

theorem rootedWeakStep_of_tr {source target : State} {label : Label}
    (hstep : lts.Tr source label target) :
    lts.RootedWeakStep source label target

Uses 1 · Used by 3

Statement usesRooted weak transition

Used byCertificate checks give rooted observation congruence · Observation congruence is an equivalence relation · Strong bisimilarity implies observation congruence

TheoremRooted weak transitions are weak transitions#✓fully proved

In a labelled transition system with a silent label \(\tau\), every rooted weak transition from \(s\) to \(t\) with label \(\mu\) is a weak transition from \(s\) to \(t\) with label \(\mu\), where a weak transition with label \(\mu\) is either the trivial step from a state to itself with label \(\tau\), or a transition with label \(\mu\) preceded and followed by zero or more \(\tau\)-transitions.

theorem RootedWeakStep.toSTr {source target : State} {label : Label}
    (hstep : lts.RootedWeakStep source label target) :
    lts.STr source label target

Uses 2 · Used by 3

Statement usesRooted weak transition

Proof usesA silent step lies in the silent closure

Used byObservation congruence matches rooted weak transitions · Observation congruence implies weak bisimilarity · A rooted silent step followed by a weak transition is rooted

TheoremSilent steps before a rooted weak transition#✓fully proved

In a labelled transition system with a silent label \(\tau\), if \(s\) reaches \(m\) by zero or more \(\tau\)-transitions and there is a rooted weak transition from \(m\) to \(t\) with label \(\mu\), then there is a rooted weak transition from \(s\) to \(t\) with label \(\mu\).

theorem τSTr.rootedWeakStep_trans {source middle target : State}
    {label : Label}
    (hbefore : lts.τSTr source middle)
    (hstep : lts.RootedWeakStep middle label target) :
    lts.RootedWeakStep source label target

Uses 1 · Used by 1

Statement usesRooted weak transition

Used byObservation congruence matches rooted weak transitions

TheoremAppending silent steps to a rooted weak transition#✓fully proved

In a labelled transition system with silent action \(\tau\), if there is a rooted weak transition from \(s\) to \(m\) with label \(a\), and \(t\) is reachable from \(m\) by zero or more \(\tau\)-transitions, then there is a rooted weak transition from \(s\) to \(t\) with label \(a\).

theorem RootedWeakStep.trans_τSTr {source middle target : State}
    {label : Label}
    (hstep : lts.RootedWeakStep source label middle)
    (hafter : lts.τSTr middle target) :
    lts.RootedWeakStep source label target

Uses 1 · Used by 2

Statement usesRooted weak transition

Used byObservation congruence matches rooted weak transitions · A rooted silent step followed by a weak transition is rooted

TheoremA rooted silent step followed by a weak transition is rooted#✓fully proved

In a labelled transition system with a silent label \(\tau\), if there is a rooted weak transition from \(s\) to \(m\) with label \(\tau\) and a weak transition from \(m\) to \(t\) with label \(\mu\), then there is a rooted weak transition from \(s\) to \(t\) with label \(\mu\). Here a weak transition with label \(\mu\) is either the trivial step from a state to itself with label \(\tau\), or a transition with label \(\mu\) preceded and followed by zero or more \(\tau\)-transitions.

The initial rooted transition supplies the required actual silent step even when the following weak transition is reflexive.

theorem RootedWeakStep.trans_sTr {source middle target : State}
    {label : Label}
    (hrooted : lts.RootedWeakStep source HasTau.τ middle)
    (hweak : lts.STr middle label target) :
    lts.RootedWeakStep source label target

Uses 4 · Used by 1

Statement usesRooted weak transition

Proof usesRooted weak transitions are weak transitions · Appending silent steps to a rooted weak transition · Weak transitions with a visible label

Used byObservation congruence matches rooted weak transitions

DefinitionRooted observation congruence#✓fully proved

In a labelled transition system with a silent label \(\tau\), states \(p\) and \(q\) are rooted weakly bisimilar (observation congruent) when every transition \(p \xrightarrow{\mu} p'\) is matched by a rooted weak transition from \(q\) to some \(q'\) with label \(\mu\) such that \(p'\) and \(q'\) are weakly bisimilar, and every transition \(q \xrightarrow{\mu} q'\) is matched by a rooted weak transition from \(p\) to some \(p'\) with label \(\mu\) such that \(p'\) and \(q'\) are weakly bisimilar.

def RootedWeaklyBisimilar (left right : State) : Prop :=
  (∀ ⦃label left'⦄, lts.Tr left label left' →
    ∃ right', lts.RootedWeakStep right label right' ∧
      HomWeakBisimilarity lts left' right') ∧
  (∀ ⦃label right'⦄, lts.Tr right label right' →
    ∃ left', lts.RootedWeakStep left label left' ∧
      HomWeakBisimilarity lts left' right')

Uses 1 · Used by 9

Statement usesRooted weak transition

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol is observation congruent to a one-place buffer · Go-back-N with window 2 is observation congruent to a two-place buffer · Certificate checks give rooted observation congruence · Observation congruence matches rooted weak transitions · Observation congruence is an equivalence relation · Strong bisimilarity implies observation congruence · Observation congruence implies weak bisimilarity · Transitivity of rooted observational congruence

TheoremObservation congruence matches rooted weak transitions#✓fully proved

In a labelled transition system with a silent label \(\tau\), if \(p\) and \(q\) are rooted weakly bisimilar and there is a rooted weak transition from \(p\) to \(p'\) with label \(\mu\), then there is a state \(q'\) with a rooted weak transition from \(q\) to \(q'\) with label \(\mu\) such that \(p'\) and \(q'\) are weakly bisimilar.

theorem RootedWeaklyBisimilar.match_rootedLeft {left right left' : State}
    {label : Label} (hcongr : lts.RootedWeaklyBisimilar left right)
    (hstep : lts.RootedWeakStep left label left') :
    ∃ right', lts.RootedWeakStep right label right' ∧
      HomWeakBisimilarity lts left' right'

Uses 7 · Used by 1

Statement usesRooted weak transition · Rooted observation congruence

Proof usesWeak bisimilarity transfers weak transitions · Rooted weak transitions are weak transitions · A rooted silent step followed by a weak transition is rooted · Appending silent steps to a rooted weak transition · Silent steps before a rooted weak transition

Used byTransitivity of rooted observational congruence

TheoremTransitivity of rooted observational congruence#✓fully proved

In a labelled transition system with silent action \(\tau\), if \(p\) is rooted observationally congruent to \(q\) and \(q\) is rooted observationally congruent to \(r\), then \(p\) is rooted observationally congruent to \(r\).

@[trans]
theorem RootedWeaklyBisimilar.trans {left middle right : State}
    (hleft : lts.RootedWeaklyBisimilar left middle)
    (hright : lts.RootedWeaklyBisimilar middle right) :
    lts.RootedWeaklyBisimilar left right

Uses 3 · Used by 1

Statement usesRooted observation congruence

Proof usesRooted weak transition · Observation congruence matches rooted weak transitions

Used byObservation congruence is an equivalence relation

TheoremObservation congruence is an equivalence relation#✓fully proved

In every labelled transition system with a silent label \(\tau\), rooted weak bisimilarity (observation congruence) is reflexive, symmetric and transitive.

theorem observationCongruent_equivalence :
    Equivalence (lts.RootedWeaklyBisimilar)

Uses 4

Statement usesRooted observation congruence

Proof usesRooted weak transition · Transitivity of rooted observational congruence · Transitions are rooted weak transitions

TheoremStrong bisimilarity implies observation congruence#✓fully proved

In a labelled transition system with a silent label \(\tau\), any two strongly bisimilar states are rooted weakly bisimilar.

theorem observationCongruent_of_bisimilar {left right : State}
    (hbisim : HomBisimilarity lts left right) :
    lts.RootedWeaklyBisimilar left right

Uses 4

Statement usesRooted observation congruence

Proof usesStrong bisimilarity implies weak bisimilarity · Rooted weak transition · Transitions are rooted weak transitions

TheoremObservation congruence implies weak bisimilarity#✓fully proved

In a labelled transition system with a silent label \(\tau\), any two rooted weakly bisimilar states are weakly bisimilar.

theorem RootedWeaklyBisimilar.to_homWeakBisimilarity {left right : State}
    (hcongr : lts.RootedWeaklyBisimilar left right) :
    HomWeakBisimilarity lts left right

Uses 4

Statement usesRooted observation congruence

Proof usesWeak bisimilarity answers a strong step with a weak step · Rooted weak transition · Rooted weak transitions are weak transitions

12 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.