Elementary transition systems and refinement

Abstract

Elementary transition systems are-in a strong categorical sense-the transition system version of a basic system model of net theory called elementary net systems. The structural notion of a region associated with elementary transition systems captures the intuitive idea of a local state as modelled by the conditions of an elementary net system. In this paper we equip elementary transition systems with a refinement operation over the local states (regions). We then show our operation satisfies a number of interesting properties. In particular, this operation supports compositional reasoning. It is very hard if not impossible to define a corresponding operation at the level of nets which enjoys similar properties. This is due to the concrete choice of conditions used to enforce intended behaviour. Thus our results show that the more abstract-but essentially equivalent-model of elementary transition systems is the appropriate framework for theoretical studies concerning refinement operations for elementary net systems.