In the model of negotiations introduced by Esparza et al. (2013), a distributed set of agents strive to achieve a final outcome through a sequence of negotiations within potentially smaller groups. Mukund et al. (2023) extended this model to include timing constraints between negotiations. In this model of local-timed negotiations (LTNs), each agent has its own local reference clock that evolves independently of the others, and represents its local-time. Apart from their reference clocks, agents can have other local clocks that can be checked for guards and updated using resets (like in a timed automaton), when they move from one negotiation to another. LTNs come with a special feature where negotiations can be specified to be time-synchronizing or not. Agents participating in a time-synchronizing negotiation are required to synchronize their local reference clocks before deciding on an outcome. Due to this feature, agents which have drifted far apart in their local times are forced to resynchronize their local-times again. This makes reachability undecidable for LTNs. In this paper, we consider LTNs which ensure a connected communication: in every cyclic behaviour, every agent participates in a time-synchronization with every other agent, either directly or indirectly. We show that connected communication makes reachability in LTNs decidable. A counterpart of this notion of connected communication has been used in message sequence graphs by Alur et al. (1999), and in distributed controller synthesis by Thiagarajan et al. (2005) to gain decidability.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Using Communication to Bound Clock Drift in Local-Timed Negotiations

  • Abhinav Garg,
  • Madhavan Mukund,
  • Adwitee Roy,
  • B. Srivathsan,
  • Gautham Viswanathan

摘要

In the model of negotiations introduced by Esparza et al. (2013), a distributed set of agents strive to achieve a final outcome through a sequence of negotiations within potentially smaller groups. Mukund et al. (2023) extended this model to include timing constraints between negotiations. In this model of local-timed negotiations (LTNs), each agent has its own local reference clock that evolves independently of the others, and represents its local-time. Apart from their reference clocks, agents can have other local clocks that can be checked for guards and updated using resets (like in a timed automaton), when they move from one negotiation to another. LTNs come with a special feature where negotiations can be specified to be time-synchronizing or not. Agents participating in a time-synchronizing negotiation are required to synchronize their local reference clocks before deciding on an outcome. Due to this feature, agents which have drifted far apart in their local times are forced to resynchronize their local-times again. This makes reachability undecidable for LTNs. In this paper, we consider LTNs which ensure a connected communication: in every cyclic behaviour, every agent participates in a time-synchronization with every other agent, either directly or indirectly. We show that connected communication makes reachability in LTNs decidable. A counterpart of this notion of connected communication has been used in message sequence graphs by Alur et al. (1999), and in distributed controller synthesis by Thiagarajan et al. (2005) to gain decidability.