Semantics frameworks for a class of modular algebraic nets

Among the various proposal for an `algebraic specification of concurrency', OBJSA Nets are a class of algebraic high-level nets which combine superimposed automata (SA) nets, a modular class of Petri nets, and the algebraic specification language OBJ. OBJSA Nets together with their support environment ONE (OBJSA Net Environment), constitute a specification language for distributed systems which is called OBJSAN as each OBJSAN specification is mapped by ONE into an OBJSA Net. To enhance specification modularity and reusability, an OBJSAN specification is obtained by composing, via transition fusion (i.e., superposition), some OBJSAN (open) components. An OBJSAN component is a couple which consists of a net and an OBJ module. The net part expresses the control of the system to be specified and the OBJ part describes data modification through occurrence of events modelled by net transitions. An OBJSAN component is either closed, if all of its transitions are closed, or open if it contains at least one open transition, i.e., a transition which is only partially extensionally specified, since couples of its input/output places have to be identified through superposition of the transition itself with other transition(s). Open transitions represent the interface of the component toward other components, and are specified by non executable modules (in OBJ called theories), while close transitions are specified by executable modules (in OBJ called theories