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 to sorted 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 predicate sorting 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