12

Because a CCS process is worth a thousand pixels – and it is easy to see the underlying LTS – here are two processes that simulates each other but are not bisimilar: $$P = ab + a$$ $$Q = ab$$ $\mathcal{R_1}=\{(ab+a, ab), (b, b), (0,b), (0, 0)\}$ is a simulation. $\mathcal{R_2}=\{(ab, ab+a), (b, b), (0,0)\}$ is a simulation. $P\ \mathcal R_1\ Q$ and $Q\ \...


10

Even if there's a simulation in each direction, the simulations back and forth may not relate the same sets of states. Sometimes you have a simulation $R_1$ in one direction, and a simulation $R_2$ in the other direction, and two states $p_1$ and $q$ which are related by $R_1$ but not by $R_2$ nor by any other simulation in the same direction. The canonical ...


9

You can easily profit from warfare that way: $$ M \stackrel{\mathrm{def}} = c.( d_{\text{tea}}.\bar e_{\text{tea}}.M + r.\bar b.M + c.( d_{\text{coffee}}.\bar e_{\text{coffee}}.M + r.\bar b.\bar b.M ) ) $$ note that you have to press refund to get a tea if you put too many coins. If you don't want that, you can ...


8

I only know CSP and CCS/pi-calculus (not ACP). CSP was motivated by imperative programming processes communicating via messages. Hoare then tried to abstract away a simple calculus out of it. CCS, on the other hand, was an effort to create a foundational calculus like lambda calculus. Given their original starting points, and given their final form, I ...


7

Another partial answer. The approach to semantics taken by the various communities differed, at least originally. ACP semantics are axiomatic/algebraic. CSP semantics are denotational, generally in terms of traces. CCS/$\pi$-calculus semantics are operational, generally in terms of labelled transition systems. Of course, since the original semantics, ...


6

Answering (at least) the part of your question regarding why research has diverged instead of converged. Being no expert on process algebras, I was once wondering the exact same thing: why are there so many theories? I was pointed to a survey by Parrow: Expressiveness of Process Algebras, 2008. I think it is very nicely written and even a novice could ...


5

This $M_0$ machine is more convenient than the one you propose: $$ M_0 := c.M_1 $$ $$ M_1 := d_{\text{tea}}.\bar e_{\text{tea}}.M_1 + r.\bar b.M_0 + c.M_2$$ $$ M_{n} := d_{\text{tea}}.\bar e_{\text{tea}}.M_{n-1} + d_{\text{coffee}}.\bar e_{\text{coffee}}.M_{n-2} + r.\underbrace{\bar b.\dots\bar b.}_{n}M_0 + c.M_{n+1}$$ (But using infinite processes is ...


5

You seem to be confusing the definition of bisimilarity with an algorithm for finding a bisimulation. In your examples, the states are indeed bisimilar, and the relation is the set $$\{(A,A)\}$$ It is easy to verify that it satisfies the desired properties. This means that the structures are indeed bisimilar. What you were trying to do is to find an ...


5

I think you are asking about expressivity of concurrent programming languages. This is a deep and not well-understood field. For example you say that "the $\pi$-calculus [...] has the power to implement almost any synchronization primitive I've ever heard of". It is well known that the $\pi$-calculus cannot implement broadcasting (see e.g. here). The $\pi$-...


5

To my knowledge the two terms do not have a formal established definition and are often used interchangeably. There are different characteristics associated to each however, as @Dave already pointed out. I'll try to elaborate a bit further. In both cases you start by introducing the syntax of a language for expressing (concurrent) systems. This introduces ...


4

The distinction is not so clear. Nevertheless, here is an attempt to provide an alternative answer to your question. A calculus involves calculation. Thus a process calculus will involve a notion of reduction. Examples include the $\pi$-calculus and CCS (and others from the Milner School). Algebra involves equations. A a process algebra will be phrased in ...


3

As to the question what benefits it would give you, the answer is simplicity. Modern programming languages are large beasts with complicated semantics, starting with syntax, and not ending with the rules for integer and floating point arithmetic (real languages, as you know, don't work with 'mathematical' integers and reals, but rather with finite ...


3

If you have doubts about whether a certain type of relation exists, a good place to search is Rob van Glabbeek's extensive catalogue of such relations. That article is a bit dated by now, but still extremely comprehensive. Linear Time-Branching Time Spectrum II, Robert J. van Glabbeek, 1993. There are several papers on the algorithmic aspect. I would ...


3

CSP is the formal basis of the programming language Occam which compiled to INMOS Transputers. Transputers appeared in all sorts of devices, such as set-top boxes for satellite TV. Eventually, however, the company doing all of this work failed to achieve commercial success, and was eventually absorbed by another company.


3

Late and early only make sense when building the LTS. The notion of bisimulation stays the same. However there are several notion of bisimilarities in the π-calculus for example. These are related to how new names are handled. It happens in the π-calculus because it is a name-passing process calculus. There is no such thing in CCS where names cannot be sent....


2

I am not completely sure about what is causing your confusion, but perhaps this can help: $a.\bar{b}.0$ can only perform $a$. $(a.\bar{b}.0)\setminus\{b\}$ can only perform $a$. $((a.\bar{b}.0)\setminus\{b\})[a\to b]$ can only perform $b$ (i.e. $a$ after substitution). The full process $((a.\bar{b}.0)\setminus\{b\})[a\to b]\mid(\bar{b}.b.0)+\bar{b}.c.0$ ...


2

(partial answer) For the relation $\mathcal{R} = \{(\tau.a, 0)\}$, $\mathcal{R} \nsubseteq \approx$ but $\mathcal{R} \subseteq \, \approx \! \mathcal{R} \approx$. Why is $\mathcal{R} \subseteq \, \approx \! \mathcal{R} \approx$? Actually, the inclusion $\mathcal{R} \subseteq \, \approx \! \mathcal{R} \approx$ holds for any relation $\mathcal{R}$, ...


2

I wondered if there were much more restrictive formalisms for describing concurrent processes? Petri nets are IMO more restrictive than the process calculus and such. They are state-transition systems, which are pretty much like formal grammars (like parsing expression grammars). They all boil down to states and rules / transitions. Petri nets include ...


2

Gilles' answer is very good and formal, and indeed, if $LTS_1$ is simulated by $LTS_2$ with a relation $R$, and $LTS_2$ is simulated by $LTS_1$ with the inverse of $R$, then $R$ is a bisimulation. However, if the two relations are not the inverse of one another, then you might not be able to build a bisimulation. For instance, a simple example comes from ...


2

As you propably know, a process (in terms of process algebra like CSP) can consume an input and will the behave like another process (unless it is a process that does not accept input, usually called STOP). You can construct a graph where the nodes are the processes and the outgoing edges the input that the node can consume, directed to the node (process) ...


2

You can always return the bisimulation $∅$ in constant time. You are right about the fact that in order to return $R$, you will have at least some sanity checks. For example you could think that returning all bisimulations of the form $\{(p,q)\}$ when $p$ and $q$ have the same label and such that $p\not→$ and $q\not→$ is easy, but not that much: you need ...


1

One of the most celebrated applications of CSP and was the use of the CSP tool FDR in the analysis of the Needham-Schroeder protocol. It has had other applications in analyzing protocols and software design. Breaking and fixing the Needham-Schroeder Public-Key Protocol using FDR, Gavin Lowe, TACAS 1996 Using CSP to detect errors in the TMN protocol ,...


1

The middle transition fertig is the shared action so this must be ran parallel, but after this there are 2 transitions which dont have to run parallel, one is kochen and the other is essen. Assume, we are now in the point where fertig is done by both processes and now we have 2 options, kochen and essen. We do both one after another as options: if i do ...


Only top voted, non community-wiki answers of a minimum length are eligible