A Predicate Transformer for Choreographies (Full Version)

Sung-Shik Jongmans, Petra van den Bos

Research output: Book/ReportTechnical reportAcademic

69 Downloads (Pure)


Abstract. Construction and analysis of distributed systems is difficult; choreographic programming is a deadlock-freedom-by-construction approach to simplify it. In this paper, we present a new theory of choreographic programming. It supports for the first time: construction of distributed systems that require decentralised decision making (i.e., if/ while-statements with multiparty conditions); analysis of distributed systems to provide not only deadlock freedom but also functional correctness (i.e., pre/postcondition reasoning). Both contributions are enabled by a single new technique, namely a predicate transformer for choreographies.
Original languageEnglish
Place of PublicationHeerlen
PublisherOpen Universiteit Nederland
Number of pages36
Publication statusPublished - 2022

Publication series

SeriesOUNL-CS (Technical Reports)


Dive into the research topics of 'A Predicate Transformer for Choreographies (Full Version)'. Together they form a unique fingerprint.

Cite this