Negative premises in applied process calculi
Johannes Åman Pohjola, Johannes Borgström, Joachim Parrow, Palle Raabjerg, Ioana Rodhe · 2013
Abstract. 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, and 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. 1