Simulating Truly Concurrent CSP - Formal Methods: Foundations and Applications - page 140

In [7], Kwiatkowska and Phillips have proposed a 'failures with divergence and
conflict' semantics for CSP. The semantics consists of a set of triples ( F , D , C ),
where F is a failure set, D a divergence set and C is a conflict relation on Σ ∗ ,
C

Σ ∗ , defined by induction on the syntax of CSP. Furthermore, they
distinguish possible conflict from guaranteed conflict. Analogously, they define a
concurrency relation co . Our definitions 2 and 1 (and proposition 3 in particular)
relate to their notions of possible concurrency and guaranteed conflict-freedom.
In contrast to their work, rather than define a new semantics of CSP we have
used the traces semantics

Σ ∗ ×

⊆

to simulate 'truly concurrent CSP'. In our approach,
concurrency is encountered whenever the controller's bag X grows beyond one
element with frequency one. In particular, a single event is concurrent with itself
if and only if there is a trace t such that its cardinality in the bag is greater than
one after t . In contrast, each trace is by definition concurrent with itself in the
semantics given by Kwiatkowska and Phillips.
Another important difference with that work is in refinement of concurrency
information. In their semantics, only the refinement

T

→ → → → → | ∅ |

a b STOP b a STOP a STOP b → STOP

holds but not conversely. Using the modified controller C 1 to incorporate con-
currency information in the traces of a process yields the opposite refinement
relation, as shown in example 6.1. Thus, in our approach, a process refines an-
other with a higher level of concurrency.
In [12], Taubner and Vogler present a non-interleaving semantics of CSP based
on the notion of 'step'. In their semantics, a step is a finite bag of events from
Σ . Traces and failures are lifted from sequences of events to sequences

of steps, and refusals are defined over sets of steps. The empty step is called
the null-step, and refusal of the null-step corresponds to divergence. A non-
divergent process may never refuse the null-step. Their semantics generalizes
the interleaving semantics of CSP in the sense that the special case of singleton
steps is exactly the interleaving semantics.
That approach, like ours, realizes possible concurrency in the sense that when-
ever a step is possible, all of its sub-steps are also possible. One distinguishing
feature of their semantics is that it lacks the commonly used τ event to model
hidden actions. While the authors present this as a theoretical advantage because
they succeed in establishing the common CSP laws in their semantics, it might
be considered a disadvantage from a practical perspective. For that reason, our
approach aims to detect any concurrent events, whether they are visible or hid-
den. The code related to an externally visible event a is likely to interfere with
the code of a hidden a that is executed concurrently. Therefore, our controller
registers even externally invisible events. Compared with their semantics, ours
appears more verbose because it records not only the steps but also the creation
of the steps (filling the bag).
On the level of traces our approach can be regarded as generalizing theirs: the
controller can be modified to ensure that it refuses new s events after an e event
until its bag is empty; that yields traces such that the state of the bag before

∪{ }