Abstract
A subgroup discovery-based method has recently been proposed to understand the behavior of models in the (original) feature space. The subgroups identified represent areas of feature space where the model obtains better or worse predictive performance when compared to the average test performance. For instance, in the marketing domain, the approach extracts subgroups such as: in groups of customers with higher income and who are younger, the random forest achieves higher accuracy than on average. Here, we propose a complementary method, Meta Subspace Analysis (MSA), MSA uses metalearning to analyze these subgroups in the metafeature space. We use association rules to relate metafeatures of the feature space represented by the subgroups to the improvement or degradation of the performance of models. For instance, in the same domain, the approach extracts rules such as: when the class entropy decreases and the mutual information increases in the subgroup data, the random forest achieves lower accuracy. While the subgroups in the original feature space are useful for the end user and the data scientist developing the corresponding model, the meta-level rules provide a domain-independent perspective on the behavior of the model that is suitable for the same data scientist but also for ML researchers, to understand the behavior of algorithms. We illustrate the approach with the results of two well-known algorithms, naive Bayes and random forest, on the Adult dataset. The results confirm some expected behavior of algorithms. However, and most interestingly, some unexpected behaviors are also obtained, requiring additional investigation. In general, the empirical study demonstrates the usefulness of the approach to obtain additional knowledge about the behavior of models.

Abstract
TCP is the default transport protocol of choice, namely for message-oriented middleware protocols (e.g., ZMTP, AMQP, MQTT) or distributed language runtimes (e.g., distributed Erlang), where exactly-once (EO) messaging is paramount. However, EO is only guaranteed within the TCP session, since reality shows that TCP connections can fail under many circumstances. Ensuring EO delivery ends up at the middleware layer, at the cost of higher complexity and lack of obliviouness - due to the use of permanent per-peer state. Moreover, using TCP at scale in highly concurrent systems leads to the need for TCP connection multiplexing, and possibly drastic performance loss due to head-of-line blocking. This paper introduces Exon, an oblivious exactly-once messaging protocol, and a corresponding lightweight (requiring no persistent storage, minimal memory, and low computation) library implementation over UDP. Exon uses a novel strategy of a per-message four-way protocol to ensure oblivious exactly-once messaging, with on-demand protocol-level "soft half-connections", established when needed and safely discarded. Obliviousness here refers to the protocol's ability to discard connection-specific state between incarnations, although some global information is retained. Exon achieves simultaneously: correctness with no timing assumptions, obliviousness, and performance through merging and pipelining basic protocol messages. Exon also employs a reliable delegation technique to handover the sending responsibility to a mediating node, without violating EO, when the sender the receiver are directly unreachable to each other and even if the message had already been delivered. The empirical evaluation of Exon demonstrates significant improvements (40%) over TCP in throughput and latency under packet loss, while maintaining a negligible (8%) overhead in healthy networks.

Abstract
Conflict-free Replicated Data Types (CRDTs) allow optimistic replication in a principled way. Different replicas can proceed independently, being available even under network partitions and always converging deterministically: Replicas that have received the same updates will have equivalent state, even if received in different orders. After a historical tour of the evolution from sequential data types to CRDTs, we present in detail the two main approaches to CRDTs, operation-based and state-based, including two important variations, the pure operation-based and the delta-state based. Intended for prospective CRDT researchers and designers, this article provides solid coverage of the essential concepts, clarifying some misconceptions that frequently occur, but also presents some novel insights gained from considerable experience in designing both specific CRDTs and approaches to CRDTs.

Abstract
This document presents the outcomes of the Dagstuhl Seminar Roadmap for Responsible Robotics, held in September 2023 at the Leibniz Center for Informatics, Schloss Dagstuhl, Germany. The seminar brought together researchers from the fields of robotics, computer science, social and cognitive sciences, and philosophy with the aim of charting a path toward improving responsibility in robotic systems. Through intensive interdisciplinary discussions centered on the various values at stake as robotics increasingly integrates into human life, the participants identified key priorities to guide future research and regulatory efforts. The resulting road map outlines actionable steps to ensure that robotic systems coevolve with human societies, promoting human agency and humane values rather than undermining them. Designed for diverse stakeholders-researchers, policy makers, industry leaders, practitioners, nongovernmental organizations (NGOs), and civil society groups-this road map provides a foundation for collaborative efforts toward responsible robotics.

Abstract
Distributed Hash Tables (DHTs) remain to this day a central component of modern peer-to-peer (P2P) systems, which rely on complex DHT protocols to scale to millions of nodes. The correct operation of DHTs is therefore essential for the proper functioning of these systems. For this reason, formal methods have been employed to model and verify a range of correctness properties of various DHT protocols. However, these verification efforts have focused on protocol-specific properties, such as topological invariants, instead of functional properties. This focus limits our understanding of the precise guarantees offered by each protocol. We propose a protocol-independent axiomatization of DHT properties using Allen Temporal Logic (ATL). To validate our axiomatization, we have implemented it in the Alloy analyser and used our implementation both to establish a number of DHT-derived properties and to generate a set of DHT execution traces that cover an exhaustive list of DHT corner case behaviours.

Abstract
TLA(+) is one of the most popular formal methods for designing concurrent and distributed systems. TLA(+) specifications can be verified with the TLC model checker, but unfortunately only one user-specified configuration of the system is verified at a time. If configurations are simple (e.g. the number of processes in a concurrent algorithm) it is viable to run TLC for several configurations to gain confidence that the system indeed works correctly for all of them. However, for complex configurations it is difficult to do so, and critical configurations can easily be missed. This paper introduces Blast, a tool that simplifies this task, by enabling the user to easily verify a TLA(+) specification for all configurations inside a given scope. Our evaluation using a large benchmark of TLA(+) examples, shows that Blast can be effectively used in a wide range of specifications and helped us uncover issues in several of them.