Distinguishing between communicating transactions

DOI10.1016/J.IC.2017.12.001MaRDI QIDQ1706141zbMATH OpenOpenAlexFDO

Authors Vasileios Koutavas, Maciej Gazda, Matthew Hennessy

Publication date 21 March 2018

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1703.03256

zbMATH Keywords

Hennessy-Milner logicbisimulationcommunicating transactionsnon-isolated transactions

Mathematics Subject Classification ID

Logic in computer science (03B70) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

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.

Recommendations

• Communicating transactions (extended abstract)
• Bisimulations for communicating transactions (extended abstract)
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• \textsf{cJoin}: \textsf{Join} with communicating transactions
• scientific article; zbMATH DE number 2241924

Cites work

• scientific article; zbMATH DE number 177261 (Why is no real title available?)
• A domain equation for bisimulation
• A new approach to abstract syntax with variable binding
• Algebraic laws for nondeterminism and concurrency
• Bisimulations for communicating transactions (extended abstract)
• CONCUR 2005 – Concurrency Theory
• Communicating transactions (extended abstract)
• Formal Methods for the Design of Real-Time Systems
• Modal logics for mobile processes
• Modal logics for nominal transition systems
• Nominal logic, a first order theory of names and binding
• On reduction-based process semantics
• The \(\pi\)-calculus: A theory of mobile processes
• Transactional events
• Transactors: a programming model for maintaining globally consistent distributed state in unreliable environments
• \textsf{cJoin}: \textsf{Join} with communicating transactions

Cited in

(3)

• Modal logics for nominal transition systems
• Communicating transactions (extended abstract)
• Bisimulations for communicating transactions (extended abstract)

Describes a project that uses

Uses Software

• Transactors
• Uppaal

This page was built for publication: Distinguishing between communicating transactions

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1706141)