Reward machines have recently been proposed as a means of encoding team tasks in cooperative multi-agent reinforcement learning. The resulting multi-agent reward machine is then decomposed into individual reward machines, one for each member of the team, allowing agents to learn in a decentralised manner while still achieving the team task. In this paper, we show how multi-agent reward machines for team tasks can be synthesised automatically from an abstraction of the environment in which the agents act and a high-level specification of the desired team behaviour expressed in a fragment of Alternating-time Temporal Logic. We present results from a number of benchmarks which suggest that our automated approach performs as well or better than reward machines in the literature.

Structural equation models (SEM) are a standard approach to representing causal dependencies between variables. In this paper we propose a new interpretation of existing formalisms in the field of Actual Causality in which SEM's are viewed as mechanisms transforming the dynamics of exogenous variables into the dynamics of endogenous variables. This allows us to combine counterfactual causal reasoning with existing temporal logic formalizms, and to introduce a temporal logic, CPLTL, for causal reasoning about such structures. Then, we demonstrate that the standard restriction to so-called recursive models (with no cycles in the dependency graphs) is not necessary in our approach. This fact provides us extra tools for reasoning about mutually dependent processes and feedback loops. Finally, we introduce the notions of model equivalence for temporal causal models and show that CPLTL has an efficient model-checking procedure.

There has been considerable work on reasoning about the strategic ability of agents under imperfect information. However, existing logics such as Probabilistic Strategy Logic are unable to express properties relating to information transparency. Information transparency concerns the extent to which agents' behaviours and actions are observable by other agents. Reasoning about information transparency is useful in many domains including security, privacy, and decision-making. In this paper, we present a formal framework for reasoning about information transparency properties in stochastic multi-agent systems. We extend Probabilistic Strategy Logic with new observability operators that capture the degree of observability of temporal properties by agents. We show that the model checking problem for the resulting logic is decidable.

A key problem in the design of normative multi-agent systems is the cost of enforcing a norm (for the system operator) or complying with the norm (for the system users). If the cost is too high, ensuring compliant behavior may be uneconomic, or users may be deterred from participating in the MAS. In this paper, we consider the problem of synthesizing minimum cost dynamic norms to satisfy a system-level objective specified in Alternating Time Temporal Logic with Strategy Contexts (ATLsc∗). We show that synthesizing a dynamic norm under a bound on the cost of any prohibited set of actions has the same complexity as synthesizing arbitrary norms. We also show that synthesizing norms that minimize the average cost of the prohibited set of actions is unsolvable; however, synthesizing ε-optimal norms is possible.

Reward machines (RMs) are automata structures that encode (non-Markovian) reward functions for reinforcement learning (RL). RMs can reward any behaviour representable in regular languages and, when paired with RL algorithms that exploit RM structure, have been shown to significantly improve sample efficiency in many domains. In this work, we present pushdown reward machines (pdRMs), an extension of reward machines based on deterministic pushdown automata. pdRMs can recognise and reward temporally extended behaviours representable in deterministic context-free languages, making them more expressive than reward machines. We introduce two variants of pdRM-based policies, one which has access to the entire stack of the pdRM, and one which can only access the top k symbols (for a given constant k) of the stack. We propose a procedure to check when the two kinds of policies (for a given environment, pdRM, and constant k) achieve the same optimal state values. We then provide theoretical results establishing the expressive power of pdRMs, and space complexity results for the proposed learning problems. Lastly, we propose an approach for off-policy RL algorithms that exploits counterfactual experiences with pdRMs. We conclude by providing experimental results showing how agents can be trained to perform tasks representable in deterministic context-free languages using pdRMs.

Autonomous systems use independent decision-making with only limited human intervention to accomplish goals in complex and unpredictable environments. As the autonomy technologies that underpin them continue to advance, these systems will find their way into an increasing number of applications in an ever wider range of settings. If we are to deploy them to perform safety-critical or mission-critical roles, it is imperative that we have justified confidence in their safe and correct operation. Verification is a key process for establishing such confidence. However, autonomous systems pose challenges to existing verification practices. This paper highlights viewpoints of the Roadmap Working Group of the IEEE Robotics and Automation Society Technical Committee for Verification of Autonomous Systems, identifying these grand challenges, and providing a vision for future research efforts that will be needed to address them.

We present Pure-Past Action Masking (PPAM), a lightweight approach to action masking for safe reinforcement learning. In PPAM, actions are disallowed (“masked”) according to specifications expressed in Pure-Past Linear Temporal Logic (PPLTL). PPAM can enforce non-Markovian constraints, i.e., constraints based on the history of the system, rather than just the current state of the (possibly hidden) MDP. The features used in the safety constraint need not be the same as those used by the learning agent, allowing a clear separation of concerns between the safety constraints and reward specifications of the (learning) agent. We prove formally that an agent trained with PPAM can learn any optimal policy that satisfies the safety constraints, and that they are as expressive as shields, another approach to enforce non-Markovian constraints in RL. Finally, we provide empirical results showing how PPAM can guarantee constraint satisfaction in practice.

Reward machines allow the definition of rewards for temporally extended tasks and behaviors. Specifying “informative” reward machines can be challenging. One way to address this is to generate reward machines from a high-level abstract description of the learning environment, using techniques such as AI planning. However, previous planning-based approaches generate a reward machine based on a single (sequential or partial-order) plan, and do not allow maximum flexibility to the learning agent. In this paper we propose a new approach to synthesising reward machines which is based on the set of partial order plans for a goal. We prove that learning using such “maximally permissive” reward machines results in higher rewards than learning using RMs based on a single plan. We present experimental results which support our theoretical claims by showing that our approach obtains higher rewards than the single-plan approach in practice.

Abstract Synthetic populations are representations of actual individuals living in a specific area. They play an increasingly important role in studying and modeling individuals and are often used to build agent-based social simulations. Traditional approaches for synthesizing populations use a detailed sample of the population (which may not be available) or combine data into a single joint distribution, and draw individuals or households from these. The latter group of existing sample-free methods fail to integrate (1) the best available data on spatial granular distributions, (2) multi-variable joint distributions, and (3) household level distributions. In this paper, we propose a sample-free approach where synthetic individuals and households directly represent the estimated joint distribution to which attributes are iteratively added, conditioned on previous attributes such that the relative frequencies within each joint group of attributes are maintained and fit granular spatial marginal distributions. In this paper we present our method and test it for the Zuid-West district of The Hague, the Netherlands, showing that spatial, multi-variable and household distributions are accurately reflected in the resulting synthetic population.

There have been a number of attempts to develop a formal definition of causality that accords with our intuitions about what constitutes a cause. Perhaps the best known is the “modified” definition of actual causality, HPm, due to Halpern. In this paper, we argue that HPm gives counterintuitive results for some simple causal models. We propose Dynamic Causality (DC), an alternative semantics for causal models that leads to an alternative definition of causes. DC ascribes the same causes as HPm on the examples of causal models widely discussed in the literature and ascribes intuitive causes for the kinds of causal models we consider. Moreover, we show that the complexity of determining a cause under the DC definition is lower than for the HPm definition.

Reward machines have recently been proposed as a means of encoding team tasks in cooperative multi-agent reinforcement learning. The resulting multi-agent reward machine is then decomposed into individual reward machines, one for each member of the team, allowing agents to learn in a decentralised manner while still achieving the team task. In this paper, we show how multi-agent reward machines for team tasks can be synthesised automatically from an abstraction of the environment in which the agents act and a high-level specification of the desired team behaviour expressed in a fragment of Alternating-time Temporal Logic. We present results from a number of benchmarks which suggest that our automated approach performs as well or better than reward machines in the literature.

For an agent in a multi-agent environment, it is often beneficial to be able to predict what other agents will do next when deciding how to act. Previous work in multi-agent intention scheduling assumes a priori knowledge of the current goals of other agents. In this paper, we present a new approach to multi-agent intention scheduling in which an agent uses online goal recognition to identify the goals currently being pursued by other agents while acting in pursuit of its own goals. We show how online goal recognition can be incorporated into an MCTS-based intention scheduler, and evaluate our approach in a range of scenarios. The results demonstrate that our approach can rapidly recognise the goals of other agents even when they are pursuing multiple goals concurrently, and has similar performance to agents which know the goals of other agents a priori.

In multi-agent systems, norm enforcement is a mechanism for steering the behavior of individual agents in order to achieve desired system-level objectives. Due to the dynamics of multi-agent systems, however, it is hard to design norms that guarantee the achievement of the objectives in every operating context. Also, these objectives may change over time, thereby making previously defined norms ineffective. In this paper, we investigate the use of system execution data to automatically synthesise and revise conditional prohibitions with deadlines, a type of norms aimed at preventing agents from exhibiting certain patterns of behaviors. We propose DDNR (Data-Driven Norm Revision), a data-driven approach to norm revision that synthesises revised norms with respect to a data set of traces describing the behavior of the agents in the system. We evaluate DDNR using a state-of-the-art, off-the-shelf urban traffic simulator. The results show that DDNR synthesises revised norms that are significantly more accurate than the original norms in distinguishing adequate and inadequate behaviors for the achievement of the system-level objectives.

To build a theory of intention revision for agents operating in stochastic environments, we need a logic in which we can explicitly reason about their decision-making policies and those policies' uncertain outcomes. Towards this end, we propose PLBP, a novel probabilistic temporal logic for Markov Decision Processes that allows us to reason about policies of bounded size. The logic is designed so that its expressive power is sufficient for the intended applications, whilst at the same time possessing strong computational properties. We prove that the satisfiability problem for our logic is decidable, and that its model checking problem is PSPACE-complete. This allows us to e.g. algorithmically verify whether an agent's intentions are coherent, or whether a specific policy satisfies safety and/or liveness properties.

We propose a logic of east and west (LEW ) for points in 1D Euclidean space. It formalises primitive direction relations: east (E), west (W) and indeterminate east/west (Iew). It has a parameter τ ∈ N>1, which is referred to as the level of indeterminacy in directions. For every τ ∈ N>1, we provide a sound and complete axiomatisation of LEW , and prove that its satisfiability problem is NP-complete. In addition, we show that the finite axiomatisability of LEW depends on τ : if τ = 2 or τ = 3, then there exists a finite sound and complete axiomatisation; if τ > 3, then the logic is not finitely axiomatisable. LEW can be easily extended to higher-dimensional Euclidean spaces. Extending LEW to 2D Euclidean space makes it suitable for reasoning about not perfectly aligned representations of the same spatial objects in different datasets, for example, in crowd-sourced digital maps.

Recent work in multi-agent intention scheduling has shown that enabling agents to predict the actions of other agents when choosing their own actions can be beneficial. However existing approaches to 'intention-aware' scheduling assume that the programs of other agents are known, or are "similar" to that of the agent making the prediction. While this assumption is reasonable in some circumstances, it is less plausible when the agents are not co-designed. In this paper, we present a new approach to multi-agent intention scheduling in which agents predict the actions of other agents based on a high-level specification of the tasks performed by an agent in the form of a reward machine (RM) rather than on its (assumed) program. We show how a reward machine can be used to generate tree and rollout policies for an MCTS-based scheduler. We evaluate our approach in a range of multi-agent environments, and show that RM-based scheduling out-performs previous intention-aware scheduling approaches in settings where agents are not co-designed

Manufacturing is transitioning from a mass production model to a service model in which facilities `bid' for previously unseen products. To decide whether to bid for a previously unseen product, a facility must be able to synthesize, on the fly, a process plan controller that delegates abstract manufacturing tasks in a supplied process recipe to the available manufacturing resources. First-order representations of the state are commonly considered in reasoning about action in AI. Here we show that we can leverage the wide literature on the Situation Calculus automatically synthesize such controllers. We identify two important decidable cases---finite domains and bounded action theories---for which we provide practical synthesis techniques.

In multi-agent systems, norm enforcement is a mechanism for steering the behavior of individual agents in order to achieve desired system-level objectives. Due to the dynamics of multi-agent systems, however, it is hard to design norms that guarantee the achievement of the objectives in every operating context. Also, these objectives may change over time, thereby making previously defined norms ineffective. In this paper, we investigate the use of system execution data to automatically synthesise and revise conditional prohibitions with deadlines, a type of norms aimed at prohibiting agents from exhibiting certain patterns of behaviors. We propose DDNR (Data-Driven Norm Revision), a data-driven approach to norm revision that synthesises revised norms with respect to a data set of traces describing the behavior of the agents in the system. We evaluate DDNR using a state-of-the-art, off-the-shelf urban traffic simulator. The results show that DDNR synthesises revised norms that are significantly more accurate than the original norms in distinguishing adequate and inadequate behaviors for the achievement of the system-level objectives.

We propose a new approach to intention progression in multi-agent settings where other agents are effectively black boxes. That is, while their goals are known, the precise programs used to achieve these goals are not known. In our approach, agents use an abstraction of their own program called a partially-ordered goal-plan tree (pGPT) to schedule their intentions and predict the actions of other agents. We show how a pGPT can be derived from the program of a BDI agent, and present an approach based on Monte Carlo Tree Search (MCTS) for scheduling an agent's intentions using pGPTs. We evaluate our pGPT-based approach in cooperative, selfish and adversarial multi-agent settings, and show that it out-performs MCTS-based scheduling where agents assume that other agents have the same program as themselves.

It is often advantageous to be able to extract resource requirements in resource logics of strategic ability, rather than to verify whether a fixed resource requirement is sufficient for achieving a goal. We study Parameterised Resource-Bounded Alternating Time Temporal Logic where parameter extraction is possible. We give a parameter extraction algorithm and prove that the model-checking problem is 2EXPTIME-complete.

A key problem in Belief-Desire-Intention agents is how an agent progresses its intentions, i.e., which plans should be selected and how the execution of these plans should be interleaved so as to achieve the agent’s goals. Previous approaches to the intention progression problem assume the agent has perfect information about the state of the environment. However, in many real-world applications, an agent may be uncertain about whether an environment condition holds, and hence whether a particular plan is applicable or an action is executable. In this paper, we propose SAU, a Monte-Carlo Tree Search (MCTS)-based scheduler for intention progression problems where the agent’s beliefs are uncertain. We evaluate the performance of our approach experimentally by varying the degree of uncertainty in the agent’s beliefs. The results suggest that SAU is able to successfully achieve the agent’s goals even in settings where there is significant uncertainty in the agent’s beliefs.

The BDI model forms the basis of much of the research on symbolic models of agency and agent-oriented software engineering. While many variants of the basic BDI model have been proposed in the literature, there has been no systematic review of research on BDI agent architectures in over 10 years. In this paper, we survey the main approaches to each component of the BDI architecture, how these have been realised in agent programming languages, and discuss the trade-offs inherent in each approach.

There has recently been increasing interest in using reactive synthesis techniques to automate the production of manufacturing process plans. Previous work has assumed that the set of manufacturing resources is known and fixed in advance. In this paper, we consider the more general problem of whether a controller can be synthesized given sufficient resources. In the unbounded setting, only the types of available manufacturing resources are given, and we want to know whether it is possible to manufacture a product using only resources of those type(s), and, if so, how many resources of each type are needed. We model manufacturing processes and facilities as transducers (automata with output), and show that the unbounded orchestration problem is decidable and the (Pareto) optimal set of resources necessary to manufacture a product is computable for uni-transducers. However, for multitransducers, the problem is undecidable.

In this paper, we model manufacturing processes and facilities as transducers (automata with output). The problem of whether a given manufacturing process can be realized by a given set of manufacturing resources can then be stated as an orchestration problem for transducers. We first consider the conceptually simpler case of uni-transducers (transducers with a single input and a single output port), and show that synthesizing orchestrations for uni-transducers is EXPTIME-complete. Surprisingly, the complexity remains the same for the more expressive multi-transducer case, where transducers have multiple input and output ports and the orchestration is in charge of dynamically connecting ports during execution.

We consider the problem of detecting norm violations in open multi-agent systems (MAS). In this extended abstract, we outline the approach of [Alechina et al., 2018], and show how, using ideas from scrip systems, we can design mechanisms where the agents comprising the MAS are incentivised to monitor the actions of other agents for norm violations.

The Procedural Reasoning System (PRS) is arguably the first implementation of the Belief--Desire--Intention (BDI) approach to agent programming. PRS remains extremely influential, directly or indirectly inspiring the development of subsequent BDI agent programming languages. However, perhaps surprisingly given its centrality in the BDI paradigm, PRS lacks a formal operational semantics, making it difficult to determine its expressive power relative to other agent programming languages. This paper takes a first step towards closing this gap, by giving a formal semantics for a significant fragment of PRS. We prove key properties of the semantics relating to PRS-specific programming constructs, and show that even the fragment of PRS we consider is strictly more expressive than the plan constructs found in typical BDI languages.

A key advantage of BDI-based approaches to agent programming, is that agents can deliberate about which course of action to adopt to achieve a goal or respond to an event. However, while state-of-the-art BDI-based agent programming languages allow the programmer to specify the context(s) in which a particular plan is applicable, they are typically limited to a single, hardcoded, deliberation strategy for all task environments. In this paper, we present an alternative approach, in which an agent’s deliberation strategy forms part of the agent program. We show how both conventional agent programs and the agent’s deliberation strategy can be encoded in the agent programming language meta-APL. Key steps in the deliberation cycle of meta-APL are reflected in the state of the agent and can be queried and updated by meta-APL rules, allowing application-specific BDI deliberation strategies to be programmed in a straightforward way. To illustrate the flexibility of meta-APL, we show how three typical BDI deliberation strategies can be programmed using meta-APL rules. We then show how meta-APL can used to program a simple adaptive deliberation strategy that avoids interference between intentions.

We consider the problem of detecting norm violations in open multi-agent systems (MAS). We show how, using ideas from scrip systems, we can design mechanisms where the agents comprising the MAS are incentivised to monitor the actions of other agents for norm violations. The cost of providing the incentives is not borne by the MAS and does not come from fines charged for norm violations (fines may be impossible to levy in a system where agents are free to leave and rejoin again under a different identity). Instead, monitoring incentives come from (scrip) fees for accessing the services provided by the MAS. In some cases, perfect monitoring (and hence enforcement) can be achieved: no norms will be violated in equilibrium. In other cases, we show that, while it is impossible to achieve perfect enforcement, we can get arbitrarily close; we can make the probability of a norm violation in equilibrium arbitrarily small. We show using simulations that our theoretical results, which apply to systems with a large number of agents, hold for multi-agent systems with as few as 1000 agents–the system rapidly converges to the steady-state distribution of scrip tokens necessary to ensure monitoring and then remains close to the steady state.

In this article, we study a minimal change approach to preference dynamics. We treat a set of preferences as a special kind of theory, and define minimal change preference contraction and revision operations in the spirit of the Alchourrón, Gärdenfors, and Makinson theory of belief revision. We characterise minimal contraction of preference sets by a set of postulates and prove a representation theorem. We also give a linear time algorithm which implements minimal contraction by a single preference. We then define minimal contraction by a set of preferences, and show that the problem of a minimal contraction by a set of preferences is NP-hard.

Many problems in AI and multi-agent systems research are most naturally formulated in terms of the abilities of a coalition of agents. There exist several excellent logical tools for reasoning about coalitional ability. However, coalitional ability can be affected by the availability of resources, and there is no straightforward way of reasoning about resource requirements in logics such as Coalition Logic (CL) and Alternating-time Temporal Logic (ATL). In this article, we describe a logic for reasoning about coalitional ability under resource constraints. We extend ATL with costs of actions and hence of strategies. We give a complete and sound axiomatization of the resulting logic, Resource-Bounded ATL (RB-ATL) and a model-checking algorithm for it.

International audience

We present an approach to incentivising monitoring for norm violations in open multi-agent systems such as Wikipedia. In such systems, there is no crisp definition of a norm violation; rather, it is a matter of judgement whether an agent's behaviour conforms to generally accepted standards of behaviour. Agents may legitimately disagree about borderline cases. Using ideas from scrip systems and peer prediction, we show how to design a mechanism that incentivises agents to monitor each other's behaviour for norm violations. The mechanism keeps the probability of undetected violations (submissions that the majority of the community would consider not conforming to standards) low, and is robust against collusion by the monitoring agents.

Determining the most appropriate means of producing a given product, i.e., which manufacturing and assembly tasks need to be performed in which order and how, is termed process planning. In process planning, abstract manufacturing tasks in a process recipe are matched to available manufacturing resources, e.g., CNC machines and robots, to give an executable process plan. A process plan controller then delegates each operation in the plan to specific manufacturing resources. In this paper we present an approach to the automated computation of process plans and process plan controllers. We extend previous work to support both non-deterministic (i.e., partially controllable) resources, and to allow operations to be performed in parallel on the same part. We show how implicit fairness assumptions can be captured in this setting, and how this impacts the definition of process plans.

Alternating Time Temporal Logic (ATL) is widely used for the verification of multi-agent systems. We consider Resource Agent Logic ( RAL ), which extends ATL to allow the verification of properties of systems where agents act under resource constraints. The model checking problem for RAL with unbounded production and consumption of resources is known to be undecidable. We review existing (un)decidability results for fragments of RAL , tighten some existing undecidability results, and identify several aspects which affect decidability of model checking. One of these aspects is the availability of a ‘do nothing’, or idle action, which does not produce or consume resources. Analysis of undecidability results allows us to identify a significant new fragment of RAL for which model checking is decidable.

Several logics for expressing coalitional ability under resource bounds have been proposed and studied in the literature. Previous work has shown that if only consumption of resources is considered or the total amount of resources produced or consumed on any path in the system is bounded, then the model-checking problem for several standard logics, such as Resource-Bounded Coalition Logic (RB-CL) and Resource-Bounded Alternating-Time Temporal Logic (RB-ATL) is decidable. However, for coalition logics with unbounded resource production and consumption, only some undecidability results are known. In this paper, we show that the model-checking problem for RB-ATL with unbounded production and consumption of resources is decidable but EXPSPACE-hard. We also investigate some tractable cases and provide a detailed comparison to a variant of the resource logic RAL, together with new complexity results.

Abstract We consider the problem of decomposing a group norm into a set of individual obligations for the agents comprising the group, such that if the individual obligations are fulfilled, the group obligation is fulfilled. Such an assignment of tasks to agents is often subject to additional social or organizational norms that specify permissible ways in which tasks can be assigned. An important role of social norms is that they can be used to impose ‘fairness constraints’, which seek to distribute individual responsibility for discharging the group norm in a ‘fair’ or ‘equitable’ way. We propose a simple language for this kind of fairness constraints and analyse the problem of computing a fair decomposition of a group obligation, both for non-repeating and for repeating group obligations.

A key advantage the reactive planning approach adopted by BDI-based agents is the ability to recover from plan execution failures, and almost all BDI agent programming languages and platforms provide some form of failure handling mechanism. In general, these consist of simply choosing an alternative plan for the failed subgoal (e.g., JACK, Jadex). In this paper, we propose an alternative approach to recovering from execution failures that relies on exploiting positive interactions between an agent's intentions. A positive interaction occurs when the execution of an action in one intention assists the execution of actions in other intentions (e.g., by (re)establishing their preconditions). We have implemented our approach in a scheduling algorithm for BDI agents which we call SP. The results of a preliminary empirical evaluation of SP suggest our approach out-performs existing failure handling mechanisms used by state-of-the-art BDI languages. Moreover, the computational overhead of SP is modest.

There is a rising demand for customised products with a high degree of complexity. To meet these demands, manufacturing lines are increasingly becoming autonomous, networked, and intelligent, with production lines being virtualised into a manufacturing cloud, and advertised either internally to a company, or externally in a public cloud. In this paper, we present a novel approach to two key problems in such future manufacturing systems: the realisability problem (whether a product can be manufactured by a set of manufacturing resources) and the control problem (how a particular product should be manufactured). We show how both production recipes specifying the steps necessary to manufacture a particular product, and manufacturing resources and their topology can be formalised as labelled transition systems, and define a novel simulation relation which captures what it means for a recipe to be realisable on a production topology. We show how a controller that can orchestrate the resources in order to manufacture the product on the topology can be extracted from the simulation relation, and give an algorithm to compute a simulation relation and a controller.

No description available

We describe a tool, MatchMaps, that generates sameAs and partOf matches between spatial objects (such as shops, shopping centres, etc.) in crowd-sourced and authoritative geospatial datasets. MatchMaps uses reasoning in qualitative spatial logic, description logic and truth maintenance techniques, to produce a consistent set of matches. We report the results of an initial evaluation of MatchMaps by experts from Ordnance Survey (Great Britain’s National Mapping Authority). In both the case studies considered, MatchMaps was able to correctly match spatial objects (high precision and recall) with minimal human intervention.

Several logics for expressing coalitional ability under resource bounds have been proposed and studied in the literature. Previous work has shown that if only consumption of resources is considered or the total amount of resources produced or consumed on any path in the system is bounded, then the model-checking problem for several standard logics, such as Resource-Bounded Coalition Logic (RB-CL) and Resource-Bounded Alternating-Time Temporal Logic (RB-ATL) is decidable. However, for coalition logics with unbounded resource production and consumption, only some undecidability results are known. In this paper, we show that the model-checking problem for RB-ATL with unbounded production and consumption of resources is decidable.

In many logic-based BDI agent programming languages, plan selection involves inferencing over some underlying knowledge representation. While context-sensitive plan selection facilitates the development of flexible, declarative programs, the overhead of evaluating repeated queries to the agent's beliefs and goals can result in poor run time performance. In this paper we present an approach to multi-cycle query caching for logic-based BDI agent programming languages. We extend the abstract performance model presented in (Alechina et al. 2012) to quantify the costs and benefits of caching query results over multiple deliberation cycles. We also present results of experiments with prototype implementations of both single- and multi-cycle caching in three logic-based BDI agent platforms, which demonstrate that significant performance improvements are achievable in practice.

We present a family of sound and complete logics for reasoning about deliberation strategies for SimpleAPL programs. SimpleAPL is a fragment of the agent programming language 3APL designed for the implementation of cognitive agents with beliefs, goals and plans. The logics are variants of PDL, and allow us to prove safety and liveness properties of SimpleAPL agent programs under different deliberation strategies. We show how to axiomatise different deliberation strategies for SimpleAPL programs, and, for each strategy we prove a correspondence between the operational semantics of SimpleAPL and the models of the corresponding logic. We illustrate the utility of our approach with an example in which we show how to verify correctness properties for a simple agent program under different deliberation strategies.

Recent work on Alternating-Time Temporal Logic and Coalition Logic has allowed the expression of many interesting properties of coalitions and strategies. However, there is no natural way of expressing resource requirements in these logics. In this article, we present a Resource-Bounded Coalition Logic (RBCL) that has explicit representation of resource bounds in the language. We give a complete and sound axiomatization of RBCL, a procedure for deciding satisfiability of RBCL formulas, and a model-checking algorithm.

Abstract In previous work we presented the DTRD algorithm, an optimistic synchronization algorithm for parallel discrete event simulation of multi‐agent systems, and showed that it outperforms Time Warp and time windows on a range of test cases. DTRD uses a decision‐theoretic model of rollback to derive an optimal time to delay read event so as to maximize the rate of LVT progression. The algorithm assumes that the inter‐arrival times (both virtual and real) of events are normally distributed. In this paper we present a more detailed evaluation of the DTRD algorithm, and specifically how the performance of the algorithm is affected when the inter‐arrival times do not follow the assumed distributions. Our analysis suggests that the performance of the algorithm is relatively insensitive to events whose inter‐arrival times are not normally distributed. However, as the variance of event inter‐arrival times increases, its performance degrades to that of Time Warp. The evaluation approach we present is generally applicable, and we sketch how a similar analysis may be performed for two other decision‐theoretic optimistic synchronization algorithms. Copyright © 2009 John Wiley & Sons, Ltd.

In previous work we presented the DTRD algorithm, an optimistic synchronisation algorithm for parallel discrete event simulation of multi-agent systems, and showed that it outperforms time warp and time windows on range of test cases. DTRD uses a decision theoretic model of rollback to derive an optimal time to delay read event so as to maximise the rate of LVT progression. The algorithm assumes that the inter-arrival times (both virtual and real) of events are normally distributed. In this paper we present a more detailed evaluation of the DTRD algorithm, and specifically how the performance of the algorithm is affected when the inter-arrival times do not follow the assumed distributions. Our analysis suggests that the performance of the algorithm is relatively insensitive to events whose inter-arrival times are not normally distributed. However as the variance of the input events increases its performance degrades to that of Time Warp. Our approach to evaluation is general, and we outline how the analysis may be applied to other decision theoretic algorithms

In this paper we present a throttling mechanism for optimistic simulations of multi-agent systems, which delays read accesses to the shared simulation state that are likely to be rolled back. We develop a decision-theoretic model of rollback and show how this can be used to derive the optimal time to delay a read event so as to minimize the expected overall execution time of the simulation. We briefly describe an implementation of this approach in ASSK, a distributed simulation kernel developed to investigate synchronization mechanisms for MAS simulation, and report the results of preliminary experiments to evaluate the effectiveness of our approach.

The paper presents a load management mechanism for distributed simulations of multi-agent systems. The mechanism minimizes the cost of accessing the shared state in the distributed simulation by dynamically redistributing shared state variables according to the access pattern of the simulation model. To evaluate the effectiveness and performance of the mechanism, a series of benchmark experiments were performed using the PDES-MAS framework for distributed simulation of multi-agent systems. Although preliminary, the results indicate that the proposed mechanism significantly reduces the overall access cost of the system.

Agent based systems are increasingly being applied in a wide range of areas including telecommunications, business process modeling, computer games, control of mobile robots, and military simulations. Such systems are typically extremely complex and it is often useful to be able to simulate an agent based system to learn more about its behavior or investigate the implications of alternative architectures. The authors discuss the application of distributed discrete event simulation techniques to the simulation of multiagent systems. We identify the efficient distribution of the agents' environment as a key problem in the simulation of agent based systems and present an approach to the decomposition of the environment that facilitates load balancing.