nLab
trace alphabet

Contents

Idea

When discussing languages, say, in the theory of finite automata?, the usual starting point is a set, Σ\Sigma, of symbols, which is taken to be the alphabet for the language. The next step is to form the free monoid, Σ *\Sigma^*, on the alphabet, and then a language is simply a subset of Σ *\Sigma^*, and these can be used in a number of situations to describe the workings of a ‘system’, the symbols being used to represent certain operations or actions of the system, and the words in Σ *\Sigma^* thus corresponding to sequences of operations. Usually the system will not allow arbitrary sequences of operations to be performed, and so the system determines a language, namely the allowable execution sequences. Describing the language, helps describe and determine the overall ‘system’.

If the system being studied has some concurrency in it, so that certain of the operations are (causally) independent of each other, then one way of modelling such a system is to use a (Mazurkiewicz) trace alphabet, that is one in which the independence is explicitly taken into consideration.

Definition

A (Mazurkiewicz) trace alphabet is a pair (Σ,I)(\Sigma, I) where Σ\Sigma is a (usually finite) set of actions and IΣ×ΣI \subseteq \Sigma \times \Sigma is an irreflexive and symmetric relation.

The relation II is usually referred to as independence. Its complement D=(Σ×Σ)ID = (\Sigma \times \Sigma) - I is called the dependency relation. It will be reflexive and symmetric. (Such a sense of ‘dependency relation’ is interpreted in a related but slightly different way from that in the use of dependency graphs in project planning.)

Example

Consider the following ‘dependency diagram, with some vertices (states) and labelled edges (actions):

<inkscape:perspective id='perspective10' inkscape:persp3d-origin='372.04724 : 350.78739 : 1' inkscape:vp_x='0 : 526.18109 : 1' inkscape:vp_y='0 : 1000 : 0' inkscape:vp_z='744.09448 : 526.18109 : 1' sodipodi:type='inkscape:persp3d'></inkscape:perspective> <sodipodi:namedview bordercolor='#666666' borderopacity='1.0' gridtolerance='10000' guidetolerance='10' id='base' inkscape:current-layer='layer1' inkscape:cx='302.21784' inkscape:cy='362.85714' inkscape:document-units='px' inkscape:pageopacity='0.0' inkscape:pageshadow='2' inkscape:window-height='701' inkscape:window-width='663' inkscape:window-x='0' inkscape:window-y='22' inkscape:zoom='0.78209877' objecttolerance='10' pagecolor='#ffffff' showgrid='false'></sodipodi:namedview> <rdf:RDF> <cc:Work rdf:about=''> <dc:format>image/svg+xml</dc:format> <dc:type rdf:resource='http://purl.org/dc/dcmitype/StillImage'></dc:type> </cc:Work> </rdf:RDF> a b c d e

(arrow go from left to right but are not showing up … bother!)

We take Σ={a,b,c,d,e}\Sigma = \{ a,b,c,d,e\} and note that, starting at the left, bb depends on aa (written a<ba\lt b, since we cannot start action bb until action aa has been completed. This gives a labelled poset.

Here the first information to encode in DD is the poset structure of dependency

{(a,a),(a,b),(a,c),(a,d),(a,e),(b,b),(b,d),etc.},\{(a,a),(a,b),(a,c),(a,d),(a,e),(b,b),(b,d), etc.\},

then symmetrise this, and take the complement to get

I={(b,c),(c,b),(d,e),(e,d),(b,e),(e,b),(c,d),(d,c)}.I = \{(b,c),(c,b),(d,e),(e,d),(b,e), (e,b), (c,d),(d,c)\}.

Note this encoding does not involve the relationship given by adjacency, and hence ignore if an ‘execution sequence’ is ‘allowable’ (i.e., realistic) so (c,d)(c,d) is in II even though we could not first ‘do’ cc and then ‘do’ dd (unless of course bb had already been done).

The language (trace language?) corresponding to the model will be a subset of the trace monoid of the trace alphabet (Σ,I)(\Sigma, I) given here. It will encode allowable execution sequences but also will consider the allowable sequences ( traces ): abcdea b c d e, acbdea c b d e, abdcea b d c e, acebda c e b d etc. to be identified.

Reference

  • A Mazurkiewicz, Trace theory in ‘Advances in Petri Nets’, volume 255 of LNCS, Springer (1987).

Revised on November 15, 2010 07:50:42 by Tim Porter (95.147.238.71)