Abstract
Team automata describe networks of automata with input and output actions, extended with synchronisation policies guiding how many interacting components can synchronise on a shared input/output action. Given such a team automaton, we can reason over communication properties such as receptiveness (sent messages must be received) and responsiveness (pending receivesmust be satisfied). Previouswork focused on how to identify these communication properties. However, automatically verifying these properties is non-trivial, as it may involve traversing networks of interacting automata with large state spaces. This paper investigates (1) how to characterise communication properties for team automata (and subsumed models) using test-free propositional dynamic logic, and (2) how to use this characterisation to verify communication properties by model checking. A prototype tool supports the theory, using a transformation to interact with the mCRL2 tool for model checking.

Abstract
[No abstract available]

Abstract
Background: modern robots employ artificial intelligence algorithms in a broad ange of applications. These robots acquire information about their surroundings and use these highly-specialized algorithms to reason about their next actions. Despite their effectiveness, artificial intelligence algorithms are highly susceptible to adversarial attacks. This work focuses on mitigating attacks aimed at tampering with the communication channel between nodes running micro-ROS, which is an adaptation of the Robot Operating System (ROS) for extremely resource-constrained devices (usually assigned to collect information), and more robust nodes running ROS2, typically in charge of executing computationally costly tasks, like processing artificial intelligence algorithms. Methods: we followed the instructions described in the Data Distribution Service for Extremely Resource Constrained Environments (DDS-XRCE) specification on how to secure the communication between micro-ROS and ROS2 nodes and developed a custom communication transport that combines the application programming interface (API) provided by eProsima and the implementation of the Transport Security Layer version 1.3 (TLS 1.3) protocol developed by wolfSSL. Results: first, we present the first open-source transport layer based on TLS 1.3 to secure the communication between micro-ROS and ROS2 nodes, providing initial benchmarks that measure its temporal overhead. Second, we demystify how the DDS-XRCE and DDS Security specifications interact from a cybersecurity point of view. Conclusions: by providing a custom encrypted transport for micro-ROS and ROS2 applications to communicate, extremely resource-constrained devices can now participate in DDS environments without compromising the security, privacy, and authenticity of their message exchanges with ROS2 nodes. Initial benchmarks show that encrypted single-value messages present around 20% time overhead compared to the default non-encrypted micro-ROS transport. Finally, we presented an analysis of how the DDS-XRCE and DDS Security specifications relate to each other, providing insights not present in the literature that are crucial for further investigating the security characteristics of combining these specifications.

Abstract
We consider global models of communicating agents specified as transition systems labelled by interactions in which multiple senders and receivers can participate. A realisation of such a model is a set of local transition systems—one per agent—which are executed concurrently using synchronous communication. Our core challenge is how to check whether a global model is realisable and, if it is, how to synthesise a realisation. We identify and compare two variants to realise global interaction models, both relying on bisimulation equivalence. Then we investigate, for both variants, realisability conditions to be checked on global models. We propose a synthesis method for the construction of realisations by grouping locally indistinguishable states. The paper is accompanied by a tool that implements realisability checks and synthesises realisations. © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.

Abstract

Abstract