Technical Report 2013-014

Negative Premises in Applied Process Calculi

Johannes Åman Pohjola, Johannes Borgström, Joachim Parrow, Palle Raabjerg, and Ioana Rodhe

June 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, 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.

Available as PDF (470 kB, no cover)

Download BibTeX entry.