(joint work with Christel Baier, Sascha Klüppelholz, and Joachim Klein)

Priority designates an alternative among a set of possible actions of an actor as its preferred choice. In a concurrent system that involves many independent actors, the individual actors may not have compatible priorities. Such incompatible priorities make it non-trivial to determine what actions the system as a whole must take to remain consistent and to make coherent progress. This explains why in models of concurrency, priority is treated as a global, non-compositional property. Because of its compositional, distributed nature, such a global notion of priority does not bode well in Reo: accommodating priority in Reo requires a compositional model of priority.

In this talk, we present a compositional model of priority formalized as Constraint Automata with Priority (CAP). Although inspired by Reo, CAP constitutes an independent general model for specification and analysis of concurrent systems with priorities. CAP preserves, lifts, and propagates locally specified priorities through composition to yield globally consistent and coherent priorities for a composed system. For Reo, CAP serves as a new formal semantics that supports 4 new channel types: two priority-imposing and two priority-blocking channels. These primitives suffice to express preferences in selections via priority mergers, localize the effects of such preferences, etc. More interestingly, these primitives suffice to construct context-sensitive behavior (i.e., derive a context sensitive LossySync as a circuit constructed from these primitives and the non-deterministic LossySync channel).