Compliance for reversible client/server interactions

TL;DR

This paper extends the concept of compliance in session behaviors to include reversible interactions with checkpoints, providing formal semantics, a co-inductive characterization, and an algorithmic decision procedure.

Contribution

It introduces checkpoints into session behaviors, formalizes their compliance, and develops a sound, complete axiomatic system with an algorithmic decision procedure.

Findings

Defined checkpoint compliance for reversible interactions

Provided a co-inductive characterization of compliance

Developed a decision procedure for compliance

Abstract

In the setting of session behaviours, we study an extension of the concept of compliance when a disciplined form of backtracking is present. After adding checkpoints to the syntax of session behaviours, we formalise the operational semantics via a LTS, and define a natural notion of checkpoint compliance. We then obtain a co-inductive characterisation of such compliance relation, and an axiomatic presentation that is proved to be sound and complete. As a byproduct we get a decision procedure for the new compliance, being the axiomatic system algorithmic.