Peer-to-peer systems are the most resilient form of distributed computing, but the design of robust protocols for their coordination is difficult. This makes it hard to specify and reason about global behaviour of such systems. This paper presents swarm protocols to specify such systems from a global viewpoint. Swarm protocols are projected to machines, that is local specifications of peers. We take inspiration from behavioural types with a key difference: peers communicate through an event notification mechanism rather than through point-to-point message passing. Our goal is to adhere to the principles of local-first software where network devices collaborate on a common task while retaining full autonomy: every participating device can locally make progress at all times, not encumbered by unavailability of other devices or network connections. This coordination-free approach leads to inconsistencies that may emerge during computations. Our main result shows that under suitable well-formedness conditions for swarm protocols consistency is eventually recovered and the locally observable behaviour of conforming machines will eventually match the global specification. The model we propose elaborates on an existing industrial platform and provides the basis for tool support (sketched here and fully described in a companion artifact paper), wherefore we consider this work to be a viable step towards reasoning about local-first and peer-to-peer software systems.
The asynchronous and unidirectional communication model supported by mailboxes is a key reason for the success of actor languages like Erlang and Elixir for implementing reliable and scalable distributed systems. While many actors may send messages to some actor, only the actor may (selectively) receive from its mailbox. Although actors eliminate many of the issues stemming from shared memory concurrency, they remain vulnerable to communication errors such as protocol violations and deadlocks. Mailbox types are a novel behavioural type system for mailboxes first introduced for a process calculus by de'Liguoro and Padovani in 2018, which capture the contents of a mailbox as a commutative regular expression. Due to aliasing and nested evaluation contexts, moving from a process calculus to a programming language is challenging. This paper presents Pat, the first programming language design incorporating mailbox types, and describes an algorithmic type system. We make essential use of quasi-linear typing to tame some of the complexity introduced by aliasing. Our algorithmic type system is necessarily co-contextual, achieved through a novel use of backwards bidirectional typing, and we prove it sound and complete with respect to our declarative type system. We implement a prototype type checker, and use it to demonstrate the expressiveness of Pat on a factory automation case study and a series of examples from the Savina actor benchmark suite.
Many multivariate data sets exhibit a form of positive dependence, which can either appear globally between all variables or only locally within particular subgroups. A popular notion of positive dependence that allows for localized positivity is positive association. In this work we introduce the notion of extremal positive association for multivariate extremes from threshold exceedances. Via a sufficient condition for extremal association, we show that extremal association generalizes extremal tree models. For H\"usler--Reiss distributions the sufficient condition permits a parametric description that we call the metric property. As the parameter of a H\"usler--Reiss distribution is a Euclidean distance matrix, the metric property relates to research in electrical network theory and Euclidean geometry. We show that the metric property can be localized with respect to a graph and study surrogate likelihood inference. This gives rise to a two-step estimation procedure for locally metrical H\"usler--Reiss graphical models. The second step allows for a simple dual problem, which is implemented via a gradient descent algorithm. Finally, we demonstrate our results on simulated and real data.
Cooperative multi-agent reinforcement learning (MARL) for navigation enables agents to cooperate to achieve their navigation goals. Using emergent communication, agents learn a communication protocol to coordinate and share information that is needed to achieve their navigation tasks. In emergent communication, symbols with no pre-specified usage rules are exchanged, in which the meaning and syntax emerge through training. Learning a navigation policy along with a communication protocol in a MARL environment is highly complex due to the huge state space to be explored. To cope with this complexity, this work proposes a novel neural network architecture, for jointly learning an adaptive state space abstraction and a communication protocol among agents participating in navigation tasks. The goal is to come up with an adaptive abstractor that significantly reduces the size of the state space to be explored, without degradation in the policy performance. Simulation results show that the proposed method reaches a better policy, in terms of achievable rewards, resulting in fewer training iterations compared to the case where raw states or fixed state abstraction are used. Moreover, it is shown that a communication protocol emerges during training which enables the agents to learn better policies within fewer training iterations.
In 1975 the first author proved that every finite tight two-person game form $g$ is Nash-solvable, that is, for every payoffs $u$ and $w$ of two players the obtained game $(g;u,w)$, in normal form, has a Nash equilibrium (NE) in pure strategies. This result was extended in several directions; here we strengthen it further. We construct two special NE realized by a lexicographically safe (lexsafe) strategy of one player and a best response of the other. We obtain a polynomial algorithm computing these lexsafe NE. This is trivial when game form $g$ is given explicitly. Yet, in applications $g$ is frequently realized by an oracle $\cO$ such that size of $g$ is exponential in size $|\cO|$ of $\cO$. We assume that game form $g = g(\cO)$ generated by $\cO$ is tight and that an arbitrary {\em win-lose game} $(g;u,w)$ (in which payoffs $u$ and $w$ are zero-sum and take only values $\pm 1$) can be solved, in time polynomial in $|\cO|$. These assumptions allow us to construct an algorithm computing two (one for each player) lexsafe NE in time polynomial in $|\cO|$. We consider four types of oracles known in the literature and show that all four satisfy the above assumptions.
We investigate the asymptotics for two geometric measures, geometric quantiles and halfspace depths. While much literature is known on the population side, we fill out some gaps there to obtain a full picture, before turning to the sample versions, where the questions on asymptotics become crucial in view of applications. This is the core of the paper: We provide rates of convergence for the sample versions and address the extremal behaviour of the geometric measures according to the type of underlying distribution.
Refactoring is a crucial technique for improving the efficiency and maintainability of software by restructuring its internal design while preserving its external behavior. While classical programs have benefited from various refactoring methods, the field of quantum programming lacks dedicated refactoring techniques. The distinct properties of quantum computing, such as quantum superposition, entanglement, and the no-cloning principle, necessitate specialized refactoring techniques. This paper bridges this gap by presenting a comprehensive set of refactorings specifically designed for quantum programs. Each refactoring is carefully designed and explained to ensure the effective restructuring of quantum programs. Additionally, we highlight the importance of tool support in automating the refactoring process for quantum programs. Although our study focuses on the quantum programming language Q\#, our approach is applicable to other quantum programming languages, offering a general solution for enhancing the maintainability and efficiency of quantum software.
Semantic representation is a key enabler for several application domains, and the multi-agent systems realm makes no exception. Among the methods for semantically representing agents, one has been essentially achieved by taking a behaviouristic vision, through which one can describe how they operate and engage with their peers. The approach essentially aims at defining the operational capabilities of agents through the mental states related with the achievement of tasks. The OASIS ontology -- An Ontology for Agent, Systems, and Integration of Services, presented in 2019 -- pursues the behaviouristic approach to deliver a semantic representation system and a communication protocol for agents and their commitments. This paper reports on the main modeling choices concerning the representation of agents in OASIS 2, the latest major upgrade of OASIS, and the achievement reached by the ontology since it was first introduced, in particular in the context of ontologies for blockchains.
Bid optimization for online advertising from single advertiser's perspective has been thoroughly investigated in both academic research and industrial practice. However, existing work typically assume competitors do not change their bids, i.e., the wining price is fixed, leading to poor performance of the derived solution. Although a few studies use multi-agent reinforcement learning to set up a cooperative game, they still suffer the following drawbacks: (1) They fail to avoid collusion solutions where all the advertisers involved in an auction collude to bid an extremely low price on purpose. (2) Previous works cannot well handle the underlying complex bidding environment, leading to poor model convergence. This problem could be amplified when handling multiple objectives of advertisers which are practical demands but not considered by previous work. In this paper, we propose a novel multi-objective cooperative bid optimization formulation called Multi-Agent Cooperative bidding Games (MACG). MACG sets up a carefully designed multi-objective optimization framework where different objectives of advertisers are incorporated. A global objective to maximize the overall profit of all advertisements is added in order to encourage better cooperation and also to protect self-bidding advertisers. To avoid collusion, we also introduce an extra platform revenue constraint. We analyze the optimal functional form of the bidding formula theoretically and design a policy network accordingly to generate auction-level bids. Then we design an efficient multi-agent evolutionary strategy for model optimization. Offline experiments and online A/B tests conducted on the Taobao platform indicate both single advertiser's objective and global profit have been significantly improved compared to state-of-art methods.
Promoting behavioural diversity is critical for solving games with non-transitive dynamics where strategic cycles exist, and there is no consistent winner (e.g., Rock-Paper-Scissors). Yet, there is a lack of rigorous treatment for defining diversity and constructing diversity-aware learning dynamics. In this work, we offer a geometric interpretation of behavioural diversity in games and introduce a novel diversity metric based on \emph{determinantal point processes} (DPP). By incorporating the diversity metric into best-response dynamics, we develop \emph{diverse fictitious play} and \emph{diverse policy-space response oracle} for solving normal-form games and open-ended games. We prove the uniqueness of the diverse best response and the convergence of our algorithms on two-player games. Importantly, we show that maximising the DPP-based diversity metric guarantees to enlarge the \emph{gamescape} -- convex polytopes spanned by agents' mixtures of strategies. To validate our diversity-aware solvers, we test on tens of games that show strong non-transitivity. Results suggest that our methods achieve much lower exploitability than state-of-the-art solvers by finding effective and diverse strategies.
The concept of smart grid has been introduced as a new vision of the conventional power grid to figure out an efficient way of integrating green and renewable energy technologies. In this way, Internet-connected smart grid, also called energy Internet, is also emerging as an innovative approach to ensure the energy from anywhere at any time. The ultimate goal of these developments is to build a sustainable society. However, integrating and coordinating a large number of growing connections can be a challenging issue for the traditional centralized grid system. Consequently, the smart grid is undergoing a transformation to the decentralized topology from its centralized form. On the other hand, blockchain has some excellent features which make it a promising application for smart grid paradigm. In this paper, we have an aim to provide a comprehensive survey on application of blockchain in smart grid. As such, we identify the significant security challenges of smart grid scenarios that can be addressed by blockchain. Then, we present a number of blockchain-based recent research works presented in different literatures addressing security issues in the area of smart grid. We also summarize several related practical projects, trials, and products that have been emerged recently. Finally, we discuss essential research challenges and future directions of applying blockchain to smart grid security issues.