Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [pi-calculus]

The pi-calculus is a model of concurrency in terms of communication over channels. It allows channel names to be exchanged over channel and thus permits changing network configurations.

4
votes
1answer
44 views

Are two CCS processes equivalent with respect to weak bisimilarity if and only if they satisfy exactly the same set of HML formulas?

I was skimming this recent paper and I was struck by the following statement: two processes are equivalent with respect to weak bisimilarity if and only if they satisfy exactly the same set of HML ...
4
votes
1answer
53 views

Recursion in pi-calculus

In the book by Sangiorgi and Walker ("The $\pi$-calculus: A theory of Mobile Processes"), Subsection 3.2 is devoted to recursion. They state the following constraint (pages 132-133): "The ...
1
vote
1answer
34 views

Is the Choice operator implementable on $\pi$-calculus?

I was reading about $\pi$-calculus, and some authors include in the basic operations a Choice operator $P \oplus Q$ which means that either $P$ or $Q$ will be executed, but not both. On page 8 of "...
4
votes
1answer
37 views

What is a “name/variable of base type” in applied $\pi$-calculus?

I'm studying the articleVerifying privacy-type properties of electronic voting protocols which uses Applied $\pi$-calculus to formalize voting protocols and verifies some privacy-related properties. ...
5
votes
1answer
71 views

Sequential execution in $\pi$-calculus

I am relatively new to $\pi$-Caculus and have a doubt wrt sequential execution in In $\pi$-Calculus . Does passing of common names over common channels shared between two Agents, represent a ...
2
votes
1answer
59 views

How exactly does on describe the formal semantics of the Applied $\pi$-Calculus?

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'...
3
votes
2answers
116 views

Why do some authors not include summation in the $\pi$-Calculus?

In Robin Milner's book "Communicating and Mobile Systems: the $\pi$-Calculus", on page 87, the set of expressions of the $\pi$-Calculus is defined as $$P ::= \sum_{i\in I} \pi_i.P_i\ {\huge|}\ P_1|...
6
votes
1answer
104 views

Pi Calculus: Restriction necessary for molecular (atomic) action?

In "A Calculus of Mobile Processes, Part 1" [1], Milner et al. give an example for transmitting a pair of values $(u,v)$ from the process $P$ to either $R$ or $Q$ (see page 13). All three processes ...
7
votes
2answers
293 views

Automaton equivalent of the π calculus?

If Turing Machines are the automata equivalent of the $\lambda$ calculus, what is the automaton equivalent of the $\pi$ calculus? I suppose it would be some class of automata that resembled a Turing ...
6
votes
1answer
295 views

Late and Early Bisimulation

This is a follow up to my earlier questions on coinduction and bisimulation. A relation $R \subseteq S \times S$ on the states of an LTS is a bisimulation iff $\forall (p,q)\in R,$ $$ \begin{array}...