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 [process-algebras]

Process algebras (also known as process calculi) are formal models of concurrency

1
vote
1answer
51 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
votes
1answer
40 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\}$, ...
3
votes
1answer
55 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: $...
5
votes
1answer
49 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 ...
5
votes
1answer
57 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 ...
4
votes
1answer
82 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 ...
1
vote
0answers
58 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 ...
4
votes
0answers
63 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
votes
2answers
333 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 ...
4
votes
1answer
151 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'...
2
votes
2answers
385 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 ...
3
votes
1answer
75 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 ...
3
votes
1answer
135 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 ...
4
votes
1answer
349 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 ...
2
votes
1answer
649 views

LTS of this simple FSP

I have this finite-state process with the corresponding labeled transition system: The FSP is: ...
6
votes
1answer
297 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}...
19
votes
3answers
3k 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 \...
19
votes
3answers
1k 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 ...
11
votes
2answers
202 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 ...