Modelling concurrency with semi-commutations
The aim of this paper is to propose a mathematical tool, as well general as precise, for reasoning about concurrent systems. Ordered semi-commutative monoids are chosen for this purpose; their directed subsets represent processes of concurrent systems. Properties of such processes are proved; the main one is the diamond property. Infinite semitraces and their graphs are defined. Special sequences of actions, called linearizations and fair linearizations, are distinguished in order to represent finite and infinite processes. Finally, the approach is applied for modelling behaviours of general Petri-nets. Some kind of fairness, oriented on tokens, is introduced. It is shown that complete processes of general petri-nets, contrary to those of elementary nets, are not always fair.
KeywordsDependency Graph Concurrent System Concurrent Process Commutative Monoids Firing Sequence
Unable to display preview. Download preview PDF.
- M.Clerbout/M.Latteux: Semi-Commutations; Information and Computation 73, 1987.Google Scholar
- A.Mazurkiewicz: Complete Processes and Inevitability; Report 86-06, University of Leiden 1986.Google Scholar
- A.Mazurkiewicz: Trace Theory; Advanced Course on Petri Nets 86, LNCS 255, 1987.Google Scholar
- E.Ochmański: Semi-Commutation for Place/Transition Systems; EATCS Bulletin 38, June 1989.Google Scholar
- E.Ochmański: Semi-Commutation and Deterministic Petri Nets; Proceedings of MFCS'90, LNCS 452, 1990.Google Scholar