# Questions tagged [process-algebras]

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

19 questions
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 ...
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\}$, ...
55 views

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: $... 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 ... 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 ... 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 ... 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 ... 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 (... 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 ... 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'... 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 ... 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 ... 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 ... 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 ... 1answer 649 views ### LTS of this simple FSP I have this finite-state process with the corresponding labeled transition system: The FSP is: ... 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}... 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 \...
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 ...
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 ...