A Game-Based Semantics for CSP
Jesko Hecking-Harbusch
CSP is a well-studied modeling language for concurrent processes. It provides a textual representation for which several semantics are defined (e.g. transformation into labeled transition systems or into traces). In contrast, Petri games entail a formal definition of safety games in which the environment player and the system player can develop independently as well as synchronize on certain transitions. The realizability question and the synthesis problem can be answered for certain Petri games. In this thesis, an alternative, game-based semantics for CSP will be presented which produces Petri games. This semantics connects CSP and games. The rules of the structural operational semantics are outlined and a running example shows why such a semantics is beneficial and how the Petri game can be derived from a given CSP specification.
Bachelor Thesis.