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.
14
questions
0
votes
0
answers
30
views
Where can I find a list of logics with their corresponding calculus and computation phenomena?
I was watching some lectures by Prof. Pfenning on Proof Theory. Between 5:30 and 15:00, he gave a list for some different kinds of judgments along with their calculus and computation phenomena that ...
- 109
2
votes
1
answer
145
views
How to simulate natural number in Pi Calculus
I have some questions about Pi Calculus:
How to simulate the natural numbers only with its primitives?
It's possible simulate the if else clauses without the sum (+)?
A minimal and standart example ...
- 123
2
votes
0
answers
60
views
Applied $\pi$-calculus: Name binding and if clauses
Assume in the applied pi-calculus we have the following process:
$$(\nu n)\overline{c} \langle n \rangle.0 | (\nu n) (c(y).(\text{if n=y then P else Q}))$$
where $P$ and $Q$ are further processes.
I ...
- 21
2
votes
0
answers
53
views
What qualifies the structural relation in the pi calculus as a congruence?
In the pi calculus, there is an equivalence relation between terms that are structurally equivalent and should "act the same", which is usually described as structural congruence rules. For example, ...
- 711
5
votes
1
answer
141
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 ...
- 228
4
votes
1
answer
130
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 ...
- 83
1
vote
1
answer
119
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 "...
- 13
4
votes
1
answer
50
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.
...
- 807
5
votes
1
answer
94
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 ...
- 163
2
votes
1
answer
75
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'...
- 331
4
votes
2
answers
199
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|...
- 331
6
votes
1
answer
124
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 ...
- 243
7
votes
2
answers
448
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 ...
- 1,287
6
votes
1
answer
377
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}...
- 20.2k