Labelled partially ordered sets (pomsets) are widely used to model the behavior of a concurrent system; in this approach, the order describes the causal dependence of the events while the labelling denotes which action is performed by an event. In particular, the incomparability of two events denotes that they can be executed simultaneously. Typical examples of this line of research are series-parallel pomsets, pomsets without autoconcurrency (also known as semiwords or partial words) and dependence graphs of Mazurkiewicz traces.
In this presentation, we propose two pomset semantics for a local trace language based on the idea of several sequential observers. Any such sequential observer sees a linear execution of the events. Comparing several sequential observations, one can obtain (partial) knowledge about the concurrency in the execution which then is represented as a pomset. In the first pomset semantics (called processes) we detect only some, but not necessarily all concurrency. Differently in the second pomset semantics (called proper pomsets), all concurrency is represented. Of course, these two semantics are closely related: The processes are the order extensions of the proper pomsets and the proper pomsets are those processes whose order cannot be weakened anymore. One can describe the model of Mazurkiewicz traces, of concurrent automata as well as that of P-traces in the realm of local trace languages. Our pomset semantics via proper pomsets generalize dependence graphs of Mazurkiewicz traces, dependence orders of stably concurrent automata as well as CCI-sets of P-traces.
Büchi’s paradigmatic result on the relation between finite automata and monadic second order logic has been generalized into different directions, e. g. to finite and infinite trees, to dependence graphs of Mazurkiewicz traces, to dependence orders of computations of stably concurrent automata, to graphs, to series-parallel pomsets, etc. Here, we present another generalization: a local trace language is recognizable if and only if its set of proper pomsets is bounded and definable in monadic second order logic. Furthermore, there are non-recognizable local trace languages whose set of proper pomsets is definable.