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 P[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, P[N] is a symmetric strict monoidal category(1), parallel composition is the monoidal operation on morphisms and sequential composition is morphism composition. Besides P[N], we introduce a category S[N] containing the classical occurrence and step sequences. The term algebras of P[N] and of S[N] are in general incomparable, thus we introduce two more categories H[N] and S[N] providing an upper and a lower bound, respectively, A simple axiom expressing the functoriality of parallel composition maps H[N] to P[N] and S[N] to S[N], while commutativity of parallel composition maps H[N] to S[N] and P[N] to S[N] (see Fig.4).

Axiomatizing the algebra of net computations and processes

DEGANO, PIERPAOLO;MONTANARI, UGO GIOVANNI ERASMO
1996

Abstract

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 P[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, P[N] is a symmetric strict monoidal category(1), parallel composition is the monoidal operation on morphisms and sequential composition is morphism composition. Besides P[N], we introduce a category S[N] containing the classical occurrence and step sequences. The term algebras of P[N] and of S[N] are in general incomparable, thus we introduce two more categories H[N] and S[N] providing an upper and a lower bound, respectively, A simple axiom expressing the functoriality of parallel composition maps H[N] to P[N] and S[N] to S[N], while commutativity of parallel composition maps H[N] to S[N] and P[N] to S[N] (see Fig.4).
Degano, Pierpaolo; Meseguer, J; Montanari, UGO GIOVANNI ERASMO
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/11568/201697
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 47
  • ???jsp.display-item.citation.isi??? 42
social impact