Finite-state CCS agents

DefinitionSum of prefixes#✓fully proved

For a list \(l\) of pairs \((a, q)\) of a label and a process, the process that chooses among the prefixes \(a.q\) listed in \(l\): the empty list gives the inactive process \(\mathbf{0}\), and the list with head \((a, q)\) and tail \(r\) gives the choice \(a.q + P\) between the prefix \(a.q\) and the process \(P\) built in the same way from \(r\).

def sumOf : List (Label Name × Process Name Constant) → Process Name Constant
  | [] => .nil
  | (a, q) :: rest => .choice (.prefix a q) (sumOf rest)

Uses 2 · Used by 5

Statement usesCCS labels · Recursive CCS processes

Used byRecursive specification of the data-free alternating-bit protocol · Recursive specification of the alternating-bit protocol with data · Recursive CCS specification of go-back-N · Constants listing their transitions realize them · Transitions of a sum of prefixes

TheoremTransitions of a sum of prefixes#✓fully proved

For every recursive specification, every list \(l\) of pairs of a label and a process, every label \(a\) and every process \(q\), the sum of the prefixes listed in \(l\) has a transition labelled \(a\) to \(q\) exactly when \((a, q)\) belongs to \(l\).

theorem step_sumOf_iff {spec : Specification Name Constant}
    (l : List (Label Name × Process Name Constant)) (a : Label Name)
    (q : Process Name Constant) :
    Process.Step spec (sumOf l) a q ↔ (a, q) ∈ l

Uses 9 · Used by 1

Statement usesSum of prefixes · CCS labels · Recursive CCS processes · Transitions of recursive CCS · Recursive CCS specification

Proof usesComplementary labels · Relabelling · Actions permitted by a restriction · Relabelling an action

Used byConstants listing their transitions realize them

DefinitionRealization of a code-level transition system#✓fully proved

Fix a recursive specification. A family of processes \(P_x\) indexed by codes \(x\) realizes a function \(s\) that lists, for each code \(x\), labelled transitions \((a, y)\) with \(a\) a label and \(y\) a code, when for every code \(x\), every label \(a\) and every process \(q\), the process \(P_x\) has a transition with label \(a\) to \(q\) exactly when \(s(x)\) contains an entry \((a, y)\) with \(P_y = q\).

def Realizes (spec : Specification Name Constant) {α : Type*}
    (realize : α → Process Name Constant) (steps : α → List (Label Name × α)) : Prop :=
  ∀ x a q, Process.Step spec (realize x) a q ↔ ∃ y, (a, y) ∈ steps x ∧ realize y = q

Uses 4 · Used by 16

Statement usesCCS labels · Recursive CCS processes · Transitions of recursive CCS · Recursive CCS specification

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · The alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · The silent closure of the buffer is trivial · Visible weak steps of the buffer · Go-back-N with window 2 is observation congruent to a two-place buffer · Go-back-N with window 2 implements a two-place buffer · Lossy acknowledgements break the buffer specification · Configuration transitions are process transitions in lossy go-back-N · The stuck lossy go-back-N configuration refuses new messages · Constants listing their transitions realize them · Parallel composition preserves realization · Restriction preserves realization · Certificate checks give rooted observation congruence · Certificate checks give weak bisimilarity

TheoremConstants listing their transitions realize them#✓fully proved

Fix a recursive specification, a map \(\iota\) from codes to process constants and a function \(s\) listing labelled transitions for each code. Suppose that for every code \(x\), writing \((a_1, y_1), \dots, (a_n, y_n)\) for the entries of \(s(x)\) in order, the body of the constant \(\iota(x)\) is \(a_1.\iota(y_1) + (a_2.\iota(y_2) + \dots + (a_n.\iota(y_n) + 0))\), which is \(0\) when \(n = 0\). Then the processes \(\iota(x)\), indexed by codes \(x\), realize \(s\).

theorem Realizes.constant {α : Type*} (inj : α → Constant)
    (steps : α → List (Label Name × α))
    (hspec : ∀ x, spec (inj x) =
      sumOf ((steps x).map fun y => (y.1, Process.constant (inj y.2)))) :
    Realizes spec (fun x => Process.constant (inj x)) steps

Uses 11 · Used by 11

Statement usesRealization of a code-level transition system · Sum of prefixes · CCS labels · Recursive CCS processes · Recursive CCS specification

Proof usesTransitions of a sum of prefixes · Complementary labels · Transitions of recursive CCS · Relabelling · Actions permitted by a restriction · Relabelling an action

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · The alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · The silent closure of the buffer is trivial · Visible weak steps of the buffer · Go-back-N with window 2 is observation congruent to a two-place buffer · Go-back-N with window 2 implements a two-place buffer · Lossy acknowledgements break the buffer specification · Configuration transitions are process transitions in lossy go-back-N · The stuck lossy go-back-N configuration refuses new messages

DefinitionCode-level parallel composition#✓fully proved

Given functions \(s\) and \(t\) listing the labelled transitions of codes \(x\) and \(y\), the transitions of the pair \((x, y)\) are listed in three blocks: \((a, (x', y))\) for each entry \((a, x')\) of \(s(x)\); then \((a, (x, y'))\) for each entry \((a, y')\) of \(t(y)\); then \((\tau, (x', y'))\) for each entry \((a, x')\) of \(s(x)\) and each entry \((b, y')\) of \(t(y)\) whose labels are complementary, that is, one is the input and the other the output on the same name.

def parSteps {α β : Type*} (s : α → List (Label Name × α)) (t : β → List (Label Name × β))
    (z : α × β) : List (Label Name × (α × β)) :=
  (s z.1).map (fun y => (y.1, (y.2, z.2))) ++ (t z.2).map (fun w => (w.1, (z.1, w.2))) ++
    (s z.1).flatMap fun y =>
      (t z.2).filterMap fun w => (Label.synchronize y.1 w.1).map fun c => (c, (y.2, w.2))

Uses 2 · Used by 13

Statement usesCCS labels · Synchronization of CCS labels

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · The alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · Alternating-bit configuration transitions · Transitions of the alternating-bit protocol with data · Transitions of go-back-N configurations · Go-back-N with window 2 is observation congruent to a two-place buffer · Go-back-N with window 2 implements a two-place buffer · Transitions of lossy go-back-N configurations · Configuration transitions are process transitions in lossy go-back-N · The stuck lossy go-back-N configuration refuses new messages · Parallel composition preserves realization

TheoremParallel composition preserves realization#✓fully proved

Fix a recursive specification. If the processes \(P_x\) realize \(s\) and the processes \(Q_y\) realize \(t\), then the parallel compositions \(P_x \mid Q_y\), indexed by pairs \((x, y)\), realize the code-level parallel composition of \(s\) and \(t\).

theorem Realizes.parallel {α β : Type*} {f : α → Process Name Constant}
    {g : β → Process Name Constant} {s : α → List (Label Name × α)}
    {t : β → List (Label Name × β)} (hf : Realizes spec f s) (hg : Realizes spec g t) :
    Realizes spec (fun z => .parallel (f z.1) (g z.2)) (parSteps s t)

Uses 11 · Used by 8

Statement usesRealization of a code-level transition system · Code-level parallel composition · CCS labels · Recursive CCS processes · Recursive CCS specification

Proof usesComplementary labels · Synchronization of CCS labels · Transitions of recursive CCS · Relabelling · Actions permitted by a restriction · Relabelling an action

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · The alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · Go-back-N with window 2 is observation congruent to a two-place buffer · Go-back-N with window 2 implements a two-place buffer · Configuration transitions are process transitions in lossy go-back-N · The stuck lossy go-back-N configuration refuses new messages

DefinitionBoolean restriction test#✓fully proved

For a list \(L\) of blocked names, the test returns true on a label exactly when the label is the silent action \(\tau\), or an input or an output on a name that does not occur in \(L\). It is the Boolean form of the condition that restriction by \(L\) allows the label.

def allowedB (blocked : List Name) : Label Name → Bool
  | .tau => true
  | .input n => !blocked.contains n
  | .output n => !blocked.contains n

Uses 1 · Used by 2

Statement usesCCS labels

Used byCode-level restriction · Restriction preserves realization

DefinitionCode-level restriction#✓fully proved

For a list \(L\) of blocked names and a function \(s\) listing the labelled transitions of each code, the restricted transitions of a code \(x\) are the entries \((a, y)\) of \(s(x)\), in order, whose label \(a\) is the silent action \(\tau\) or an input or an output on a name that does not occur in \(L\).

def restrictSteps {α : Type*} (blocked : List Name) (s : α → List (Label Name × α)) (x : α) :
    List (Label Name × α) :=
  (s x).filter fun y => allowedB blocked y.1

Uses 2 · Used by 5

Statement usesBoolean restriction test · CCS labels

Used byAlternating-bit configuration transitions · Transitions of the alternating-bit protocol with data · Transitions of go-back-N configurations · Transitions of lossy go-back-N configurations · Restriction preserves realization

TheoremRestriction preserves realization#✓fully proved

Fix a recursive specification and a list \(L\) of blocked names. If the processes \(P_x\) realize \(s\), then the restricted processes \(P_x \setminus L\) realize the code-level restriction of \(s\) by \(L\).

theorem Realizes.restriction {α : Type*} {f : α → Process Name Constant}
    {s : α → List (Label Name × α)} (blocked : List Name) (hf : Realizes spec f s) :
    Realizes spec (fun x => .restriction blocked (f x)) (restrictSteps blocked s)

Uses 11 · Used by 8

Statement usesRealization of a code-level transition system · Code-level restriction · CCS labels · Recursive CCS processes · Recursive CCS specification

Proof usesBoolean restriction test · Complementary labels · Transitions of recursive CCS · Relabelling · Actions permitted by a restriction · Relabelling an action

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · The alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · Go-back-N with window 2 is observation congruent to a two-place buffer · Go-back-N with window 2 implements a two-place buffer · Configuration transitions are process transitions in lossy go-back-N · The stuck lossy go-back-N configuration refuses new messages

DefinitionForward certificate check#✓fully proved

Let \(s\) list the labelled transitions \((a, x')\) of each implementation code \(x\), let \(t\) list those of each specification code \(y\), and let \(R\) be a finite list of code pairs. The forward check succeeds when for every pair \((x, y)\) in \(R\) and every entry \((a, x')\) of \(s(x)\), either \(a = \tau\) and \((x', y)\) is in \(R\), or some entry \((a, y')\) of \(t(y)\) with the same label has \((x', y')\) in \(R\).

def forwardCheck (s : α → List (Label Name × α)) (t : β → List (Label Name × β))
    (rel : List (α × β)) : Bool :=
  rel.all fun p => (s p.1).all fun step =>
    (step.1 == .tau && rel.contains (step.2, p.2)) ||
      (t p.2).any fun spec => spec.1 == step.1 && rel.contains (step.2, spec.2)

Uses 1 · Used by 2

Statement usesCCS labels

Used byWeak-bisimulation certificate check · Certificate checks give weak bisimilarity

DefinitionBackward certificate check#✓fully proved

Let \(s\) list the labelled transitions \((a, x')\) of each implementation code \(x\), let \(t\) list those of each specification code \(y\), and let \(R\) be a finite list of code pairs. The backward check succeeds when for every pair \((x, y)\) in \(R\) and every entry \((a, y')\) of \(t(y)\), at least one of the following holds: \(a = \tau\) and \((x, y')\) is in \(R\); some entry \((a, x')\) of \(s(x)\) with the same label has \((x', y')\) in \(R\); or some entry \((\tau, x'')\) of \(s(x)\) has \((x'', y)\) in \(R\), and the first occurrence of \((x'', y)\) in \(R\) comes strictly before the first occurrence of \((x, y)\).

def backwardCheck (s : α → List (Label Name × α)) (t : β → List (Label Name × β))
    (rel : List (α × β)) : Bool :=
  rel.all fun p => (t p.2).all fun spec =>
    (spec.1 == .tau && rel.contains (p.1, spec.2)) ||
      ((s p.1).any fun step => step.1 == spec.1 && rel.contains (step.2, spec.2)) ||
      (s p.1).any fun step =>
        step.1 == .tau && rel.contains (step.2, p.2) && rel.idxOf (step.2, p.2) < rel.idxOf p

Uses 1 · Used by 2

Statement usesCCS labels

Used byWeak-bisimulation certificate check · Certificate checks give weak bisimilarity

DefinitionWeak-bisimulation certificate check#✓fully proved

For transition lists \(s\) of implementation codes and \(t\) of specification codes and a finite list \(R\) of code pairs, the certificate check succeeds when both the forward check and the backward check succeed on \(s\), \(t\) and \(R\).

def certCheck (s : α → List (Label Name × α)) (t : β → List (Label Name × β))
    (rel : List (α × β)) : Bool :=
  forwardCheck s t rel && backwardCheck s t rel

Uses 3 · Used by 8

Statement usesBackward certificate check · Forward certificate check · CCS labels

Used byThe alternating-bit protocol with data is observation congruent to the buffer · The alternating-bit protocol transmits data correctly · The alternating-bit protocol is observation congruent to a one-place buffer · The alternating-bit protocol implements a one-place buffer · Go-back-N with window 2 is observation congruent to a two-place buffer · Go-back-N with window 2 implements a two-place buffer · Certificate checks give rooted observation congruence · Certificate checks give weak bisimilarity

TheoremCertificate checks give weak bisimilarity#✓fully proved

Let \(f\) realize the code-level transition function \(s\) and \(g\) realize \(t\) for a recursive specification, and let \(R\) be a list of code pairs on which the certificate check of \(s\), \(t\) and \(R\) succeeds. Then for every pair \((x, y)\) in \(R\), the processes \(f(x)\) and \(g(y)\) are weakly bisimilar in the labelled transition system of the specification.

theorem weaklyBisimilar_of_certCheck (hf : Realizes spec f s) (hg : Realizes spec g t)
    (hcheck : certCheck s t rel = true) {x : α} {y : β} (hxy : (x, y) ∈ rel) :
    (Process.lts spec).HomWeakBisimilarity (f x) (g y)

Uses 11 · Used by 4

Statement usesRealization of a code-level transition system · Weak-bisimulation certificate check · CCS labels · Recursive CCS processes · Labelled transition system of a recursive specification · Recursive CCS specification

Proof usesBackward certificate check · Forward certificate check · Transitions of recursive CCS · A silent step lies in the silent closure · Silent steps before a weak transition

Used byThe alternating-bit protocol transmits data correctly · The alternating-bit protocol implements a one-place buffer · Go-back-N with window 2 implements a two-place buffer · Certificate checks give rooted observation congruence

DefinitionDirect check of the root condition#✓fully proved

Given code-level transition functions \(s\) on codes \(\alpha\) and \(t\) on codes \(\beta\), each listing labelled steps to codes, a relation \(R\) given as a list of code pairs, and codes \(x\) and \(y\), the root check succeeds exactly when every listed step \((a, x')\) of \(s(x)\) is matched by some listed step \((a, y')\) of \(t(y)\) with the same label and \((x', y') \in R\), and every listed step \((a, y')\) of \(t(y)\) is matched by some listed step \((a, x')\) of \(s(x)\) with the same label and \((x', y') \in R\).

This is a sufficient check of the root condition of observation congruence at \((x, y)\). Rooted weak bisimilarity also allows silent steps around the matching step, so the check is incomplete.

def rootCheck (s : α → List (Label Name × α)) (t : β → List (Label Name × β))
    (rel : List (α × β)) (x : α) (y : β) : Bool :=
  ((s x).all fun step => (t y).any fun spec =>
      spec.1 == step.1 && rel.contains (step.2, spec.2)) &&
    (t y).all fun spec => (s x).any fun step =>
      step.1 == spec.1 && rel.contains (step.2, spec.2)

Uses 1 · Used by 4

Statement usesCCS labels

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

TheoremCertificate checks give rooted observation congruence#✓fully proved

Let \(f\) realize the code-level transition function \(s\) and \(g\) realize \(t\) for a recursive specification, and let \(R\) be a list of code pairs on which the certificate check of \(s\), \(t\) and \(R\) succeeds. If the root check of \(s\), \(t\) and \(R\) succeeds at codes \(x\) and \(y\), then the processes \(f(x)\) and \(g(y)\) are rooted weakly bisimilar (observation congruent) in the labelled transition system of the specification (Milner, Chapter 7).

theorem rootedWeaklyBisimilar_of_certCheck (hf : Realizes spec f s) (hg : Realizes spec g t)
    (hcheck : certCheck s t rel = true) {x : α} {y : β} (hroot : rootCheck s t rel x y = true) :
    (Process.lts spec).RootedWeaklyBisimilar (f x) (g y)

Uses 12 · Used by 3

Statement usesRealization of a code-level transition system · Weak-bisimulation certificate check · Direct check of the root condition · CCS labels · Recursive CCS processes · Labelled transition system of a recursive specification · Recursive CCS specification · Rooted observation congruence

Proof usesCertificate checks give weak bisimilarity · Transitions of recursive CCS · Rooted weak transition · Transitions are rooted weak transitions

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

15 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.