Bisimulation

TheoremBisimilarity transfers multistep transitions#✓fully proved

Let \(s\) and \(t\) be bisimilar states of a labelled transition system, and suppose \(s\) reaches a state \(s'\) by a multistep transition along a finite (possibly empty) list of labels \(\mu_1, \dots, \mu_n\). Then there is a state \(t'\) such that \(t\) reaches \(t'\) by a multistep transition along the same list of labels, and \(s'\) and \(t'\) are bisimilar.

theorem HomBisimilarity.mtr {left right left' : State} {labels : List Label}
    (hbisim : HomBisimilarity lts left right) (htr : lts.MTr left labels left') :
    ∃ right', lts.MTr right labels right' ∧ HomBisimilarity lts left' right'

Used by 1

Used byWeak bisimilarity transfers weak traces

TheoremBisimilar states enable the same labels#✓fully proved

Let \(s\) and \(t\) be bisimilar states of a labelled transition system. Then for every label \(\mu\), \(s\) has a transition labelled \(\mu\) if and only if \(t\) has a transition labelled \(\mu\).

theorem HomBisimilarity.hasOutLabel_iff {left right : State}
    (hbisim : HomBisimilarity lts left right) (label : Label) :
    lts.HasOutLabel left label ↔ lts.HasOutLabel right label

Used by 2

Used byWeakly bisimilar states enable the same weak labels · Bisimilar states have equal sets of outgoing labels

TheoremBisimilar states have equal sets of outgoing labels#✓fully proved

Let \(s\) and \(t\) be bisimilar states of a labelled transition system. Then the set of labels \(\mu\) for which \(s\) has a transition labelled \(\mu\) equals the set of labels \(\mu\) for which \(t\) has a transition labelled \(\mu\).

theorem HomBisimilarity.outgoingLabels_eq {left right : State}
    (hbisim : HomBisimilarity lts left right) :
    lts.outgoingLabels left = lts.outgoingLabels right

Uses 1 · Used by 1

Proof usesBisimilar states enable the same labels

Used byWeakly bisimilar states have the same set of weak labels

TheoremA silent step lies in the silent closure#✓fully proved

In a labelled transition system with a silent label \(\tau\), write \(\Rightarrow\) for the silent closure, the reflexive-transitive closure of the \(\tau\)-transition relation. If \(s \xrightarrow{\tau} t\) is a transition, then \(s \Rightarrow t\).

theorem τSTr.of_tr {source target : State}
    (hstep : lts.Tr source HasTau.τ target) : lts.τSTr source target

Used by 3

Used byLossy acknowledgements break the buffer specification · Certificate checks give weak bisimilarity · Rooted weak transitions are weak transitions

TheoremPrepending a silent step to the silent closure#✓fully proved

In a labelled transition system with a silent label \(\tau\), write \(\Rightarrow\) for the silent closure, the reflexive-transitive closure of the \(\tau\)-transition relation. If \(s \xrightarrow{\tau} m\) is a transition and \(m \Rightarrow t\), then \(s \Rightarrow t\).

theorem τSTr.cons {source middle target : State}
    (hstep : lts.Tr source HasTau.τ middle) (htail : lts.τSTr middle target) :
    lts.τSTr source target

Used by 2

Used byLossy acknowledgements break the buffer specification · The silent closure is made of runs of silent steps

TheoremThe silent closure is made of runs of silent steps#✓fully proved

In a labelled transition system with a silent label \(\tau\), write \(\Rightarrow\) for the silent closure, the reflexive-transitive closure of the \(\tau\)-transition relation. Then \(s \Rightarrow t\) if and only if, for some \(n \in \mathbb{N}\), there is a multistep transition from \(s\) to \(t\) whose list of labels consists of \(n\) copies of \(\tau\).

theorem τSTr_iff_exists_mtr {source target : State} :
    lts.τSTr source target ↔
      ∃ count, lts.MTr source (List.replicate count HasTau.τ) target

Uses 1

Proof usesPrepending a silent step to the silent closure

TheoremWeak transitions with a visible label#✓fully proved

In a labelled transition system with a silent label \(\tau\), write \(\Rightarrow\) for the reflexive-transitive closure of the \(\tau\)-transition relation. A weak transition \(s \stackrel{\mu}{\Longrightarrow} t\) is either the trivial one \(s \stackrel{\tau}{\Longrightarrow} s\) or a composite \(s \Rightarrow s_1 \xrightarrow{\mu} s_2 \Rightarrow t\). For a label \(\mu \ne \tau\), \(s \stackrel{\mu}{\Longrightarrow} t\) holds if and only if there are states \(s_1, s_2\) with \(s \Rightarrow s_1\), \(s_1 \xrightarrow{\mu} s_2\) and \(s_2 \Rightarrow t\).

theorem STr.iff_exists_of_ne {source target : State} {label : Label}
    (hne : label ≠ HasTau.τ) :
    lts.STr source label target ↔
      ∃ before after, lts.τSTr source before ∧
        lts.Tr before label after ∧ lts.τSTr after target

Used by 4

Used byVisible weak steps of the buffer · Lossy acknowledgements break the buffer specification · The stuck lossy go-back-N configuration refuses new messages · A rooted silent step followed by a weak transition is rooted

TheoremSilent steps before a weak transition#✓fully proved

Let \(L\) be a labelled transition system with a silent label \(\tau\). A weak \(\tau\)-transition is a sequence of zero or more \(\tau\)-steps, and for \(\mu \ne \tau\) a weak \(\mu\)-transition is zero or more \(\tau\)-steps, one \(\mu\)-step and zero or more \(\tau\)-steps. If a state \(s\) reaches a state \(m\) by zero or more \(\tau\)-steps and there is a weak \(\mu\)-transition from \(m\) to \(t\), then there is a weak \(\mu\)-transition from \(s\) to \(t\).

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

Used by 1

Used byCertificate checks give weak bisimilarity

TheoremSilent steps after a weak transition#✓fully proved

Let \(L\) be a labelled transition system with a silent label \(\tau\). A weak \(\tau\)-transition is a sequence of zero or more \(\tau\)-steps, and for \(\mu \ne \tau\) a weak \(\mu\)-transition is zero or more \(\tau\)-steps, one \(\mu\)-step and zero or more \(\tau\)-steps. If there is a weak \(\mu\)-transition from a state \(s\) to a state \(m\) and \(m\) reaches a state \(t\) by zero or more \(\tau\)-steps, then there is a weak \(\mu\)-transition from \(s\) to \(t\).

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

TheoremStrong traces are weak traces#✓fully proved

Let \(L\) be a labelled transition system with a silent label \(\tau\). A weak \(\tau\)-transition is a sequence of zero or more \(\tau\)-steps, and for \(\mu \ne \tau\) a weak \(\mu\)-transition is zero or more \(\tau\)-steps, one \(\mu\)-step and zero or more \(\tau\)-steps; the saturation of \(L\) is the system on the same states whose \(\mu\)-transitions are the weak \(\mu\)-transitions of \(L\). If \(L\) moves from a state \(s\) to a state \(t\) by a sequence of transitions labelled \(\mu_1, \dots, \mu_n\), then the saturation of \(L\) moves from \(s\) to \(t\) by a sequence of transitions with the same labels \(\mu_1, \dots, \mu_n\).

theorem MTr.to_saturate {source target : State} {labels : List Label}
    (htrace : lts.MTr source labels target) :
    lts.saturate.MTr source labels target

TheoremWeak bisimilarity is bisimilarity of the saturated system#✓fully proved

In a labelled transition system with a silent label \(\tau\), write \(\Rightarrow\) for the reflexive-transitive closure of the \(\tau\)-transition relation. The weak transitions \(s \stackrel{\mu}{\Longrightarrow} t\) are the trivial ones \(s \stackrel{\tau}{\Longrightarrow} s\) and the composites \(s \Rightarrow s_1 \xrightarrow{\mu} s_2 \Rightarrow t\); the saturated system has the same states and has the weak transitions as its transitions. Two states are weakly bisimilar if some bisimulation of the saturated system relates them. Thus two states are weakly bisimilar if and only if they are bisimilar in the saturated system; this holds by definition.

theorem HomWeakBisimilarity.iff_homBisimilarity_saturate {left right : State} :
    HomWeakBisimilarity lts left right ↔ HomBisimilarity lts.saturate left right

TheoremWeak bisimilarity answers a strong step with a weak step#✓fully proved

Let \(L\) be a labelled transition system with a silent label \(\tau\). A weak \(\tau\)-transition is a sequence of zero or more \(\tau\)-steps, and for \(\mu \ne \tau\) a weak \(\mu\)-transition is zero or more \(\tau\)-steps, one \(\mu\)-step and zero or more \(\tau\)-steps. Two states are weakly bisimilar when some bisimulation of the system whose \(\mu\)-transitions are the weak \(\mu\)-transitions of \(L\) relates them. If \(p\) and \(q\) are weakly bisimilar and \(L\) has a transition from \(p\) to \(p'\) labelled \(\mu\), then there is a state \(q'\) with a weak \(\mu\)-transition from \(q\) to \(q'\) such that \(p'\) and \(q'\) are weakly bisimilar.

theorem HomWeakBisimilarity.tr {left right left' : State} {label : Label}
    (hbisim : HomWeakBisimilarity lts left right) (hstep : lts.Tr left label left') :
    ∃ right', lts.STr right label right' ∧ HomWeakBisimilarity lts left' right'

Used by 1

Used byObservation congruence implies weak bisimilarity

TheoremWeak bisimilarity transfers weak transitions#✓fully proved

In a labelled transition system with a silent label \(\tau\), write \(\Rightarrow\) for the reflexive-transitive closure of the \(\tau\)-transition relation. The weak transitions \(s \stackrel{\mu}{\Longrightarrow} t\) are the trivial ones \(s \stackrel{\tau}{\Longrightarrow} s\) and the composites \(s \Rightarrow s_1 \xrightarrow{\mu} s_2 \Rightarrow t\); the saturated system has the same states and has the weak transitions as its transitions. Two states are weakly bisimilar if some bisimulation of the saturated system relates them. If \(s\) and \(t\) are weakly bisimilar and \(s \stackrel{\mu}{\Longrightarrow} s'\), then there is a state \(t'\) with \(t \stackrel{\mu}{\Longrightarrow} t'\) such that \(s'\) and \(t'\) are weakly bisimilar.

theorem HomWeakBisimilarity.sTr {left right left' : State} {label : Label}
    (hbisim : HomWeakBisimilarity lts left right)
    (hstep : lts.STr left label left') :
    ∃ right', lts.STr right label right' ∧ HomWeakBisimilarity lts left' right'

Used by 2

Used byLossy acknowledgements break the buffer specification · Observation congruence matches rooted weak transitions

TheoremWeak bisimilarity transfers weak traces#✓fully proved

In a labelled transition system with a silent label \(\tau\), write \(\Rightarrow\) for the reflexive-transitive closure of the \(\tau\)-transition relation. The weak transitions \(s \stackrel{\mu}{\Longrightarrow} t\) are the trivial ones \(s \stackrel{\tau}{\Longrightarrow} s\) and the composites \(s \Rightarrow s_1 \xrightarrow{\mu} s_2 \Rightarrow t\); the saturated system has the same states and has the weak transitions as its transitions. Two states are weakly bisimilar if some bisimulation of the saturated system relates them. Suppose \(s\) and \(t\) are weakly bisimilar and \(s\) reaches \(s'\) by a multistep transition of the saturated system with label list \(\mu_1, \dots, \mu_n\), that is, by weak transitions \(s \stackrel{\mu_1}{\Longrightarrow} \cdots \stackrel{\mu_n}{\Longrightarrow} s'\). Then \(t\) reaches some \(t'\) by a multistep transition of the saturated system with the same label list, and \(s'\) and \(t'\) are weakly bisimilar.

theorem HomWeakBisimilarity.saturate_mtr {left right left' : State}
    {labels : List Label}
    (hbisim : HomWeakBisimilarity lts left right)
    (htrace : lts.saturate.MTr left labels left') :
    ∃ right', lts.saturate.MTr right labels right' ∧
      HomWeakBisimilarity lts left' right'

Uses 1

Proof usesBisimilarity transfers multistep transitions

TheoremStrong bisimilarity implies weak bisimilarity#✓fully proved

In a labelled transition system with a silent label \(\tau\), write \(\Rightarrow\) for the reflexive-transitive closure of the \(\tau\)-transition relation. The weak transitions \(s \stackrel{\mu}{\Longrightarrow} t\) are the trivial ones \(s \stackrel{\tau}{\Longrightarrow} s\) and the composites \(s \Rightarrow s_1 \xrightarrow{\mu} s_2 \Rightarrow t\); the saturated system has the same states and has the weak transitions as its transitions. Two states are weakly bisimilar if some bisimulation of the saturated system relates them. If two states are bisimilar in the original system, then they are weakly bisimilar.

theorem HomBisimilarity.to_homWeakBisimilarity {left right : State}
    (h : HomBisimilarity lts left right) : HomWeakBisimilarity lts left right

Used by 1

Used byStrong bisimilarity implies observation congruence

TheoremWeakly bisimilar states enable the same weak labels#✓fully proved

In a labelled transition system with a silent label \(\tau\), write \(\Rightarrow\) for the reflexive-transitive closure of the \(\tau\)-transition relation. The weak transitions \(s \stackrel{\mu}{\Longrightarrow} t\) are the trivial ones \(s \stackrel{\tau}{\Longrightarrow} s\) and the composites \(s \Rightarrow s_1 \xrightarrow{\mu} s_2 \Rightarrow t\); the saturated system has the same states and has the weak transitions as its transitions. Two states are weakly bisimilar if some bisimulation of the saturated system relates them. If \(s\) and \(t\) are weakly bisimilar, then for every label \(\mu\), there is a weak transition \(s \stackrel{\mu}{\Longrightarrow} s'\) for some \(s'\) if and only if there is a weak transition \(t \stackrel{\mu}{\Longrightarrow} t'\) for some \(t'\).

theorem HomWeakBisimilarity.hasOutLabel_saturate_iff {left right : State}
    (hbisim : HomWeakBisimilarity lts left right) (label : Label) :
    lts.saturate.HasOutLabel left label ↔ lts.saturate.HasOutLabel right label

Uses 1 · Used by 1

Proof usesBisimilar states enable the same labels

Used byLossy acknowledgements break the buffer specification

TheoremWeakly bisimilar states have the same set of weak labels#✓fully proved

In a labelled transition system with a silent label \(\tau\), write \(\Rightarrow\) for the reflexive-transitive closure of the \(\tau\)-transition relation. The weak transitions \(s \stackrel{\mu}{\Longrightarrow} t\) are the trivial ones \(s \stackrel{\tau}{\Longrightarrow} s\) and the composites \(s \Rightarrow s_1 \xrightarrow{\mu} s_2 \Rightarrow t\); the saturated system has the same states and has the weak transitions as its transitions. Two states are weakly bisimilar if some bisimulation of the saturated system relates them. If \(s\) and \(t\) are weakly bisimilar, then the set of labels \(\mu\) with \(s \stackrel{\mu}{\Longrightarrow} s'\) for some \(s'\) equals the set of labels \(\mu\) with \(t \stackrel{\mu}{\Longrightarrow} t'\) for some \(t'\).

theorem HomWeakBisimilarity.outgoingLabels_saturate_eq {left right : State}
    (hbisim : HomWeakBisimilarity lts left right) :
    lts.saturate.outgoingLabels left = lts.saturate.outgoingLabels right

Uses 1

Proof usesBisimilar states have equal sets of outgoing labels

17 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.