7 - Reactions and transitions

Summary

In this chapter we study dynamics at the general level of s-categories. It is based upon Section 2.2 and Chapter 4, and is independent of the intervening work on bigraphs.

Recall from Chapter 2 the distinction between concrete and abstract bigraphs; the former have their nodes and edges as support, while the latter have no support. In s-categories, this distinction is less sharp; an spm category is just an s-category with empty supports. Much of the work of this chapter therefore applies to both. However, when we introduce behavioural equivalence in Section 7.2, we first make sure it is robust (i.e. that the equivalence is preserved by context) in the case where the s-category possesses RPOs; we are then able to retain this robust quality when the s-category is quotiented, or abstracted, in a certain way – even if RPOs are thereby lost.

We begin in Section 7.1 with a notion of a basic reactive system, based upon an s-category equipped with reaction rules. This determines a basic reaction relation which describes how agents may reconfigure themselves. We refine this definition to a wide reactive system, with a notion of locality based on the width of objects in a wide s-category, introduced in Definition 2.14. We are then able to describe where each reaction occurs in an agent, and thus to define a wide reaction relation that permits reactions to occur only in certain places.

In Section 7.2 we introduce labelled transition systems, which refine reactive systems by describing the reactions that an agent may perform, possibly with assistance from its environment.