locus: Blueprint🔗

A blueprint for locus: a Lean 4 mechanisation of Milner's bigraphs and bigraphical reactive systems, with their behavioural theory, a certified simulator and model checker, and an application. Each chapter states the main results of one part of the development in conventional notation, each attached to the Lean declaration that carries it; the Lean files hold the rest. Anything not yet proved is marked OPEN and has no Lean attachment.

Pages generated from the Lean, published on this site beside the Blueprint. Every figure in them is drawn from a Lean value, and every Lean excerpt is cut from the source by name.

A tutorial on bigraphs, in six chapters:

• I. Rooms, Wires and Laws: place graphs, link graphs and their composition.

• II. Rules, Reactions and CCS: reaction rules and reaction.

• III. Mobile processes: the π-calculus in bigraphs.

• IV. Contexts, Labels and Locations: labels from contexts, and bisimilarity.

• V. Adequacy for Linear Rules: engaged transitions, and adequacy for linear rules.

• VI. Modelling Miolingo: an application.

Problem books: chapter I and chapter II.

Animations and write-ups:

• Dining philosophers, model-checked: the naive, repaired and fair protocols and a livelock, each with the model checker's verdicts, and the alternating bit protocol, with its messages tracked. Every drawing is generated from the Lean model.

• Bigraph trace player: the player on its own, running the naive dining protocol to deadlock.

• The same fork, later: the tracked-logic write-up.

Papers: none yet.