Systems for system implementation

Abstract

Inspired by Meseguer and Montanari's "Petri Nets are Monoids", we propose that a refinement o f a Petri net is a special kind o f net morphism were the target object is enriched with ali conceivable sequential and concurrent computations. Then it is proven that while refinement o f nets satisfies the vertical compositionality requirement (i.e., refinements compose), it lacks the horizontal compositionality requirement (i.e., refinement does not distribute over parallel composition). To achieve both requirements, a new categoria! semantic domain based on labeled transition systems with full concurrency, called nonsequential automata, is constructed. Again, a class of morphisms stands for refinement and, in this framework, the diagonal compositionality requirement (i.e., both vertical and horizontal) is achieved. Adjunctions between both models are provided extending the approach ofWinskel and Nielsen. The steps of abstraction involved in moving between models show that nonsequential automata are more concrete than Petri nets.