Trace theory
Encyclopedia
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 commutative monoid or trace monoid
, or equivalently, the history monoid
, which provides a concrete algebraic foundation, analogous to the way that the free monoid provides the underpining for formal language
s.
The power of trace theory stems from the fact that the algebra of dependency graph
s (such as Petri net
s) is isomorphic to that of trace monoids, and thus, one can apply both algebraic formal language
tools, as well as tools from graph theory
.
While the trace monoid had been studied by Pierre Cartier
and Dominique Foata
for its combinatorics
in the 1960s, trace theory was first formulated by Antoni Mazurkiewicz in the 1970s, in an attempt to evade some of the problems in the theory of concurrent computation, including the problems of interleaving and non-deterministic choice with regards to refinement in process calculi.
Mathematics
Mathematics is the study of quantity, space, structure, and change. Mathematicians seek out patterns and formulate new conjectures. Mathematicians resolve the truth or falsity of conjectures by mathematical proofs, which are arguments sufficient to convince other mathematicians of their validity...
and computer science
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, 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 commutative monoid or trace monoid
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, but allowing certain reshufflings to take place...
, or equivalently, the 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...
, which provides a concrete algebraic foundation, analogous to the way that the free monoid provides the underpining for formal language
Formal language
A formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...
s.
The power of trace theory stems from the fact that the algebra of dependency graph
Dependency graph
In mathematics, computer science and digital electronics, a dependency graph is a directed graph representing dependencies of several objects towards each other...
s (such as Petri net
Petri net
A Petri net is one of several mathematical modeling languages for the description of distributed systems. A Petri net is a directed bipartite graph, in which the nodes represent transitions and places...
s) is isomorphic to that of trace monoids, and thus, one can apply both algebraic formal language
Formal language
A formal language is a set of words—that is, finite strings of letters, symbols, or tokens that are defined in the language. The set from which these letters are taken is the alphabet over which the language is defined. A formal language is often defined by means of a formal grammar...
tools, as well as tools from graph theory
Graph theory
In mathematics and computer science, graph theory is the study of graphs, mathematical structures used to model pairwise relations between objects from a certain collection. A "graph" in this context refers to a collection of vertices or 'nodes' and a collection of edges that connect pairs of...
.
While the trace monoid had been studied by Pierre Cartier
Pierre Cartier (mathematician)
Pierre Cartier is a mathematician. An associate of the Bourbaki group and at one time a colleague of Alexander Grothendieck, his interests have ranged over algebraic geometry, representation theory, mathematical physics, and category theory....
and Dominique Foata
Dominique Foata
Dominique Foata is a mathematician who works in enumerative combinatorics. With Pierre Cartier and Marcel-Paul Schützenberger he pioneered the modern approach to classical combinatorics, that lead, in part, to the current blossoming of algebraic combinatorics...
for its combinatorics
Combinatorics
Combinatorics is a branch of mathematics concerning the study of finite or countable discrete structures. Aspects of combinatorics include counting the structures of a given kind and size , deciding when certain criteria can be met, and constructing and analyzing objects meeting the criteria ,...
in the 1960s, trace theory was first formulated by Antoni Mazurkiewicz in the 1970s, in an attempt to evade some of the problems in the theory of concurrent computation, including the problems of interleaving and non-deterministic choice with regards to refinement in process calculi.