7.3. Certified bisimulation🔗

Theorem7.3.1

Statement uses 2

Statement dependency previews

Preview

Definition 7.2.1

Loading preview

Statement dependency preview content is loaded from the rendered-fragment cache.

used by 1✓L∃∀N

A bisimulation certificate holds the tagged state graph of each system, a relation on state indices, and for the weak check an answering path for each move. If the rules on both sides satisfy G1 and the strong, respectively weak, check passes, the initial states s_0, t_0 of the two graphs satisfy

\llbracket s_0 \rrbracket \sim \llbracket t_0 \rrbracket, \qquad\text{respectively}\qquad \llbracket s_0 \rrbracket \approx \llbracket t_0 \rrbracket .

Rests on NEW: BigraphSim.BD.outFace, BigraphSim.Par, RuleG.g1, TRules.

Lean code for Theorem7.3.1●2 theorems

theoremdefined in Logic/CertBisimProof.lean

complete

theorem certBisimSound {Ctrl₁ Ctrl₂ : Type} [DecidableEq Ctrl₁]
  [DecidableEq Ctrl₂] (S₁ : Bigraph.Sig Ctrl₁) (S₂ : Bigraph.Sig Ctrl₂)
  (α : Type) [DecidableEq α] : CertBisimSoundStatement S₁ S₂ α

theorem certBisimSound {Ctrl₁ Ctrl₂ : Type}
  [DecidableEq Ctrl₁] [DecidableEq Ctrl₂]
  (S₁ : Bigraph.Sig Ctrl₁)
  (S₂ : Bigraph.Sig Ctrl₂) (α : Type)
  [DecidableEq α] :
  CertBisimSoundStatement S₁ S₂ α

**CertBisimSound** (PROVED; `CertBisimSoundStatement`): for G1 rules on
both sides, a passing strong certificate makes the two initial agents
strongly bisimilar. The bisimulation relates `a` and `b` when they sit,
up to `≏`, at a related pair of listed states.

theoremdefined in Logic/CertBisimProof.lean

complete

theorem certWeakBisimSound {Ctrl₁ Ctrl₂ : Type} [DecidableEq Ctrl₁]
  [DecidableEq Ctrl₂] (S₁ : Bigraph.Sig Ctrl₁) (S₂ : Bigraph.Sig Ctrl₂)
  (α : Type) [DecidableEq α] : CertWeakBisimSoundStatement S₁ S₂ α

theorem certWeakBisimSound {Ctrl₁ Ctrl₂ : Type}
  [DecidableEq Ctrl₁] [DecidableEq Ctrl₂]
  (S₁ : Bigraph.Sig Ctrl₁)
  (S₂ : Bigraph.Sig Ctrl₂) (α : Type)
  [DecidableEq α] :
  CertWeakBisimSoundStatement S₁ S₂ α

**CertWeakBisimSound** (PROVED; `CertWeakBisimSoundStatement`): for G1
rules on both sides, a passing weak certificate makes the two initial
agents weakly bisimilar. Same relation as `certBisimSound`; each answer
is the certificate's path, read as library moves by `walk_sound`.

Theorem7.3.2

uses 1used by 0✓L∃∀N

The alternating bit protocol with unbounded lossy FIFO channels, each queue a nested chain of message nodes, is weakly bisimilar to a one-place buffer (accept and deliver visible, every other rule silent):

\llbracket \mathrm{Accept}_0 \mid T[\mathrm{nil}] \mid \mathrm{Replier}_1 \mid K[\mathrm{nil}] \rrbracket \;\approx\; \llbracket \mathrm{Buff} \rrbracket .

With channels of capacity one the same holds by certificate alone (112 states): PROVED, kernel-checked in Logic/Examples/ABPCert.lean, a module built on demand.

Rests on UNBRIDGED: ABP.Act, ABP.buff, ABP.buff0, ABPInf.abpInf, ABPInf.encS; NEW: BigraphSim.BD.outFace; not audited: ABP.BCtl, ABP.bsig, ABPInf.Ctl, ABPInf.J0, ABPInf.agentS, ABPInf.sig, ABPInf.st0.

Lean code for Theorem7.3.2●1 theorem

theoremdefined in Logic/Examples/ABPInfSplit.lean

complete

theorem abpInf_wbisim_buff : ABPInf.AbpInfStatement

theorem abpInf_wbisim_buff :
  ABPInf.AbpInfStatement

**(v) PROVED: the ABP with unbounded lossy FIFO channels is weakly bisimilar to the
one-place buffer.**