I often hear phrases like 'true concurrency semantics' and 'true concurrency equivalences' without any references. What does those terms mean and why are they important?
What are some examples of true concurrency equivalences and what is the need for them? E.g. in which cases they are more applicable than more standard equivalences (bisimulation, trace equivalence, etc)?
The term "true concurrency" arises in the theoretical study of concurrent and parallel computation. It is in contrast to interleaving concurrency. True concurrency is concurrency that cannot be reduced to interleaving. Concurrency is interleaved if at each step in the computation, only one atomic computing action (e.g. an exchange of messages between sender and receiver) can take place. Concurrency is true if more than one such atomic action take place in a step.
The simplest way of distinguishing both is to look at the rule for parallel composition. In an interleaving based setting, it would look something like this:
$$\frac{P \rightarrow P'}{P|Q \rightarrow P'|Q}$$
This rule enforces that only one process in a parallel composition can execute an atomic action. For true concurrency, a rule like the following would be more appropriate.
$$\frac{P \rightarrow P'\quad Q \rightarrow Q'}{P|Q \rightarrow P'|Q'}$$
This rule allows both participants in a parallel composition to execute atomic actions.
Why would one be interested in interleaved concurrency, when concurrency theory is really the study of systems that execute computation steps in parallel? The answer is, and that's a great insight, that for simple forms of message passing concurrency, true concurrency and interleaving based concurrency are not contextually distinguishable. In other words, interleaved concurrency behaves like true concurrency as far as observers can see. Interleaving is a good decomposition of true concurrency. Since interleaving is easier to handle in proofs, people often only study the simpler interleaving based concurrency (e.g. CCS and $\pi$-calculi). However, this simplicity disappears for concurrent computation with richer forms of observation (e.g. timed computation): the difference between true concurrency and interleaved concurrency becomes observable.
Standard equivalences like bisimulations and traces have the same definitions for true and interleaving based concurrency. But they may or may not equate different processes, depending on the underlying calculus.
Let me give an informal explanation of why interleaving and truly concurrent interaction are indistinguishable in simple process calculi. The setting is a CCS or $\pi$-like calculus. Say we have a program
$$ P \quad=\quad \overline{x} \ |\ \overline{y} \ |\ x.y.\overline{a} \ |\ y.\overline{b} $$ Then we have the following truly concurrent reduction: \begin{eqnarray*} P &\rightarrow& y.\overline{a} \ |\ \overline{b} \end{eqnarray*} This reduction step can be matched by the following interleaved steps: \begin{eqnarray*} P &\rightarrow & \overline{x} \ |\ x.y.\overline{a} \ |\ \overline{b} \\ &\rightarrow & y.\overline{a} \ |\ \overline{b} \end{eqnarray*} The only difference between both is that the former takes one step, while the latter two. But simple calculi cannot detect the number of steps used to reach a process.
At the same time, $P$ has the following second interleaved reduction sequence: \begin{eqnarray*} P &\rightarrow & \overline{y} \ |\ y.\overline{a} \ |\ y.\overline{b} \\ &\rightarrow & \overline{a} \ |\ y.\overline{b} \end{eqnarray*} But this is also a reduction sequence in a truly concurrent setting, as long as true concurrency is not forced (i.e. interleaved executions are allowed even when there is potential for more than one interaction at a time).
To say the truth, I was googling for an answer myself. What is the semantics here? We assign a meaning "transition system" to the description "process algebra"; i.e. meaning is the transition system that is generated from the initial system description using defined SOS rules. Thus, using interleaving semantics, we lose all the concurrent structure in the obtained transition system.
Another answer could be that it is not "observable difference" but the difference in "observability". Using an interleaving semantics, we can observe only linear runs; whilst, using true concurrency we may observe "concurrent runs" (cf W.Reisig'13 Petri nets book).
Still, I have some doubts on what I said above, and it would be interesting to hear deeper insights. I.e., using Lamport vector clocks, how much of relativity theory can be transferred to concurrency theory.
