Logical fragments for Mazurkiewicz traces : expressive power and algebraic characterizations

Abstract

Mazurkiewicz trace are a model for concurrency. They can be seen as a generalization of words by introducing partial commutation between specific letters. Several logical and language-theoretic characterizations of the variety of monoids DA are known for words. We show which of them also hold for traces and which of them do not hold. An important tool for this task are Ehrenfeucht-Fraisse games. For several logical fragments, we introduce characterizations in terms of these games. They are used to separate logical fragments over traces that have the same expressive power over words. An essential property is, whether one can express concurrency within a fragment or not.

Mazurkiewicz Spuren sind ein Modell für Nebenläufigkeit. Sie entstehen als Verallgemeinerung von Wörtern, indem man partielle Kommutation zwischen einzelnen Buchstaben erlaubt. Wir zeigen, welche logischen und sprachtheoretischen Charakterisierung der Monoid-Varietät DA sich von Wörtern auf Spuren übertragen lassen und welche nicht. Ein wichtiges technisches Hilfsmittel dazu sind Ehrenfeucht-Fraisse-Spiele. Wir geben von verschiedenen logischen Fragmenten eine Charakterisierung durch solche Spiele an. Diese werden verwendet, um logische Fragmente, die über Wörtern gleich sind, bei Spuren von einander abzugrenzen. Ein wichtiges Kriterium hierbei ist, ob ein logisches Fragment die Formulierung von Nebenläufigkeit zulässt oder nicht.