Axiomatizing the algebra of net computations and processes

Pierpaolo Degano, Jose Meseguer, Ugo Montanari

Research output: Contribution to journalArticle


Descriptions of concurrent behaviors in terms of partial orderings (called nonsequential processes or simply processes in Petri net theory) have been recognized as superior when information about distribution in space, about causal dependency or about fairness must be provided. However, at least in the general case of Place/Transition (P/T) nets, the proposed models lack a suitable, general notion of sequential composition. In this paper, a new algebraic axiomatization is proposed, where, given a net N, a term algebra script P sign [N] with two operations of parallel and sequential composition is defined. The congruence classes generated by a few simple axioms are proved isomorphic to a slight refinement of classical processes. Actually, script P sign[N] is a symmetric strict monoidal category1, parallel composition is the monoidal operation on morphisms and sequential composition is morphism composition. Besides script P sign[N], we introduce a category script capital L sign [N] containing the classical occurrence and step sequences. The term algebras of script P sign[N] and of script capital L sign [N] are in general incomparable, thus we introduce two more categories script K sign[N] and script T sign[N] providing an upper and a lower bound, respectively. A simple axiom expressing the functoriality of parallel composition maps script K sign[N] to script P sign[N] and script capital L sign[N] to script T sign[N], while commutativity of parallel composition maps script K sign[N] to script P sign[N] and (P[N] to script T sign[N] (see Fig. 4).

Original languageEnglish (US)
Pages (from-to)641-667
Number of pages27
JournalActa Informatica
Issue number7
StatePublished - Oct 1 1996
Externally publishedYes

ASJC Scopus subject areas

  • Software
  • Information Systems
  • Computer Networks and Communications

Fingerprint Dive into the research topics of 'Axiomatizing the algebra of net computations and processes'. Together they form a unique fingerprint.

  • Cite this