Natasha Alechina

CLeaR Conference 2026 Conference Paper

Abstractions in Causal Models and Game Structures

• Sylvia S. Kerkhove
• Natasha Alechina
• Mehdi Dastani

We investigate abstractions in causal and strategic models of multi-agent systems, exploiting the relationship between these models. The paper contains two main results. The first one demonstrates that abstraction in causal models is a faithful correspondent of abstraction in strategic models, i. e. , for a given causal model, if we generate a corresponding strategic model and abstract this model, we will obtain the same model as when we abstract the causal model first and then generate its corresponding strategic model. The second result is that a causal dependency in an abstract (high-level) model entails a causal dependency in the original (low-level) model. This allows us to reason about causes in a simpler abstract model and derive conclusions about causality in the much larger low-level model. These results set the stage for studying and using abstractions of causal models in multi-agent settings.

AAAI Conference 2026 Conference Paper

Rational Revision of Group Intentions

• Nima Motamed
• Natasha Alechina
• Mehdi Dastani
• Dragan Doder

In systems such as group calendars or collaborative platforms, agents make group commitments to future actions that must adapt as new facts or constraints emerge. We develop a formal framework for revising such group intentions in systems where coalitions adopt shared, temporally extended intentions represented in a logic based on Alternating-Time Temporal Logic with strategy contexts. After formulating coherence criteria for systems of group intentions, we establish representation theorems in the style of Katsuno and Mendelzon, showing that revision operators satisfy rationality postulates precisely when they can be represented by preorders on strategy profiles. These results extend classical revision theory by covering non-total preorders and a logic of higher expressive power. Altogether, the framework lays the groundwork for principled revision of group intentions in systems where both coordination and change are essential.

AAMAS Conference 2026 Conference Paper

Reasoning About Responsibility for Taking Risks

• Maksim Gladyshev
• Natasha Alechina
• Mehdi Dastani
• Dragan Doder

Tracing responsibility and assigning blame to decision-making actorsinmulti-agentsystemshasdrawnattentionofMAScommunity in recent years. Existing approaches have proposed several definitions for multi-agent responsibility, but while these definitions differ in details, most of them agree that responsibility for some event may be allocated to agents only if the event is actually realized. In this paper, we argue that in many scenarios this restriction is too strong and that an undesirable outcome may be understood as a (high) risk of some event, and not necessarily as the realization of the event. To cover such cases, we propose a logical framework for reasoning about various notions of multi-agent responsibility for taking risks. The proposed logic contains primitives for probability, strategic power, time and knowledge modalities, which, as we demonstrate, allow to express various notions of group responsibility in probabilistic settings. As the main result we prove that the proposed logic has a complete axiomatization, a decidable satisfiability problem, and an efficient model-checking procedure.

JAIR Journal 2026 Journal Article

Synthesising Reward Machines for Cooperative Multi-Agent Reinforcement Learning

• Giovanni Varricchione
• Natasha Alechina
• Mehdi Dastani
• Brian Logan

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.

AAMAS Conference 2025 Conference Paper

Causes and Strategies in Multiagent Systems

• Sylvia S. Kerkhove
• Natasha Alechina
• Mehdi Dastani

Causality plays an important role in daily processes, human reasoning, and artificial intelligence. There has however not been much research on causality in multi-agent strategic settings. In this work, we introduce a systematic way to build a multi-agent system model, represented as a concurrent game structure, for a given structural causal model. In the obtained so-called causal concurrent game structure, transitions correspond to interventions on agent variables of the given causal model. The Halpern and Pearl framework of causality is used to determine the effects of a certain value for an agent variable on other variables. The causal concurrent game structure allows us to analyse and reason about causal effects of agents’ strategic decisions. We formally investigate the relation between causal concurrent game structures and the original structural causal models.

ECAI Conference 2025 Conference Paper

Contributions to the ECAI-2025 Journal Track

• Natasha Alechina
• Esra Erdem 0001

The journal track of the 28th European Conference on Artificial Intelligence (ECAI-2025) offered the authors of papers recently accepted for publication by either one of the two leading discipline-wide journals in AI, Artificial Intelligence (AIJ) and the Journal of Artificial Intelligence Research (JAIR), the opportunity to present their work at the conference without undergoing an additional round of reviewing. Papers were eligible only if no part had previously been presented at a conference with archival proceedings. Traditionally, the authors of such papers would have missed out on the opportunity to present their work to a broader research audience. This limitation tends to discourage the submission of original work to journals without prior conference publications on the same topic. The intention of the journal track is to encourage a “journal-first” publication strategy–by giving authors the option to present their work at a suitable conference venue such as ECAI. On the following pages, for each paper presented at the journal track, we provide the DOI and the abstract of the original publication.

AAAI Conference 2025 Conference Paper

Probabilistic Strategy Logic with Degrees of Observability

• Chunyan Mu
• Nima Motamed
• Natasha Alechina
• Brian Logan

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.

KR Conference 2025 Conference Paper

Pushdown Reward Machines for Reinforcement Learning

• Giovanni Varricchione
• Toryn Q. Klassen
• Natasha Alechina
• Mehdi Dastani
• Brian Logan
• Sheila A. McIlraith

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.

I&C Journal 2025 Journal Article

Reasoning about group responsibility for exceeding risk threshold in one-shot games

• Maksim Gladyshev
• Natasha Alechina
• Mehdi Dastani
• Dragan Doder

Tracing and analysing the responsibility for unsafe outcomes of actors' decisions in multi-agent settings have been studied in recent years. These studies often focus on deterministic scenarios and assume that the unsafe outcomes for which actors can be held responsible are actually realized. This paper considers a broader notion of responsibility where unsafe outcomes are not necessarily realized, but their probabilities are unacceptably high. We present a logic combining strategic, probabilistic and temporal primitives designed to express concepts such as the risk of an undesirable outcome and being responsible for exceeding a risk threshold in one-shot games. We demonstrate that the proposed logic is (weakly) complete, decidable and has an efficient model-checking procedure. Finally, we define a probabilistic notion of responsibility and study its formal properties in the proposed logic setting.

OVERLAY Workshop 2025 Workshop Paper

Run-time verification of robot-assisted surgery using visual input

• Kristina Gogoladze
• Romy van Jaarsveld
• Natasha Alechina
• Ronald de Jong
• Yasmina Al Khalil
• Gino Kuiper
• Brian Logan
• Jelle P. Ruurda

AAAI Conference 2025 Conference Paper

Temporal Causal Reasoning with (Non-Recursive) Structural Equation Models

• Maksim Gladyshev
• Natasha Alechina
• Mehdi Dastani
• Dragan Doder
• Brian Logan

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.

IJCAI Conference 2024 Conference Paper

Intention Progression with Temporally Extended Goals

• Yuan Yao
• Natasha Alechina
• Brian Logan

The Belief-Desire-Intention (BDI) approach to agent development has formed the basis for much of the research on architectures for autonomous agents. A key advantage of the BDI approach is that agents may pursue multiple intentions in parallel. However, previous approaches to managing possible interactions between concurrently executing intentions are limited to interactions between simple achievement goals (and in some cases maintenance goals). In this paper we present a new approach to intention progression for agents with temporally extended goals which allow mixing reachability and invariant properties, e. g. , ``travel to location A while not exceeding a gradient of 5%''. Temporally extended goals may be specified at run-time (top-level goals), and as subgoals in plans. In addition, our approach allows human-authored plans and plans implemented as RL policies to be freely mixed in an agent program, allowing the development of agents with `neuro-symbolic' architectures.

ECAI Conference 2024 Conference Paper

Maximally Permissive Reward Machines

• Giovanni Varricchione
• Natasha Alechina
• Mehdi Dastani
• Brian Logan 0001

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.

AAAI Conference 2024 Conference Paper

Pure-Past Action Masking

• Giovanni Varricchione
• Natasha Alechina
• Mehdi Dastani
• Giuseppe De Giacomo
• Brian Logan
• Giuseppe Perelli

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.

IJCAI Conference 2024 Conference Paper

Revising Beliefs and Intentions in Stochastic Environments

• Nima Motamed
• Natasha Alechina
• Mehdi Dastani
• Dragan Doder

The development of autonomous agents operating in dynamic and stochastic environments requires theories and models of how beliefs and intentions are revised while taking their interplay into account. In this paper, we initiate the study of belief and intention revision in stochastic environments, where an agent's beliefs and intentions are specified in a decidable probabilistic temporal logic. We then provide general Katsuno & Mendelzon-style representation theorems for both belief and intention revision, giving clear semantic characterizations of revision methods.

JAIR Journal 2023 Journal Article

A Logic of East and West

• Heshan Du
• Natasha Alechina
• Amin Farjudian
• Brian Logan
• Can Zhou
• Anthony G. Cohn

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.

IJCAI Conference 2023 Conference Paper

Data-Driven Revision of Conditional Norms in Multi-Agent Systems (Extended Abstract)

• Davide Dell'Anna
• Natasha Alechina
• Fabiano Dalpiaz
• Mehdi Dastani
• Brian Logan

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.

ECAI Conference 2023 Conference Paper

Dynamic Causality

• Maksim Gladyshev
• Natasha Alechina
• Mehdi Dastani
• Dragan Doder
• Brian Logan 0001

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.

KR Conference 2023 Conference Paper

Group Responsibility for Exceeding Risk Threshold

• Maksim Gladyshev
• Natasha Alechina
• Mehdi Dastani
• Dragan Doder

The need for tools and techniques to formally analyze and trace the responsibility for unsafe outcomes to decision-making actors is urgent. Existing formal approaches assume that the unsafe outcomes for which actors can be held responsible are actually realized. This paper considers a broader notion of responsibility where unsafe outcomes are not necessarily realized, but their probabilities are unacceptably high. We present a logic combining strategic, probabilistic and temporal primitives designed to express concepts such as the risk of an undesirable outcome and being responsible for exceeding a risk threshold. We demonstrate that the proposed logic is complete and decidable.

AAMAS Conference 2023 Conference Paper

Intention Progression with Maintenance Goals

• Di Wu
• Yuan Yao
• Natasha Alechina
• Brian Logan
• John Thangarajah

IJCAI Conference 2023 Conference Paper

Multi-Agent Intention Recognition and Progression

• Michael Dann
• Yuan Yao
• Natasha Alechina
• Brian Logan
• Felipe Meneguzzi
• John Thangarajah

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.

PRL Workshop 2023 Workshop Paper

Preemptive Restraining Bolts

• Giovanni Varricchione
• Natasha Alechina
• Mehdi Dastani
• Giuseppe De Giacomo
• Brian Logan
• Giuseppe Perelli

We present preemptive restraining bolts (PRBs), a new approach to safe reinforcement learning which uses non-Markovian action masking, i.e., actions are masked (disallowed) based on the history of the system, rather than just the current state. PRBs are expressed in Pure Past Linear Temporal Logic and have minimal overhead (linear in the size of the state) compared to Markovian action masking, while having the same expressive power as other non-Markovian approaches such as shields (that can express any safety Linear Temporal Logic property). As with restraining bolts, the language in which safety properties are expressed does not have to be the same as the language specifying the features of the state for the learning agent. Critically, PRBs can be applied in the learning process to learn an optimal safe policy while using only safe actions during learning. As a result, PRBs can be used to provide general safety guarantees, without compromising efficiency.

IJCAI Conference 2023 Conference Paper

Probabilistic Temporal Logic for Reasoning about Bounded Policies

• Nima Motamed
• Natasha Alechina
• Mehdi Dastani
• Dragan Doder
• Brian Logan

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.

LAMAS&SR Workshop 2023 Workshop Paper

Reasoning about Exceeding Risk Threshold

• Maksim Gladyshev
• Natasha Alechina
• Mehdi Dastani
• Dragan Doder

The problem of tracing the responsibility for unsafe outcomes to decision-making actors in multi-agent systems is urgent. While all existing approaches focus on deterministic outcomes, assuming that (a group of) agents can be held responsible for φ only if φ actually happens and agents could act differently to prevent φ, we find this notion of responsibility insufficient in many scenarios. In this work we combine coalition ability operator [G] from [12] with a probabilistic operator Lα from [5] that allow us to reason about probabilities and their changes. This approach allows us to claim that a group of agents can be held responsible for the unsafe outcome even if this outcome does not actually happen, but the group has caused its probability to be increased to an (unacceptably) high level. The proposed logic could be useful for analysing and assigning responsibility to groups of agents for their risky and unsafe behaviors. Finally, we establish (weak) completeness and decidability results for the proposed logic.

EUMAS Conference 2023 Conference Paper

Synthesising Reward Machines for Cooperative Multi-Agent Reinforcement Learning

• Giovanni Varricchione
• Natasha Alechina
• Mehdi Dastani
• Brian Logan 0001

Abstract 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. However, current work assumes the multi-agent reward machine to be given. In this paper, we show how reward machines for team tasks can be synthesised automatically from an Alternating-Time Temporal Logic specification of the desired team behaviour and a high-level abstraction of the agents’ environment. We present results suggesting that our automated approach has comparable, if not better, sample efficiency than reward machines generated by hand for multi-agent tasks.

LAMAS&SR Workshop 2022 Workshop Paper

A Probabilistic Finite Temporal Logic for Policies and Intentions

• Nima Motamed
• Natasha Alechina
• Mehdi Dastani
• Dragan Doder

KR Conference 2022 Conference Paper

Automatic Synthesis of Dynamic Norms for Multi-Agent Systems

• Natasha Alechina
• Giuseppe De Giacomo
• Brian Logan
• Giuseppe Perelli

Norms have been widely proposed to coordinate and regulate multi-agent systems (MAS) behaviour. We consider the problem of synthesising and revising the set of norms in a normative MAS to satisfy a design objective expressed in Alternating Time Temporal Logic (ATL*). ATL* is a well-established language for strategic reasoning, which allows the specification of norms that constrain the strategic behaviour of agents. We focus on dynamic norms, that is, norms corresponding to Mealy machines, that allow us to place different constraints on the agents' behaviour depending on the state of the norm and the state of the underlying MAS. We show that synthesising dynamic norms is (k + 1)-EXPTIME, where k is the alternation depth of quantifiers in the ATL* specification. Note that for typical cases of interest, k is either 1 or 2. We also study the problem of removing existing norms to satisfy a new objective, which we show to be 2EXPTIME-complete.

JAIR Journal 2022 Journal Article

Data-Driven Revision of Conditional Norms in Multi-Agent Systems

• Davide Dell'Anna
• Natasha Alechina
• Fabiano Dalpiaz
• Mehdi Dastani
• Brian Logan

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.

IJCAI Conference 2022 Conference Paper

Multi-Agent Intention Progression with Reward Machines

• Michael Dann
• Yuan Yao
• Natasha Alechina
• Brian Logan
• John Thangarajah

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

LAMAS&SR Workshop 2022 Workshop Paper

Synthesising Reward Machines for Cooperative Multi-Agent Reinforcement Learning

• Giovanni Varricchione
• Natasha Alechina
• Mehdi Dastani
• Brian Logan

AAMAS Conference 2021 Conference Paper

Intention Progression using Quantitative Summary Information

• Yuan Yao
• Natasha Alechina
• Brian Logan
• John Thangarajah

A key problem for Belief-Desire-Intention (BDI) agents is intention progression, 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. Monte-Carlo Tree Search (MCTS) has been shown to be a promising approach to the intention progression problem, out-performing other approaches in the literature. However, MCTS relies on runtime simulation of possible interleavings of the plans in each intention, which may be computationally costly. In this paper, we introduce the notion of quantitative summary information which can be used to estimate the likelihood of conflicts between an agent’s intentions. We show how offline simulation can be used to precompute quantitative summary information prior to execution of the agent’s program, and how the precomputed summary information can be used at runtime to guide the expansion of the MCTS search tree and avoid unnecessary runtime simulation. We compare the performance of our approach with standard MCTS in a range of scenarios of increasing difficulty. The results suggest our approach can significantly improve the efficiency of MCTS in terms of the number of runtime simulations performed.

IJCAI Conference 2020 Conference Paper

A Logic of Directions

• Heshan Du
• Natasha Alechina
• Anthony G. Cohn

We propose a logic of directions for points (LD) over 2D Euclidean space, which formalises primary direction relations east (E), west (W), and indeterminate east/west (Iew), north (N), south (S) and indeterminate north/south (Ins). We provide a sound and complete axiomatisation of it, and prove that its satisfiability problem is NP-complete.

IJCAI Conference 2020 Conference Paper

Intention Progression under Uncertainty

• Yuan Yao
• Natasha Alechina
• Brian Logan
• John Thangarajah

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.

AAAI Conference 2020 Conference Paper

Parameterised Resource-Bounded ATL

• Natasha Alechina
• Stéphane Demri
• Brian Logan

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 2EXPTIMEcomplete.

AAMAS Conference 2019 Conference Paper

Decidable Model Checking with Uniform Strategies

• Natasha Alechina
• Mehdi Dastani
• Brian Logan

The logic of strategic ability Resource-Bounded Alternating Time Syntactic Epistemic Logic (RB±ATSEL) has a decidable modelchecking problem for coalition uniform strategies. A strategy is coalition uniform if agents in a coalition select the same joint action in all states where the knowledge of the coalition is the same. However, this presupposes free and unbounded communication between the agents in the coalition before every action selection. In this paper we present a modified version of RB±ATSEL, RB±ATSELc, with explicit (and explicitly costed) communication actions. RB±ATSELc is interpreted on communication models which have an explicit communication step before every action selection. We show that, unlike standard ATL under imperfect information, the model checking problem for RB±ATSELc is decidable under perfect recall uniform strategies. Our decidability result also applies to ATL with imperfect information and perfect recall when interpreted on communication models.

LORI Conference 2019 Conference Paper

Group Announcement Logic with Distributed Knowledge

• Rustam Galimullin
• Thomas Ågotnes
• Natasha Alechina

Abstract Public announcement logic (PAL) is an extension of epistemic logic with dynamic operators that model the effects of all agents simultaneously and publicly acquiring the same piece of information. One of the extensions of PAL, group announcement logic (GAL), allows quantification over (possibly joint) announcements made by agents. In GAL, it is possible to reason about what groups can achieve by making such announcements. It seems intuitive that this notion of coalitional ability should be closely related to the notion of distributed knowledge, the implicit knowledge of a group. Thus, we study the extension of GAL with distributed knowledge, and in particular possible interaction properties between GAL operators and distributed knowledge. The perhaps surprising result is that there in fact are no interaction properties, contrary to intuition. We make this claim precise by providing a sound and complete axiomatisation of GAL with distributed knowledge.

AAMAS Conference 2019 Conference Paper

Groups Versus Coalitions: On the Relative Expressivity of GAL and CAL

• Tim French
• Rustam Galimullin
• Hans van Ditmarsch
• Natasha Alechina

Group Announcement Logic (GAL) and Coalition Announcement Logic (CAL) were proposed to study effects of public announcements by groups of agents on knowledge in multiagent systems. Both logics have operators that quantify over such announcements. In GAL, it is possible to express that ‘a group of agents G has a (truthful) announcement such that after this announcement, some property A holds’; for example, A may involve some agents in G gaining additional knowledge, while agents outside G remain ignorant. In CAL, the meaning of the coalition announcement operator is subtly different: it says that ‘G has an announcement such that, whatever else the agents outside G announce simultaneously, some property A is guaranteed to hold after the joint announcement’. It has been open for some time whether GAL and CAL are equally expressive. We show that this is not the case: there is a property expressible in GAL that is not expressible in CAL. It is still an open question whether CAL is subsumed by GAL, or whether the two logics have incomparable expressive power.

LORI Conference 2019 Conference Paper

Public Group Announcements and Trust in Doxastic Logic

• Elise Perrotin
• Rustam Galimullin
• Quentin Canu
• Natasha Alechina

Abstract We present a doxastic logic for multi-agent systems with public group announcements. Beliefs are represented using belief bases and a dynamic of trust is introduced in order to handle belief change under contradictory announcements. We provide a complete axiomatization for this logic and illustrate its expressive power with a simple example.

AAAI Conference 2019 Conference Paper

Qualitative Spatial Logic over 2D Euclidean Spaces Is Not Finitely Axiomatisable

• Heshan Du
• Natasha Alechina

Several qualitative spatial logics used in reasoning about geospatial data have a sound and complete axiomatisation over metric spaces. It has been open whether the same axiomatisation is also sound and complete for 2D Euclidean spaces. We answer this question negatively by showing that the axiomatisations presented in (Du et al. 2013; Du and Alechina 2016) are not complete for 2D Euclidean spaces and, moreover, the logics are not finitely axiomatisable.

AAMAS Conference 2019 Conference Paper

Strategic Responsibility Under Imperfect Information

• Vahid Yazdanpanah
• Mehdi Dastani
• Wojciech Jamroga
• Natasha Alechina
• Brian Logan

A central issue in the specification and verification of autonomous agents and multiagent systems is the ascription of responsibility to individual agents and groups of agents. When designing a (multi)agent system, we must specify which agents or groups of agents are responsible for bringing about a particular state of affairs. Similarly, when verifying a multiagent system, we may wish to determine the responsibility of agents or groups of agents for a particular state of affairs, and the contribution of each agent to bringing about that state of affairs. In this paper, we discuss several aspects of responsibility, including strategic ability of agents, their epistemic properties, and their relationship to the evolution of the system behavior. We introduce a formal framework for reasoning about the responsibility of individual agents and agent groups in terms of the agents’ strategies and epistemic properties, and state some properties of the framework.

AAAI Conference 2019 Conference Paper

Unbounded Orchestrations of Transducers for Manufacturing

• Natasha Alechina
• Tomáš Brázdil
• Giuseppe De Giacomo
• Paolo Felli
• Brian Logan
• Moshe Y. Vardi

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.

JAIR Journal 2018 Journal Article

Incentive-Compatible Mechanisms for Norm Monitoring in Open Multi-Agent Systems

• Natasha Alechina
• Joseph Y. Halpern
• Ian A. Kash
• Brian Logan

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.

IJCAI Conference 2018 Conference Paper

Incentive-Compatible Mechanisms for Norm Monitoring in Open Multi-Agent Systems (Extended Abstract)

• Natasha Alechina
• Joseph Y. Halpern
• Ian A. Kash
• Brian Logan

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.

FLAP Journal 2018 Journal Article

Modeling Norm Specification and Verification in Multiagent Systems.

• Natasha Alechina
• Brian Logan
• Mehdi Dastani

AAMAS Conference 2018 Conference Paper

Resource Logics with a Diminishing Resource

• Natasha Alechina
• Brian Logan

Model-checking resource logics with production and consumption of resources is a computationally hard and often undecidable problem. We show that it is more feasible under the assumption that there is at least one diminishing resource, that is, a resource which is consumed by every action.

AAAI Conference 2018 Conference Paper

Synthesis of Orchestrations of Transducers for Manufacturing

• Giuseppe De Giacomo
• Moshe Vardi
• Paolo Felli
• Natasha Alechina
• Brian Logan

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 EXPTIMEcomplete. 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.

AAMAS Conference 2017 Conference Paper

Causality, Responsibility and Blame in Team Plans

• Natasha Alechina
• Joseph Y. Halpern
• Brian Logan

Many objectives can be achieved (or may be achieved more effectively) only by a group of agents executing a team plan. If a team plan fails, it is often of interest to determine what caused the failure, the degree of responsibility of each agent for the failure, and the degree of blame attached to each agent. We show how team plans can be represented in terms of structural equations, and then apply the definitions of causality introduced by Halpern [11] and degree of responsibility and blame introduced by Chockler and Halpern [3] to determine the agent(s) who caused the failure and what their degree of responsibility/blame is. We also prove new results on the complexity of computing causality and degree of responsibility and blame, showing that they can be determined in polynomial time for many team plans of interest.

TARK Conference 2017 Conference Paper

Coalition and Group Announcement Logic

• Rustam Galimullin
• Natasha Alechina

Dynamic epistemic logics which model abilities of agents to make various announcements and influence each other's knowledge have been studied extensively in recent years. Two notable examples of such logics are Group Announcement Logic and Coalition Announcement Logic. They allow us to reason about what groups of agents can achieve through joint announcements in non-competitive and competitive environments. In this paper, we consider a combination of these logics -- Coalition and Group Announcement Logic and provide its complete axiomatisation. Moreover, we partially answer the question of how group and coalition announcement operators interact, and settle some other open problems.

AAAI Conference 2017 Conference Paper

Incentivising Monitoring in Open Normative Systems

• Natasha Alechina
• Joseph Halpern
• Ian Kash
• Brian Logan

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.

AIJ Journal 2017 Journal Article

The virtues of idleness: A decidable fragment of resource agent logic

• Natasha Alechina
• Nils Bulling
• Brian Logan
• Hoang Nga Nguyen

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.

AAMAS Conference 2016 Conference Paper

Decentralised Norm Monitoring in Open Multi-Agent Systems (Extended Abstract)

• Natasha Alechina
• Joseph Y. Halpern
• Ian A. Kash
• Brian Logan

JAIR Journal 2016 Journal Article

Qualitative Spatial Logics for Buffered Geometries

• Heshan Du
• Natasha Alechina

This paper describes a series of new qualitative spatial logics for checking consistency of sameAs and partOf matches between spatial objects from different geospatial datasets, especially from crowd-sourced datasets. Since geometries in crowd-sourced data are usually not very accurate or precise, we buffer geometries by a margin of error or a level of tolerance, and define spatial relations for buffered geometries. The spatial logics formalize the notions of `buffered equal' (intuitively corresponding to `possibly sameAs'), `buffered part of' (`possibly partOf'), `near' (`possibly connected') and `far' (`definitely disconnected'). A sound and complete axiomatisation of each logic is provided with respect to models based on metric spaces. For each of the logics, the satisfiability problem is shown to be NP-complete. Finally, we briefly describe how the logics are used in a system for generating and debugging matches between spatial objects, and report positive experimental evaluation results for the system.

IJCAI Conference 2016 Conference Paper

Verifying Existence of Resource-Bounded Coalition Uniform Strategies

• Natasha Alechina
• Mehdi Dastani
• Brian Logan

We consider the problem of whether a coalition of agents has a knowledge-based strategy to ensure some outcome under a resource bound. We extend previous work on verification of multi-agent systems where actions of agents produce and consume resources, by adding epistemic pre- and postconditions to actions. This allows us to model scenarios where agents perform both actions which change the world, and actions which change their knowledge about the world, such as observation and communication. To avoid logical omniscience and obtain a compact model of the system, our model of agents' knowledge is syntactic. We define a class of coalition-uniform strategies with respect to any (decidable) notion of coalition knowledge. We show that the model-checking problem for the resulting logic is decidable for any notion of coalition-uniform strategies in these classes.

IJCAI Conference 2015 Conference Paper

On the Boundary of (Un)decidability: Decidable Model-Checking for a Fragment of Resource Agent Logic

• Natasha Alechina
• Nils Bulling
• Brian Logan
• Hoang Nga Nguyen

The model-checking problem for Resource Agent Logic is known to be undecidable. We review existing (un)decidability results and identify a significant fragment of the logic for which model checking is decidable. We discuss aspects which makes model checking decidable and prove undecidability of two open fragments over a class of models in which agents always have a choice of doing nothing.

IJCAI Conference 2015 Conference Paper

Symbolic Model Checking for One-Resource RB+-ATL

• Natasha Alechina
• Brian Logan
• Hoang Nga Nguyen
• Franco Raimondi

RB±ATL is an extension of ATL where it is possible to model consumption and production of several resources by a set of agents. The modelchecking problem for RB±ATL is known to be decidable. However the only available modelchecking algorithm for RB±ATL uses a forward search of the state space, and hence does not have an efficient symbolic implementation. In this paper, we consider a fragment of RB±ATL, 1RB±ATL, that allows only one resource type. We give a symbolic model-checking algorithm for this fragment of RB±ATL, and evaluate the performance of an MCMAS-based implementation of the algorithm on an example problem that can be scaled to large state spaces.

ECAI Conference 2014 Conference Paper

A Logic of Part and Whole for Buffered Geometries

• Heshan Du
• Natasha Alechina

We propose a new qualitative spatial logic for reasoning about part-whole relations between geometries (sets of points) represented in different geospatial datasets, in particular crowd-sourced datasets. Since geometries in crowd-sourced data can be less inaccurate or precise, we buffer geometries by a margin of error or level of tolerance σ , and define part-whole relation for buffered geometries. The relations between geometries considered in the logic are: buffered part of (BPT), Near and Far. We provide a sound and complete axiomatisation of the logic with respect to metric models, and show that its satisfiability problem is NP-complete.

ECAI Conference 2014 Conference Paper

Decidable Model-Checking for a Resource Logic with Production of Resources

• Natasha Alechina
• Brian Logan 0001
• Nguyen Hoang Nga
• Franco Raimondi

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.

LORI Conference 2013 Conference Paper

Minimal Preference Change

• Natasha Alechina
• Fenrong Liu
• Brian Logan 0001

Abstract We propose a novel approach to preference change. We treat a set of preferences as a special kind of theory, and define minimal change contraction and revision operations in the spirit of minimal change as advocated by the Alchourron, Gardenfors, and Makinson (AGM) 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 also define minimal contraction by a set of preferences, and for a significant special case state postulates, prove a representation theorem, and provide an efficient algorithm implementing minimal contraction by a set of preferences.

AAAI Conference 2013 Conference Paper

Multi-Cycle Query Caching in Agent Programming

• Natasha Alechina
• Tristan Behrens
• Mehdi Dastani
• Koen Hindriks
• Jomi Hubner
• Brian Logan
• Hai Nguyen
• Marc van Zee

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.

IJCAI Conference 2013 Conference Paper

Reasoning about Normative Update

• Natasha Alechina
• Mehdi Dastani
• Brian Logan

We consider the problem of updating a multi-agent system with a set of conditional norms. A norm comes into effect when its condition becomes true, and imposes either an obligation or a prohibition on an agent which remains in force until a state satisfying a deadline condition is reached. If the norm is violated, a sanction is imposed on the agent. We define a notion of a normative update of a multi-agent system by a set of conditional norms, and study the problem of checking whether the agent(s) can bring about a state satisfying a property without incurring a specified number of sanctions.

AAMAS Conference 2012 Conference Paper

Consensus Games

• Julian Zappala
• Natasha Alechina
• Brian Logan

Consensus Games (CGs) are a novel approach to modelling coalition formation in multi-agent systems inspired by threshold models in sociology. In a CG, each agent’s degree of commitment to the coalitions in which it may participate is expressed as a quorum function. Agents are willing to form a coalition only if a quorum consensus can be achieved amongst all agents of the coalition.

AAMAS Conference 2012 Conference Paper

Epistemic Coalition Logic: Completeness and Complexity

• Thomas
• Aring; gotnes
• Natasha Alechina

Coalition logic is currently one of the most popular logics for multi-agent systems. While logics combining coalitional and epistemic operators have received considerable attention, completeness results for epistemic extensions of coalition logic have so far been missing. In this paper we provide several such results and proofs. We prove completeness for epistemic coalition logic with common knowledge, with distributed knowledge, and with both common and distributed knowledge, respectively. Furthermore, we completely characterise the complexity of the satisfiability problem for each of the three logics.

AAMAS Conference 2012 Conference Paper

Programming Norm-Aware Agents

• Natasha Alechina
• Mehdi Dastani
• Brian Logan

Normative organisations provide a means to coordinate the activities of individual agents in multiagent settings. The coordination is realized at run time by creating obligations and prohibitions (norms) for individual agents. If an agent cannot meet an obligation or violates a prohibition, the organisation imposes a sanction on the agent. In this paper, we consider \emph{norm-aware} agents that deliberate on their goals, norms and sanctions before deciding which plan to select and execute. A norm-aware agent is able to violate norms (accepting the resulting sanctions) if it is in the agent's overall interests to do so, e. g. , if meeting an obligation would result in an important goal of the agent becoming unachievable. Programming norm-aware agents in conventional BDI-based agent programming languages is difficult, as they lack support for deliberating about goals, norms and sanctions and deadlines. We present the norm-aware agent programming language N-2APL. N-2APL is based on 2APL and provides support for beliefs, goals, plans, norms, sanctions and deadlines. We give the syntax and semantics of N-2APL, and show that N-2APL agents are rational in the sense of committing to a set of plans that will achieve the agent's most important goals and obligations by their deadlines while respecting its most important prohibitions.

TIME Conference 2012 Invited Paper

Reasoning about Plan Revision in Agent Programs

• Natasha Alechina

This talk is on reasoning about agent programs written in Belief, Desire and Intention (BDI) agent programming languages. BDI programming languages (for example, [1], [2], [3]) have high-level programming primitives which correspond to the beliefs, goals and plans of an AI agent. A program contains a set of rules which allow the agent to adopt plans given its current beliefs and goals. Plans are essentially imperative programs. For example, an agent may have a rule which says that if it believes that it is currently located in room 1 and its goal is to be in room 2, then a suitable plan to adopt would be to exit room 1, turn right, move forward for 3 meters, turn right, and enter room 2.

AAMAS Conference 2011 Conference Paper

Agent Programming with Priorities and Deadlines

• Konstantin Vikhorev
• Natasha Alechina
• Brian Logan

We present AgentSpeak(RT), a real-time BDI agent programming language based on AgentSpeak(L). AgentSpeak(RT) extends AgentSpeak intentions with deadlines which specify the time by which the agent should respond to an event, and priorities which specify the relative importance of responding to a particular event. The AgentSpeak(RT) interpreter commits to a priority-maximal set of intentions: a set of intentions which is maximally feasible while preferring higher priority intentions. We prove some properties of the language, such as guaranteed reactivity delay of the AgentSpeak(RT) interpreter and probabilistic guarantees of successful execution of intentions by their deadlines.

TCS Journal 2011 Journal Article

Reasoning about plan revision in BDI agent programs

• Natasha Alechina
• Mehdi Dastani
• Brian Logan
• John-Jules Ch. Meyer

Facilities for handling plan execution failures are essential for agents which must cope with the effects of nondeterministic actions, and some form of failure handling can be found in most mature agent programming languages and platforms. While such features simplify the development of more robust agents, they make it hard to reason about the execution of agent programs, e. g. , to verify their correctness. In this paper, we present an approach to the verification of agent programs which admit exceptional executions. We consider executions of the BDI-based agent programming language 3APL in which plans containing non-executable actions can be revised using plan revision rules, and present a logic for reasoning about normal and exceptional executions of 3APL programs. We provide a complete axiomatization for the logic and, using a simple example, show how to express properties of 3APL programs as formulas of the logic.

AAMAS Conference 2010 Conference Paper

Resource-bounded alternating-time temporal logic

• Natasha Alechina
• Brian Logan
• Hoang Nga Nguyen
• Abdur Rakib

Many problems in AI and multi-agent systems research are mostnaturally 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 theavailability of resources, and there is no straightforward way ofreasoning about resource requirements in logics such as CoalitionLogic (CL) and Alternating-time Temporal Logic (ATL). In thispaper, we propose a logic for reasoning about coalitional abilityunder resource constraints. We extend ATL with costs of actionsand hence of strategies. We give a complete and sound axiomatisation of the resulting logic Resource-Bounded ATL (RB-ATL) andan efficient model-checking algorithm for it.

IJCAI Conference 2009 Conference Paper

• Natasha Alechina
• Brian Logan
• Nguyen Hoang Nga
• Abdur Rakib

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. This paper presents a Resource-Bounded Coalition Logic (RBCL) which has explicit representation of resource bounds in the language, and gives a complete and sound axiomatisation of RBCL.

LORI Conference 2009 Conference Paper

Expressing Properties of Coalitional Ability under Resource Bounds

• Natasha Alechina
• Brian Logan 0001
• Nguyen Hoang Nga
• Abdur Rakib

Abstract We introduce Coalition Logic for Resource Games (CLRG) which extends Coalition Logic by allowing explicit reasoning about resource endowments of coalitions of agents and resource bounds on strategies. We show how to express interesting properties of coalitional ability under resource bounds in this logic, including properties of Coalitional Resource Games introduced by Wooldridge and Dunne in [1]. We also give an efficient model-checking algorithm for CLRG which makes it possible to verify the properties automatically.

AAMAS Conference 2008 Conference Paper

Reasoning about agent deliberation

• Natasha Alechina
• Mehdi Dastani
• Brian Logan
• John-Jules Meyer

We present a logic for reasoning about properties of agent programs under different agent execution strategies. Using the agent programming language SimpleAPL as an example, we show how safety and liveness properties can be expressed by translating agent programs into expressions of the logic. We give sound and complete axiomatizations of two different program execution strategies for SimpleAPL programs, and, for each of those strategies, prove a correspondence between the operational semantics of SimpleAPL and the models of the corresponding logic.

KR Conference 2008 Conference Paper

Reasoning about Agent Deliberation

• Natasha Alechina
• Mehdi Dastani
• Brian S. Logan
• John-Jules Ch. Meyer

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 axiomatize different deliberation strategies for SimpleAPL programs, and, for each strategy we consider, 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.

AAMAS Conference 2008 Conference Paper

Verifying time, memory and communication bounds in systems of reasoning agents

• Natasha Alechina
• Brian Logan
• Hoang Nga Nguyen
• Abdur Rakib

We present a framework for verifying systems composed of heterogeneous reasoning agents, in which each agent may have differing knowledge and inferential capabilities, and where the resources each agent is prepared to commit to a goal (time, memory and communication bandwidth) are bounded. The framework allows us to investigate, for example, whether a goal can be achieved if a particular agent, perhaps possessing key information or inferential capabilities, is unable (or unwilling) to contribute more than a given portion of its available computational resources or bandwidth to the problem. We present a novel temporal epistemic logic, BMCL, which allows us to describe a set of reasoning agents with bounds on time, memory and the number of messages they can exchange. The bounds on memory and communication are expressed as axioms in the logic. As an example, we show how to axiomatize a system of agents which reason using resolution and prove that the resulting logic is sound and complete. We then show how to encode a simple system of reasoning agents specified in BMCL in the description language of a model checker, and verify that the agents can achieve a goal only if they are prepared to commit certain time, memory and communication resources.

AAAI Conference 2007 Conference Paper

A Logic of Agent Programs

• Natasha Alechina
• Brian Logan

We present a sound and complete logic for reasoning about SimpleAPL programs. SimpleAPL is a fragment of the agent programming language 3APL designed for the implementation of cognitive agents with beliefs, goals and plans. Our logic is a variant of PDL, and allows the specification of safety and liveness properties of agent programs. We prove a correspondence between the operational semantics of SimpleAPL and the models of the logic for two example program execution strategies. We show how to translate agent programs written in SimpleAPL into expressions of the logic, and give an example in which we show how to verify correctness properties for a simple agent program.

TARK Conference 2007 Conference Paper

Full and relative awareness: a decidable logic for reasoning about knowledge of unawareness

• Thomas Ågotnes
• Natasha Alechina

In the most popular logics combining knowledge and awareness, it is not possible to express statements about knowledge of unawareness such as “Ann knows that Bill is aware of something Ann is not aware of” – without using a stronger statement such as “Ann knows that Bill is aware of p and Ann is not aware of p”, for some particular p. Recently, however, Halpern and Rêgo (2006) introduced a logic in which such statements about knowledge of unawareness can be expressed. The logic extends the traditional framework with quantification over formulae, and is thus very expressive. As a consequence, it is not decidable. In this paper we introduce a decidable logic which can be used to reason about certain types of unawareness. The logic extends the traditional framework with an operator expressing full awareness, i. e. , the fact that an agent is aware of everything, and another operator expressing relative awareness, the fact that one agent is aware of everything another agent is aware of. The logic is less expressive than Halpern’s and Rêgo’s logic. It is, however, expressive enough to express all of Halpern’s and Rêgo’s motivating examples. In addition to proving that the logic is decidable and that its satisfiability problem is PSPACE-complete, we present an axiomatisation which we show is sound and complete.

AAMAS Conference 2006 Conference Paper

Belief Revision for AgentSpeak Agents

• Natasha Alechina
• Rafael Bordini
• Jomi H・ner
• Mark Jago
• Brian Logan

ECAI Conference 2006 Conference Paper

Knowing Minimum/Maximum n Formulae

• Thomas Ågotnes
• Natasha Alechina

We introduce a logical language with nullary operators min(n), for each non-negative integer n, which mean ‘the reasoner has at least n different beliefs’. The resulting language allows us to express interesting properties of non-monotonic and resource-bounded reasoners. Other operators, such as 'the reasoner has at most n different beliefs' and the operator introduced in [1, 4]: 'the reasoner knows at most the formulae φ 1, …, φ n ′, are definable using min(n). We introduce several syntactic epistemic logics with min(n) operators, and prove completeness and decidability results for those logics.

ECAI Conference 2006 Conference Paper

Modal Logics for Communicating Rule-Based Agents

• Natasha Alechina
• Mark Jago
• Brian Logan 0001

In this paper, we show how to establish correctness and time bounds (e. g. , quality of service guarantees) for multi-agent systems composed of communicating rule-based agents. The formal models of multi-agent systems we study are transition systems where each transition corresponds to either a rule firing or an act of communication by an agent. We present a complete and sound modal logic which formalises how the beliefs of communicating rule-based agents change over time. Using a simple example, we show how this logic can be used to specify temporal properties of belief change in multi-agent systems in a precise and realistic way, and how existing modal logic techniques such as model-checking can be used to state and verify properties of agents.

KR Conference 2006 Conference Paper

Semantics for Dynamic Syntactic Epistemic Logics

• Thomas Agotnes
• Natasha Alechina

Traditional epistemic logic assumes that agents' knowledge is closed under logical consequence. Many attempts to solve this logical omniscience problem weaken the closure condition by assuming that agents are ignorant of certain logical rules. Duc (1997) avoids the apparent paradox of non-omniscience and non-ignorance by introducing propositions on the form "A is true after some train of thought of agent i" explicitly into the language. A logic DES4n for this language is presented as a dynamic version of S4n. DES4n describes agents who do not necessarily know any (S4n) consequence of their knowledge now, but can get to know any such consequence in the future. Duc does not, however give a semantics for DES4n. In this paper we provide a semantics, for DES4n and some weaker and related systems, and prove soundness and completeness. A key assumption is that an agent can only know a finite number of formulae at each time. The semantics is based on Kripke models, where each world syntactically assigns a finite number of formulae to each agent and the transitions model steps of reasoning.

AAMAS Conference 2006 Conference Paper

Verifying space and time requirements for resource-bounded agents

• Natasha Alechina
• Piergiorgio Bertoli
• Chiara Ghidini
• Mark Jago
• Brian Logan
• Luciano Serafini

EUMAS Conference 2005 Conference Paper

Verifying Bounds on Deliberation Time in Multi-Agent Systems

• Natasha Alechina
• Brian Logan 0001

AAMAS Conference 2004 Conference Paper

A complete and decidable logic for resource-bounded agents

• Natasha Alechina
• Brian Logan
• Mark Whitsey

JELIA Conference 2004 Conference Paper

Modelling Communicating Agents in Timed Reasoning Logics

• Natasha Alechina
• Brian Logan 0001
• Mark Whitsey

Abstract Practical reasoners are resource-bounded—in particular they require time to derive consequences of their knowledge. Building on the Timed Reasoning Logics (TRL) framework introduced in [1], we show how to represent the time required by an agent to reach a given conclusion. TRL allows us to model the kinds of rule application and conflict resolution strategies commonly found in rule-based agents, and we show how the choice of strategy can influence the information an agent can take into account when making decisions at a particular point in time. We prove general completeness and decidability results for TRL, and analyse the impact of communication in an example system consisting of two agents which use different conflict resolution strategies.

AAMAS Conference 2002 Conference Paper

Ascribing beliefs to resource bounded agents

• Natasha Alechina
• Brian Logan

CSL Conference 2001 Conference Paper

Categorical and Kripke Semantics for Constructive S4 Modal Logic

• Natasha Alechina
• Michael Mendler
• Valeria de Paiva
• Eike Ritter

Abstract We consider two systems of constructive modal logic which are computationally motivated. Their modalities admit several computational interpretations and are used to capture intensional features such as notions of computation, constraints, concurrency, etc. Both systems have so far been studied mainly from type-theoretic and category-theoretic perspectives, but Kripke models for similar systems were studied independently. Here we bring these threads together and prove duality results which show how to relate Kripke models to algebraic models and these in turn to the appropriate categorical models for these logics.

LPAR Conference 2001 Conference Paper

Logical Omniscience and the Cost of Deliberation

• Natasha Alechina
• Brian Logan 0001

Abstract Logical omniscience is a well known problem which makes traditional modal logics of knowledge, belief and intentions somewhat unrealistic from the point of view of modelling the behaviour of a resource bounded agent. We propose two logics which take into account ‘deliberation time’ but use a more or less standard possible worlds semantics with classical possible worlds.