OBJSA nets are a design specification language for real, thus complex, distributed systems, supporting both process and data abstraction since they combine the well established and supported specification language OBJ with superposed automata nets, a class of nets which emphasize compositionality. The paper introduces the notions of morphism and isomorphism for OBJSA net systems and shows that any OBJSA net system can be reduced to a unique, up to isomorphism, minimal model (in a net perspective). This allows the definition of equivalence classes of OBJSA models at the same level of abstraction. Furthermore, both a net semantics for OBJSA net systems, in terms of 1-safe SA net systems, and an algebraic semantics, in terms of OBJ3 objects, are given and it is proved that all the unfoldings, and, respectively, all the algebraic specifications, of OBJSA models belonging to the same class are isomorphic

Morphisms and minimal models for OBJSA nets / E. Battiston, F. De Cindio, G. Mauri, L. Rapanotti - In: Application and Theory of Petri NetsBerlin : SPRINGER, 1991. - pp. 455-476 (( convegno Application and Theory of Petri Nets. 12th International Conference tenutosi a Gjern, Denmark nel 26-28 June 1991.

Morphisms and minimal models for OBJSA nets

F. De Cindio
Secondo
;
1991

Abstract

OBJSA nets are a design specification language for real, thus complex, distributed systems, supporting both process and data abstraction since they combine the well established and supported specification language OBJ with superposed automata nets, a class of nets which emphasize compositionality. The paper introduces the notions of morphism and isomorphism for OBJSA net systems and shows that any OBJSA net system can be reduced to a unique, up to isomorphism, minimal model (in a net perspective). This allows the definition of equivalence classes of OBJSA models at the same level of abstraction. Furthermore, both a net semantics for OBJSA net systems, in terms of 1-safe SA net systems, and an algebraic semantics, in terms of OBJ3 objects, are given and it is proved that all the unfoldings, and, respectively, all the algebraic specifications, of OBJSA models belonging to the same class are isomorphic
Settore INF/01 - Informatica
1991
Book Part (author)
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

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: https://hdl.handle.net/2434/201290
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact