Negative premises in applied process calculi

We explore two applications of negative premises to increase the expressive power of psi-calculi: reliable broadcasts and priorities. Together, these can be used to model discrete time, which we illustrate with an example from automotive applications. The negative premises can be encoded by a two-level structural operational semantics without negative premises; we use this fact to prove the standard congruence and structural laws of bisimulation with Nominal Isabelle.