2
$\begingroup$

In "Mobile Values, New Names, and Secure Communication", Abadí and Fournet describe thet Applied-$\pi$-Calculus. Although I understood a great part of the description of the Applied $\pi$-Calculus, I'm still a bit confused as to what exactly its formal semantics consists of.

The authors define (on page 2):

A signature $\Sigma$ consists of a finite set of function symbols, such as f, encrypt, and pairm each with an arity.

On page 3, they say that

Given a signature $\Sigma$, we equip it with an equational theory, that is, with an equivalence relation on terms that is closed under substitution of terms for variables.

Then they proceed, still on page 3, to define Structural equivalence, which also is an equivalence relation, but defined on extended processes and not terms.

So after reading the paper a number of times and consulting some other resources on the Internet, I have concluded that the semantics of the $\pi$-Calculus depends on a given signature (and hence is "parametrized" in a sense); and that it is composed of:

  • the signature and its equational theory, which is provided by us, depending on the application context (I may include symmetric cryptography functions and some equations modeling their behavior, and no asymmetric constructions at all, for example);
  • the structural equivalence relation for processes;
  • the internal reduction relation (structural semantics used for plain processes);
  • the reduction relation including interaction with the environment.

Is this correct, or did I miss anything?

|cite|improve this question
$\endgroup$
3
$\begingroup$

You are roughly correct. From an operational point-of-view, applied-$\pi$ is 'just' a $\pi$-calculus where interesting values (rather than just pure names) can be communicated.

Note that in process theory we usually care about coarser notions of equality, such as observational equivalence. This is defined in Section 4.1. Alas observational equivalence is hard to work with in practise due to the universal quantification over all contexts, so we define a second relation which is easier to deal with, in this case labelled bisimilarity. In order to do this, we need labelled transitions rather than reductions. We must show that these two forms of computation coincide.

To make matters even more complicated, Theorem 1 which claims that observational equivalence coincides with labelled bisimilarity is wrong.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ Could you expand on the error of that theorem? The actual result is what? $\approx \subseteq \approx_{\ell}$ or the opposite $\approx_{\ell} \subseteq \approx$ or are the two equivalences completely unrelated? $\endgroup$ – Bakuriu Sep 17 '16 at 13:34
  • $\begingroup$ @Bakuriu Sorry, don't have time now, start of term .... Abadi et al have just 2 days ago published a much revised version of the paper here, I have not read it, but maybe they deal with the question. $\endgroup$ – Martin Berger Sep 18 '16 at 9:47
  • $\begingroup$ They still have Theorem 4.1: Observational equivalence is labelled bisimilarity $\approx = \approx_{\ell}$. In section 4.5 they say that the claim is missing the hypothesis that exported variables must not be of channel type, otherwise there are processes that are in $\approx_{\ell}$ while not being $\approx$, they mention a paper by Liu where adding this hypothesis he is able to prove the theorem and argue that for their variant of the calculus and semantic the hypothesis is not needed, so it looks like they still think that the theorem is true. $\endgroup$ – Bakuriu Sep 18 '16 at 11:16

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.