Weak $\omega$-Regular Trace Languages

TL;DR

This paper investigates the classification and automata-theoretic properties of $-regular trace languages, establishing new connections between trace-closed languages and automata recognizability, especially in the context of concurrent systems.

Contribution

It introduces definitions for classifying $-regular trace languages via trace-closed word languages and proves their equivalence to Boolean combinations of deterministically $I$-diamond Buchi recognizable trace-closed languages.

Findings

Established classification of $$-regular trace languages

Proved automata-theoretic equivalence with Boolean combinations of $I$-diamond Buchi languages

First automata-theoretic characterization of trace-closed $$-regular languages

Abstract

Mazurkiewicz traces describe concurrent behaviors of distributed systems. Trace-closed word languages, which are "linearizations" of trace languages, constitute a weaker notion of concurrency but still give us tools to investigate the latter. In this vein, our contribution is twofold. Firstly, we develop definitions that allow classification of $\omega$-regular trace languages in terms of the corresponding trace-closed $\omega$-regular word languages, capturing E-recognizable (reachability) and (deterministically) B\"uchi recognizable languages. Secondly, we demonstrate the first automata-theoretic result that shows the equivalence of $\omega$-regular trace-closed word languages and Boolean combinations of deterministically $I$-diamond B\"uchi recognizable trace-closed languages.