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.

翻译：Esparza等人提出的协商是一种并发系统模型，其中涉及一组代理的计算通过其交互进行描述。在许多情况下，对交互施加时间约束是自然的——例如，限制在将卡插入ATM后输入PIN的可用时间。为建模此情况，我们为协商引入了实时性。在本地时间协商模型中，代理拥有独立演化的本地参考时间。受时间自动机网络模型的启发，每个代理配备一组本地时钟。类似于时间自动机，协商的结果包含对本地时钟的守卫和重置操作。作为一个新特性，我们允许某些交互强制参与代理的参考时钟同步。这种同步约束使我们能够建模有趣的场景。令人惊讶的是，它也赋予了无限的计算能力。我们证明，对于混合了同步与非同步交互的本地时间协商，可达性是不可判定的。我们研究了使问题可判定的同步交互使用限制。