United Kingdom

This is a short version of &#39;&#39;Logic-based specification and verification of homogeneous dynamic multi-agent systems&#39;&#39; in Autonomous Agents and Multi-Agent Systems 34, 2 (2020), where we developed a logic-based framework for formal specification and algorithmic verification of homogeneous and dynamic concurrent multi-agent transition systems (HDMAS). Homogeneity means that all agents have the same available actions at any given state and the actions have the same effects regardless of which agents perform them. Dynamicity means that the numbers of controllable and uncontrollable agents may vary throughout the system evolution, possibly at every transition. As a specification language, we extended Alternating-time Temporal Logic to express properties such as: &quot;a coalition of (at least) &lt;i&gt;n&lt;/i&gt; controllable agents can ensure against (at most) &lt;i&gt;m&lt;/i&gt; uncontrollable agents that any possible evolution of the system satisfies a given objective &amp;#947;&quot;, where &amp;#947; is specified again as a formula of that language and each of &lt;i&gt;n&lt;/i&gt; and &lt;i&gt;m&lt;/i&gt; is either a fixed number or a variable that can be quantified over. Finally, we show the algorithm and worst-case complexity for the model checking problem.

AAMAS 2021

Logic-based Specification and Verification of Homogeneous Dynamic Multi-agent Systems (JAAMAS Track)

AAMAS is the largest and most influential conference in the area of agents and multiagent systems, bringing together researchers and practitioners in all areas of agent technology and providing and internationally renowned high-profile forum for publishing and finding out about the latest developments in the field. AAMAS is the flagship conference of the non-profit International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS).  

![](https://assets.underline.io/uploads/markdown_image/1/image/ce4604bd54468a006164d16e080204fb.jpg)

Please click on the button below to register for this event.

If you are registered and see this page please check the account email you are logged in with. It must be the same as for the registration.

If you still have trouble accessing the contact please contact support at aamas2021@underline.io 

This is a short version of ''Logic-based specification and verification of homogeneous dynamic multi-agent systems'' in Autonomous Agents and Multi-Agent Systems 34, 2 (2020), where we developed a logic-based framework for formal specification and algorithmic verification of homogeneous and dynamic concurrent multi-agent transition systems (HDMAS). Homogeneity means that all agents have the same available actions at any given state and the actions have the same effects regardless of which agents perform them. Dynamicity means that the numbers of controllable and uncontrollable agents may vary throughout the system evolution, possibly at every transition. As a specification language, we extended Alternating-time Temporal Logic to express properties such as: "a coalition of (at least) n controllable agents can ensure against (at most) m uncontrollable agents that any possible evolution of the system satisfies a given objective &#947;", where &#947; is specified again as a formula of that language and each of n and m is either a fixed number or a variable that can be quantified over. Finally, we show the algorithm and worst-case complexity for the model checking problem.

technical paper

We present an ascending-price mechanism for a multi-sided market with a variety of participants, such as manufacturers, logistics agents, insurance providers, and assemblers. Each deal in the market may consist of a combination of agents from separate categories, and different such combinations are simultaneously allowed. This flexibility lets multiple intersecting markets be resolved as a single global market. Our mechanism is obviously-truthful, strongly budget-balanced, individually rational, and attains almost the optimal gain-from-trade when the market is sufficiently large.

A Global Multi-Sided Market with Ascending-Price Mechanism

Recent reinforcement learning studies extensively explore the interplay between cooperative and competitive behaviour in mixed environments. Unlike cooperative environments where agents strive towards a common goal, mixed environments are notorious for the conflicts of selfish and social interests. As a consequence, purely rational agents often struggle to maintain cooperation. A prevalent approach to induce cooperative behaviour is to assign additional rewards based on other agents' well-being. However, this approach suffers from the issue of multi-agent credit assignment, which can hinder performance. This issue is efficiently alleviated in cooperative setting with such state-of-the-art algorithms as QMIX and COMA. Still, when applied to mixed environments, these algorithms may result in unfair allocation of rewards. We propose BAROCCO, an extension of these algorithms capable to balance individual and social incentives. The mechanism behind BAROCCO is to train two distinct but interwoven components that jointly affect agents' decisions. We experimentally confirm the advantages of BAROCCO.

Balancing Rational and Other-Regarding Preferences in Cooperative-Competitive Environments

Blockchain-based Distributed Ledgers (DLs) promise to transform the existing financial system by making it truly democratic. In the past decade, blockchain technology has seen many novel applications ranging from the banking industry to real estate. However, in order to be adopted universally, blockchain systems must be scalable to support a high volume of transactions. As we increase the throughput of the DL system, the underlying peer-to-peer network might face multiple levels of challenges to keep up with the requirements. Due to varying network capacities, the slower nodes would be at a relative disadvantage compared to the faster ones, which could negatively impact their revenue. In order to quantify their relative advantage or disadvantage, we introduce two measures of network fairness, $p_f$, the probability of frontrunning and α_f$, the publishing fairness. We show that as we scale the blockchain, both these measures deteriorate, implying that the slower nodes face a disadvantage at higher throughputs. It results in the faster nodes getting more than their fair share of the reward while the slower nodes (slow in terms of network quality) get less. Thus, fairness and scalability in blockchain systems do not go hand in hand.

We might walk together, but I run faster: Network Fairness and Scalability in Blockchains

In this paper, we propose solid semantics  to obtain the most acceptable sets of arguments. Besides, we study the application of solid semantics in the field of judgement aggregation.

Solid Semantics and Extension Aggregation Using Quota Rules under Integrity Constraints

We present a novel model-based algorithm, Cooperative Prioritized Sweeping, for sample-efficient learning in large multi-agent Markov decision processes. Our approach leverages domain knowledge about the structure of the problem in the form of a dynamic decision network. Using this information, our method learns a model of the environment to determine which state-action pairs are the most likely in need to be updated, significantly increasing learning speed. Batch updates can then be performed which efficiently back-propagate knowledge throughout the value function. Our method outperforms the state-of-the-art sparse cooperative Q-learning and QMIX  algorithms, both on the well-known SysAdmin benchmark, randomized environments and a fully-observable variation of the well-known firefighter benchmark from Dec-POMDP literature.

Cooperative Prioritized Sweeping

Investors try to predict returns of financial assets to make successful investment. Many quantitative analysts have used machine learning-based methods to find unknown profitable market rules from large amounts of market data. However, there are several challenges in financial markets hindering practical applications of machine learning-based models. First, in financial markets, there is no single model that can consistently make accurate prediction because traders in markets quickly adapt to newly available information. Instead, there are a number of ephemeral and partially correct models called "alpha factors". Second, since financial markets are highly uncertain, ensuring interpretability of prediction models is quite important to make reliable trading strategies. To overcome these challenges, we propose the Trader-Company method, a novel evolutionary model that mimics the roles of a financial institute and traders belonging to it. Our method predicts future stock returns by aggregating suggestions from multiple weak learners called Traders. A Trader holds a collection of simple mathematical formulae, each of which represents a candidate of an alpha factor and would be interpretable for real-world investors. The aggregation algorithm, called a Company, maintains multiple Traders. By randomly generating new Traders and retraining them, Companies can efficiently find financially meaningful formulae whilst avoiding overfitting to a transient state of the market. We show the effectiveness of our method by conducting experiments on real market data.

Trader-Company Method: A Metaheuristics for Interpretable Stock Price Prediction

We present a general framework for modelling and verifying epistemic properties over parameterized multi-agent systems that communicate by truthful public announcements. In our framework, the number of agents or the amount of certain resources are parameterized (i.e. not known a priori), and the corresponding verification problem asks whether a given epistemic property is true regardless of the instantiation of the parameters. For example, in a muddy children puzzle, one could ask whether each child will eventually find out whether (s)he is muddy, regardless of the number of children.  Our framework is regular model checking (RMC)-based, wherein synchronous finite-state automata (equivalently, monadic second-order logic over words) are used to specify the systems. We propose an extension of public announcement logic as specification language. Of special interests is the addition of the so-called iterated public announcement operators, which are crucial for reasoning about knowledge in parameterized systems. Although the operators make the model checking problem undecidable, we show that this becomes decidable when an appropriate "disappearance relation" is given. Further, we show how Angluin's L*-algorithm for learning finite automata can be applied to find a disappearance relation, which is guaranteed to terminate if it is regular. We have implemented the algorithm and apply this to such examples as the Muddy Children Puzzle, the Russian Card Problem, and Large Number Challenge.

Regular Model Checking Approach to Knowledge Reasoning over Parameterized Systems

Studying adversarial attacks on Reinforcement Learning (RL) agents has become a key aspect of developing robust, RL-based solutions. Test-time attacks, which target the post-learning performance of an RL agent's policy, have been well studied in both white- and black-box settings. More recently, however, state-of-the-art works have shifted to investigate training-time attacks on RL agents, i.e., forcing the learning process towards a target policy designed by the attacker. Alas, these SOTA works continue to rely on white-box settings and/or use a reward-poisoning approach. In contrast, this paper studies environment-dynamics poisoning attacks at training time. Furthermore, while environment-dynamics poisoning presumes a transfer-learning capable agent, it also allows us to expand our approach to black-box attacks. Our overall framework, inspired by hierarchical RL, seeks the minimal environment-dynamics manipulation that will prompt the momentary policy of the agent to change in a desired manner. We show the attack efficiency by comparing it with the reward-poisoning approach, and empirically demonstrate the transferability of the environment-poisoning attack strategy. Finally, we seek to exploit the transferability of the attack strategy to handle black-box settings.

Transferable Environment Poisoning: Training-time Attack on Reinforcement Learning

In this paper we introduce a generic approach to solving Sequential Security Games (SGs) based on Evolutionary Algorithms. The method (named EASG) is general and largely game-independent, which allows for its application to a wide range of SGs with only slight adjustments. The efficacy of EASG is verified on 3 types of games from different domains: patrolling, surveillance, and cybersecurity. Comprehensive experiments performed on more than $300$ test games demonstrate robustness and stability of EASG, manifested by repetitively achieving optimal or near-optimal solutions. The main advantage of EASG compared to alternative approaches to solving SGs is its time efficiency. EASG finds high-quality solutions with approximately linear time scalability and can therefore be applied to solving SG instances which are beyond capabilities of the state-of-the-art exact methods. Due to anytime characteristics, EASG is particularly well suited for time-critical applications.

Evolution of Strategies in Sequential Security Games

The ability of agents to learn to communicate through interaction has been studied through emergent communication tasks. Previous works in this domain have studied the linguistic properties of the emergent languages like compositionality, generalization, and as well as the environmental pressures that shape them. However, most of these experiments require a considerable amount of shared training time between agents to communicate successfully. Our work highlights the problem of sample inefficiency of agents in population-based referential games and proposes an Action Advising framework to counter it.

Logic-based Specification and Verification of Homogeneous Dynamic Multi-agent Systems (JAAMAS Track)

Downloads

Next from AAMAS 2021

A Global Multi-Sided Market with Ascending-Price Mechanism

Similar lecture

RPPLNS: Pay-per-last-N-shares with a Randomised Twist

Stay up to date with the latest Underline news!

PRESENTATIONS

CONFERENCES

COMPANY

RESOURCES

Logic-based Specification and Verification of Homogeneous Dynamic Multi-agent Systems (JAAMAS Track)

.css-70qvj9{display:-webkit-box;display:-webkit-flex;display:-ms-flexbox;display:flex;-webkit-align-items:center;-webkit-box-align:center;-ms-flex-align:center;align-items:center;}Downloads

Next from AAMAS 2021

A Global Multi-Sided Market with Ascending-Price Mechanism

Similar lecture

RPPLNS: Pay-per-last-N-shares with a Randomised Twist

Stay up to date with the latest Underline news!

PRESENTATIONS

CONFERENCES

COMPANY

RESOURCES

Downloads