Distinguishing between Communicating Transactions

TL;DR

This paper introduces a logical framework with three modal logics to analyze observable behaviors of communicating transactions, establishing their equivalence in distinguishing power and expressiveness, and presenting the first property logics for non-isolated transactions.

Contribution

It develops the first property logics for non-isolated transactions, demonstrating their equivalence in distinguishing power and expressiveness through semantics-preserving translations.

Findings

All three logics have the same distinguishing power.

Their associated weak bisimulations coincide with contextual equivalence.

The logics are equally expressive with semantics-preserving translations.

Abstract

Communicating transactions is a form of distributed, non-isolated transactions which provides a simple construct for building concurrent systems. In this paper we develop a logical framework to express properties of the observable behaviour of such systems. This comprises three nominal modal logics which share standard communication modalities but have distinct past and future modalities involving transactional commits. All three logics have the same distinguishing power over systems because their associated weak bisimulations coincide with contextual equivalence. Furthermore, they are equally expressive because there are semantics-preserving translations between their formulae. Using the logics we can clearly exhibit subtle example inequivalences. This work presents the first property logics for non-isolated transactions.

Full text

See pages 1-last of main.pdf