Sortings for Reactive Systems

We investigate sorting or typing for Leifer and Milner's reactive systems. We focus on transferring congruence properties for bisimulations from unsorted tosorted systems. Technically, we give a general definition of sorting; we adapt Jensen's work on the transfer of congruence properties to this general definition; we construct a predicate sorting, which, for any decomposible predicate P filters out agents not satisfying P; we prove that the predicatesorting preserves congruence properties and that it suitably retains dynamics; and finally, we show how the predicate sortings can be used to achieve context-aware reaction.