Guessing the buffer bound for k-synchronizability

TL;DR

This paper investigates whether it is possible to determine if a communicating system has some finite buffer bound that makes it $k$-synchronizable, extending previous work that fixed $k$ and decided its properties.

Contribution

The authors prove that it is decidable whether there exists a finite buffer bound $k$ for a system to be $k$-synchronizable, generalizing prior fixed-$k$ results.

Findings

Decidability of the existence of a buffer bound $k$ for $k$-synchronizability.

Extension of previous fixed-$k$ decision procedures to variable $k$.

Implications for analyzing reachability in communicating systems.

Abstract

A communicating system is $k$-synchronizable if all of the message sequence charts representing the executions can be divided into slices of $k$ sends followed by $k$ receptions. It was previously shown that, for a fixed given $k$, one could decide whether a communicating system is $k$-synchronizable. This result is interesting because the reachability problem can be solved for $k$-synchronizable systems. However, the decision procedure assumes that the bound $k$ is fixed. In this paper we improve this result and show that it is possible to decide if such a bound $k$ exists.