History monoid

History monoid

In mathematics and computer science, a history monoid is a way of representing the histories of concurrently running computer processes as a collection of strings, each string representing the individual history of a process. The history monoid provides a set of synchronization primitives (such as locks, mutexes or thread joins) for providing rendezvous points between a set of independently executing processes or threads.

History monoids occur in the theory of concurrent computation, and provide a low-level mathematical foundation for process calculi, such as CSP the language of communicating sequential processes, or CCS, the calculus of communicating systems. History monoids were first presented by M.W. Shields.[1]

History monoids are isomorphic to trace monoids (free partially commutative monoids) and to the monoid of dependency graphs. As such, they are free objects and are universal. The history monoid is a type of semi-abelian categorical product in the category of monoids.

Contents

Product monoids and projection

Let

A=(\Sigma_1,\Sigma_2,\ldots,\Sigma_n)

denote an n-tuple of alphabets Σk. Let P(A) denote all possible combinations of finite-length strings from the alphabets:

P(A)=\Sigma_1^* \times \Sigma_2^* \times \cdots \times \Sigma_n^*

(In more formal language, P(A) is the Cartesian product of the free monoids of the Σk. The superscript star is the Kleene star.) Composition in the product monoid is component-wise, so that, for

\bold{u}=(u_1,u_2,\ldots,u_n) \,

and

\bold{v}=(v_1,v_2,\ldots,v_n) \,

then

\bold{uv}=(u_1v_1,u_2v_2,\ldots,u_nv_n) \,

for all \bold{u}, \bold{v} in P(A). Define the union alphabet to be

\Sigma=\Sigma_1 \cup \Sigma_2 \cup \cdots \cup \Sigma_n. \,

(The union here is the set union, not the disjoint union.) Given any string w\in \Sigma^*, we can pick out just the letters in some \Sigma_k^* using the corresponding string projection \pi_k:\Sigma^*\to\Sigma_k^*. A distribution \pi:\Sigma^*\to P(A) is the mapping that operates on w\in \Sigma^* with all of the πk, separating it into components in each free monoid:

\pi(w)\mapsto (\pi_1(w), \pi_2(w), \ldots , \pi_n(w)). \,

Histories

For every a\in\Sigma, the tuple π(a) is called the elementary history of a. It serves as an indicator function for the inclusion of a letter a in an alphabet Σk. That is,

\pi(a)=(a_1,a_2,\ldots,a_n)

where

a_i=\begin{cases} 
a \mbox{ if } a\in \Sigma_k \\
\varepsilon \mbox { otherwise }.
\end{cases}

Here, ε denotes the empty string. The history monoid H(A) is the free monoid generated by elementary histories. It is clearly a submonoid of the product monoid P(A). The elements of H(A) are called global histories, and the projections of a global history are called individual histories.

Connection to computer science

The use of the word history in this context, and the connection to concurrent computing, can be understood as follows. An individual history is a record of the sequence of states of a process (or thread or machine); the alphabet Σk is the set of states of the process.

A letter that occurs in two or more alphabets serves as a synchronization primitive between the various individual histories. That is, if such a letter occurs in one individual history, it must also occur in another history, and serves to "tie" or "rendezvous" them together.

Consider, for example, Σ1 = {a,b,c} and Σ2 = {a,d,e}. The union alphabet is of course Σ = {a,b,c,d,e}. The elementary histories are (a,a), (b,ε), (c,ε), (ε,d) and (ε,e). In this example, an individual history of the first process might be bcbcc while the individual history of the second machine might be ddded. Both of these individual histories are represented by the global history bcbdddcced, since the projection of this string onto the individual alphabets yields the individual histories. In the global history, the letter b can be considered to commute with the letters d and e, in that these can be rearranged without changing the individual histories. Such commutation is simply a statement that the first and second processes are running concurrently, and are unordered with respect to each other; they have not (yet) exchanged any messages or performed any synchronization.

The letter a serves as a synchronization primitive, as its occurrence marks a spot in both the global and individual histories, that cannot be commuted across. Thus, while the letters b and c can be re-ordered past d and e, they cannot be reordered past a. Thus, the global history bcdabe and the global history bdcaeb both have as individual histories bcab and dae, indicating that the execution of d may happen before or after c. However, the letter a is synchronizing, so that e is guaranteed to happen after c, even though e is in a different process than c.

Properties

The history monoid is isomorphic to the trace monoid, and as such, is a type of semi-abelian categorical product in the category of monoids. In particular, the history monoid H(\Sigma_1,\Sigma_2,\ldots,\Sigma_n) is isomorphic to the trace monoid \mathbb{M}(D) with the dependency relation given by

D=\left(\Sigma_1\times\Sigma_1\right)\cup
\left(\Sigma_2\times\Sigma_2\right)\cup \cdots \cup
\left(\Sigma_n\times\Sigma_n\right).

In simple terms, this is just the formal statement of the informal discussion given above: the letters in an alphabet Σk can be commutatively re-ordered past the letters in an alphabet Σj, unless they are letters that occur in both alphabets. Thus, traces are exactly global histories, and vice-versa.

Notes

  1. ^ M.W. Shields "Concurrent Machines", Computer Journal, (1985) 28 pp. 449–465.

References

  • Antoni Mazurkiewicz, "Introduction to Trace Theory", pp 3–41, in The Book of Traces, V. Diekert, G. Rozenberg, eds. (1995) World Scientific, Singapore ISBN 9810220588
  • Volker Diekert, Yves Métivier, "Partial Commutation and Traces", In G. Rozenberg and A. Salomaa, editors, Handbook of Formal Languages, Vol. 3, Beyond Words, pages 457–534. Springer-Verlag, Berlin, 1997.

Wikimedia Foundation. 2010.

Игры ⚽ Поможем сделать НИР

Look at other dictionaries:

  • Monoid — This article is about the mathematical concept. For the alien creatures in the Doctor Who adventure, see The Ark (Doctor Who). Coherence law for monoid unit In abstract algebra, a branch of mathematics, a monoid is an algebraic structure with a… …   Wikipedia

  • Trace monoid — In mathematics and computer science, a trace is a set of strings, wherein certain letters in the string are allowed to commute, but others are not. It generalizes the concept of a string, by not forcing the letters to always be in a fixed order,… …   Wikipedia

  • Process calculus — In computer science, the process calculi (or process algebras) are a diverse family of related approaches to formally modelling concurrent systems. Process calculi provide a tool for the high level description of interactions, communications, and …   Wikipedia

  • Trace theory — In mathematics and computer science, trace theory aims to provide a concrete mathematical underpinning for the study of concurrent computation and process calculi. The underpining is provided by an algebraic definition of the free partially… …   Wikipedia

  • Communicating sequential processes — In computer science, Communicating Sequential Processes (CSP) is a formal language for describing patterns of interaction in concurrent systems.[1] It is a member of the family of mathematical theories of concurrency known as process algebras, or …   Wikipedia

  • Product (category theory) — In category theory, the product of two (or more) objects in a category is a notion designed to capture the essence behind constructions in other areas of mathematics such as the cartesian product of sets, the direct product of groups, the direct… …   Wikipedia

  • Synchronization (computer science) — In computer science, synchronization refers to one of two distinct but related concepts: synchronization of processes, and synchronization of data. Process synchronization refers to the idea that multiple processes are to join up or handshake at… …   Wikipedia

  • Исчисление взаимодействующих систем — (англ. Calculus of Communicating Systems, CCS, исчисление общающихся систем) в информатике  исчисление процессов, разработанное Робином Милнером в 1980 году. Исчисление работает с моделью неразделяемых коммуникаций между ровно двумя… …   Википедия

  • List of mathematics articles (H) — NOTOC H H cobordism H derivative H index H infinity methods in control theory H relation H space H theorem H tree Haag s theorem Haagerup property Haaland equation Haar measure Haar wavelet Haboush s theorem Hackenbush Hadamard code Hadamard… …   Wikipedia

  • Calculus of communicating systems — The Calculus of Communicating Systems (CCS) is a process calculus introduced by Robin Milner in around 1980. Its actions model indivisible communications between exactly two participants. The formal language includes primitives for describing… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”