Pomsets for Local Trace Languages

Mazurkiewicz traces can be seen as equivalence classes of words or as pomsets. Their generalisation by local traces was formalized by Hoogers, Kleijn and Thiagarajan as equivalence classes of step firing sequences. First we introduce a pomset representation for local traces. Extending Büchi’s Theorem and a previous generalisation to Mazurkiewicz traces, we show then that a local trace language is recognized by a finite step transition system if and only if its class of pomsets is bounded and definable in the Monadic Second Order logic. Finally, using Zielonka’s Theorem, we show that each recognizable local trace language is described by a finite safe labelled Petri net.The complete version [22] of this paper is accessible on the web.