A Local-Time Semantics for Negotiations

TL;DR

This paper introduces a local-time semantics for negotiations in concurrent systems, incorporating local clocks and synchronization constraints, revealing undecidability in reachability with mixed interactions, and exploring decidable restrictions.

Contribution

It extends negotiations with local-time semantics, including synchronization features, and analyzes the computational complexity, showing undecidability and identifying decidable cases.

Findings

Reachability is undecidable with mixed synchronized and unsynchronized interactions.

Synchronization constraints can model complex scenarios.

Restrictions on synchronization make reachability decidable.

Abstract

Negotiations, introduced by Esparza et al., are a model for concurrent systems where computations involving a set of agents are described in terms of their interactions. In many situations, it is natural to impose timing constraints between interactions -- for instance, to limit the time available to enter the PIN after inserting a card into an ATM. To model this, we introduce a real-time aspect to negotiations. In our model of local-timed negotiations, agents have local reference times that evolve independently. Inspired by the model of networks of timed automata, each agent is equipped with a set of local clocks. Similar to timed automata, the outcomes of a negotiation contain guards and resets over the local clocks. As a new feature, we allow some interactions to force the reference clocks of the participating agents to synchronize. This synchronization constraint allows us to model interesting scenarios. Surprisingly, it also gives unlimited computing power. We show that reachability is undecidable for local-timed negotiations with a mixture of synchronized and unsynchronized interactions. We study restrictions on the use of synchronized interactions that make the problem decidable.