Constructing weak simulations from linear implications for processes with private names

Ross Horne*, Alwen Tiu

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

8 Citations (Scopus)
10 Downloads (Pure)


Abstract This paper clarifies that linear implication defines a branching-time preorder, preserved in all contexts, when used to compare embeddings of process in non-commutative logic. The logic considered is a first-order extension of the proof system BV featuring a de Morgan dual pair of nominal quantifiers, called BV1. An embedding of π-calculus processes as formulae in BV1 is defined, and the soundness of linear implication in BV1 with respect to a notion of weak simulation in the π -calculus is established. A novel contribution of this work is that we generalise the notion of a 'left proof' to a class of formulae sufficiently large to compare embeddings of processes, from which simulating execution steps are extracted. We illustrate the expressive power of BV1 by demonstrating that results extend to the internal π -calculus, where privacy of inputs is guaranteed. We also remark that linear implication is strictly finer than any interleaving preorder.

Original languageEnglish
Pages (from-to)1275-1308
Number of pages34
JournalMathematical Structures in Computer Science
Issue number8
Early online date29 Mar 2019
Publication statusPublished - 1 Sept 2019


  • calculus of structures
  • process calculi
  • proof theory
  • simulation


Dive into the research topics of 'Constructing weak simulations from linear implications for processes with private names'. Together they form a unique fingerprint.

Cite this