Questions tagged [process-algebras]
Process algebras (also known as process calculi) are formal models of concurrency
23 questions
1
vote
0
answers
27
views
Rationale behind prefix-closure in CSP trace semantics
I'm currently studying Hoare's "Communicating Sequential Processes" (1) and I've come across a concept that I find a bit puzzling. In CSP trace semantics, a process's semantics are described ...
- 111
2
votes
0
answers
46
views
Why process algebras à la chemical abstract machine are not common?
I recently read the Berry and Boudol's chemical abstract machine [1, 2]. I found the way they describe the semantic really nice and quite intuitive for a process calculus.
The aspect that really ...
- 121
0
votes
1
answer
63
views
Stratification of Bisimilarity : $\sim$ does not coincide with $\sim_\omega$
I am reading Sangiorgi's paper On the origins of bisimulation an coinduction.
Definition 2.5, on page 5, defines Stratification of Bisimilarity:
Let $W$ be the states of an LTS. We set:
$\sim_0 \...
- 121
2
votes
1
answer
79
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
3
votes
2
answers
153
views
Benefit of Petri Net Transition as Separate Object
In learning about Timed Automata, Coloured Petri Nets, and Process Calculi, I am wondering what the benefit is of having the Petri Net transition be a separate type of node in Petri Nets.
It seems ...
- 2,295
2
votes
1
answer
157
views
Restriction and re-labeling on CCS
In a process like
$$
R \stackrel{def}=((a.\bar{b}.0)\setminus\{b\})[a\to b]\mid(\bar{b}.b.0)+\bar{b}.c.0
$$
$b$ is restricted to perform on the inner process of RHS $(a.\bar{b}.0)\setminus\{b\}$, ...
- 268
3
votes
1
answer
83
views
Weak bisimulation up-to $\approx$
Given this definition of weak bisimilarity:
A configuration relation $\mathcal{R}$ is a weak bisimulation
provided that whenever $P\ \mathcal{R}\ Q$ and $\alpha$ is $\mu$ or $\tau$ action then:
$...
- 133
5
votes
1
answer
60
views
Are there (highly) restricted process calculi? Perhaps similar to formal grammar?
I've started to read about process calculi (such as CSP and π-calculus). It seems to me that they are extremely general and can represent pretty much any concurrent system, many of which will be ...
- 263
5
votes
1
answer
133
views
Problem with definition of bisimilarity
In my model checking class we have defined a bisimulation like this:
Let $K=(S,S_0,Act,R,L)$ and $K'=(S',S'_0,Act,R',L')$ be two kripke structures. A relation $B \subseteq S \times S'$ is called ...
- 415
4
votes
1
answer
210
views
How does lack of deadlock relate to computability in process calculi?
I'm interested in knowing things about the computability of concurrent programs. If you had a Turing complete language that also let you branch off new programs but had no means of communication ...
- 3,800
1
vote
0
answers
63
views
Communication senario: A sends to B or B sends to A
Consider processes A and B and the situation where either A will send a message to B or B will send a message to A. Is there a standard algorithm for this scenario that makes sure that exactly one of ...
- 107
4
votes
0
answers
78
views
Deadlock free process calculi
So when programming with locks as a synchronization primitives you can ensure no deadlock by ensuring that an ordering exists on the locks and that all acquires of the locks happen in that order (...
- 3,800
3
votes
2
answers
521
views
Terminologies of "Process calculus" and "Process algebra" [duplicate]
In the literature, the terms of "process calculus" and "process algebra" are often interchangeable. Meanwhile, it confused me.
My questions are:
Are there formal, standard, and widely-accepted ...
- 9,641
4
votes
1
answer
198
views
How to express Rob Pike's classic Go Code presentation in Hoare's CSP Algebra?
At 15:30 in this talk (p13 of this presentation here) Rich Hickey mentions the formalisms available for reasoning about Communicating Sequential Processes. He then goes on to mention that these haven'...
- 1,199
2
votes
2
answers
508
views
What are some of the practical applications of CSP process algebra?
CSP is used for the description and representation of concurrent systems, how it is used in practice (theoretically and programmatically)?
What are the application areas (other than concurrent and ...
- 87
3
votes
1
answer
88
views
Process graphs and finding infinite processes
I am reading on concurrent processes and algorithms which find infinite processes by searching the process graph recursively.
Most of the material I have found is not for beginners. I am looking for ...
- 33
3
votes
1
answer
183
views
How to quickly find a few bisimulations on a given labelled digraph?
We are given a labelled directed graph, where both vertices (or states) and edges (or transitions) have labels. Informally, two states are bisimilar when they have the same label and they can simulate ...
- 22.8k
4
votes
1
answer
465
views
How to implement simulation on two LTSs?
Does any one know how to implement the simulation relation on two labelled transition systems (LTS)?
I know how to do it for branching bi-simulation. The signature refinement theorem is used for ...
- 41
2
votes
1
answer
965
views
LTS of this simple FSP
I have this finite-state process with the corresponding labeled transition system:
The FSP is:
...
- 243
6
votes
1
answer
399
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.3k
21
votes
3
answers
4k
views
When are two simulations not a bisimulation?
Given a labelled transition system $(S,\Lambda,\to)$, where $S$ is a set of states, $\Lambda$ is a set of labels, and $\to\subseteq S\times\Lambda\times S$ is a ternary relation. As usual, write $p \...
- 20.3k
23
votes
3
answers
2k
views
Similarities and differences in major process algebras
To my knowledge, there are three major process algebras that have inspired a vast range of research into formal models of concurrency. These are:
CCS and $\pi$-calculus both by Robin Milner
CSP by ...
- 20.3k
11
votes
2
answers
257
views
CCS process for a drink dispenser with two different prices
A drink dispenser requires the user to insert a coin ($\bar c$), then press one of three buttons: $\bar d_{\text{tea}}$ requests a cup of tea $e_{\text{tea}}$, ditto for coffee, and $\bar r$ requests ...
