<p>Autonomous multi-agent systems use different modes of communication to support their autonomy and ease of interaction. In order to enable modelling and reasoning about such systems, we need frameworks that combine many forms of communication. <span>R-CHECK</span> is a modelling, simulation, and verification environment supporting the development of multi-agent systems, providing attributed channelled broadcast and multicast communication. Another common communication mode is point-to-point, wherein agents communicate with each other directly. Capturing point-to-point through <span>R-CHECK</span>’s multicast and broadcast is possible, but cumbersome and prone to interference. Here, we extend <span>R-CHECK</span> (and its underlying formal calculus <span>ReCiPe</span>) with bidirectional attributed point-to-point communication, which can be established based on identity or properties of participants. Moreover, we provide a compositional semantics that clearly describes how different modes of interaction co-exist without interference. We also support model-checking of point-to-point interactions by extending linear temporal logic with observation descriptors related to the participants in this communication mode. We argue that these extensions simplify the design, and demonstrate their benefits by means of an illustrative case study.</p>

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

A compositional semantics for reconfigurable multi-mode interaction in R-CHECK

  • Yehia Abd Alrahman,
  • Shaun Azzopardi,
  • Luca Di Stefano,
  • Nir Piterman

摘要

Autonomous multi-agent systems use different modes of communication to support their autonomy and ease of interaction. In order to enable modelling and reasoning about such systems, we need frameworks that combine many forms of communication. R-CHECK is a modelling, simulation, and verification environment supporting the development of multi-agent systems, providing attributed channelled broadcast and multicast communication. Another common communication mode is point-to-point, wherein agents communicate with each other directly. Capturing point-to-point through R-CHECK’s multicast and broadcast is possible, but cumbersome and prone to interference. Here, we extend R-CHECK (and its underlying formal calculus ReCiPe) with bidirectional attributed point-to-point communication, which can be established based on identity or properties of participants. Moreover, we provide a compositional semantics that clearly describes how different modes of interaction co-exist without interference. We also support model-checking of point-to-point interactions by extending linear temporal logic with observation descriptors related to the participants in this communication mode. We argue that these extensions simplify the design, and demonstrate their benefits by means of an illustrative case study.