Author name cluster

Rustam Galimullin

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

20 papers

2 author rows

AAAI Conference 2026 Conference Paper

Formal Verification of Diffusion Auctions

Rustam Galimullin
Munyque Mittelmann
Laurent Perrussel

In diffusion auctions, sellers can leverage an underlying social network to broaden participation, thereby increasing their potential revenue. Specifically, sellers can incentivise participants in their auction to diffuse information about the auction through the network. While numerous variants of such auctions have been recently studied in the literature, the formal verification and strategic reasoning perspectives have not been investigated yet. Our contribution is threefold. First, we introduce a logical formalism that captures the dynamics of diffusion and its strategic dimension. Second, for such a logic, we provide model-checking procedures that allow one to verify properties like the Nash equilibrium, and that pave the way towards checking the existence of sellers' strategies. Third, we establish computational complexity results for the presented algorithms.

PDF Details DOI

AAMAS Conference 2026 Conference Paper

On Angels and Demons: Strategic (De)Construction of Dynamic Models

Davide Catta
Rustam Galimullin
Munyque Mittelmann

In recent years, there has been growing interest in logics that formalise strategic reasoning about agents capable of modifying the structure of a given model. This line of research has been motivated by applications where a modelled system evolves over time, such as communication networks, security protocols, and multi-agent planning. In this paper, we introduce three logics for reasoning about strategies that modify the topology of weighted graphs. In Strategic Deconstruction Logic, a destructive agent (the demon) removes edges up to a certain cost. In Strategic Construction Logic, a constructive agent (the angel) adds edges within a cost bound. Finally, Strategic Update Logic combines both agents, who may cooperate or compete. We study the expressive power of these logics and the complexity of their model checking problems.

PDF

AAMAS Conference 2026 Conference Paper

The Dynamic Turn in Strategy Logics

Rustam Galimullin
Maksim Gladyshev
Munyque Mittelmann
Nima Motamed

Strategy Logics are well-studied frameworks for the specification and verification of strategic abilities in multi-agent systems (MAS). However, the current generation of Strategy Logics is limited to staticreasoningaboutfixedmodelsofMAS. Thislimitationexcludes a plethora of applications that require addressing dynamic changes and updates. Examples include verifying that a computer program executes correctly after an upgrade, automatically repairing MAS to meet safety requirements, and reasoning about robots operating in a dynamic environment. To address this limitation, we propose a new research agenda centered on enriching Strategy Logics with concepts and intuitions from Dynamic Epistemic Logic, aiming to develop a holistic and general framework that captures dynamic phenomena in MAS and facilitates their verification.

PDF

AAMAS Conference 2025 Conference Paper

Changing the Rules of the Game: Reasoning About Dynamic Phenomena in Multi-Agent Systems

Rustam Galimullin
Maksim Gladyshev
Munyque Mittelmann
Nima Motamed

The design and application of multi-agent systems (MAS) require reasoning about the effects of modifications on their underlying structure. In particular, such changes may impact the satisfaction of system specifications and the strategic abilities of their autonomous components. In this paper, we are concerned with the problem of verifying and synthesising modifications (or updates) of MAS. We propose an extension of the Alternating-Time Temporal Logic (ATL) that enables reasoning about the dynamics of model change, called the Logic for ATL Model Building (LAMB). We show how LAMB can express various intuitions and ideas about the dynamics of MAS, from normative updates to mechanism design. As the main technical result, we prove that, while being strictly more expressive than ATL, LAMB enjoys a P-complete model-checking procedure.

PDF

IJCAI Conference 2025 Conference Paper

First-Order Coalition Logic

Davide Catta
Rustam Galimullin
Aniello Murano

We introduce First-Order Coalition Logic (FOCL), which combines key intuitions behind Coalition Logic (CL) and Strategy Logic (SL). Specifically, FOCL allows for arbitrary quantification over actions of agents. FOCL is interesting for several reasons. First, we show that FOCL is strictly more expressive than existing coalition logics. Second, we provide a sound and complete axiomatisation of FOCL, which, to the best of our knowledge, is the first axiomatisation of any variant of SL in the literature. Finally, while discussing the satisfiability problem for FOCL, we reopen the question of the recursive axiomatisability of SL.

PDF Details DOI

LORI Conference 2025 Conference Paper

Intentionally Anonymous Public Announcements

Thomas Ågotnes
Rustam Galimullin
Ken Satoh
Satoshi Tojo

Abstract We formalise the notion of an intentionally anonymous public announcement in the tradition of public announcement logic. An anonymous announcement can be seen as in-between a public announcement from “the outside” (an announcement of $\varphi $ ) and a public announcement by one of the agents a (an announcement of $K_a\varphi $ ): we get more information than just $\varphi $, but not (necessarily) about exactly who made it. In this paper we assume that it is common knowledge that the announcer intended to be anonymous. Like in the Russian Cards puzzle, with that assumption, anonymous announcements in fact reveal more information than without. We introduce an operator for intentionally anonymous announcements, and show that in several ways it all boils down to the notion of a “safe” announcement (again, similarly to Russian Cards). We model safety via a fixed-point operator that is similar to common knowledge. Main formal results include comparisons of expressivity and axiomatic completeness for a language expressing safety.

Details

TARK Conference 2025 Conference Paper

Modal Logic for Simulation, Refinement, and Mutual Ignorance

Hans van Ditmarsch
Tim French 0002
Rustam Galimullin
Louwe B. Kuijer

Simulation and refinement are variations of the bisimulation relation, where in the former we keep only atoms and forth, and in the latter only atoms and back. Quantifying over simulations and refinements captures the effects of information change in a multi-agent system. In the case of quantification over refinements, we are looking at all the ways the agents in a system can become more informed. Similarly, in the case of quantification over simulations, we are dealing with all the ways the agents can become less informed, or in other words, could have been less informed, as we are at liberty how to interpret time in dynamic epistemic logic. While quantification over refinements has been well explored in the literature, quantification over simulations has received considerably less attention. In this paper, we explore the relationship between refinements and simulations. To this end, we also employ the notion of mutual factual ignorance that allows us to capture the state of a model before agents have learnt any factual information. In particular, we consider the extensions of multi-modal logic with the simulation and refinement modalities, as well as modalities for mutual factual ignorance. We provide reduction-based axiomatizations for several of the resulting logics that are built extending one another in a modular fashion.

Details DOI

AAMAS Conference 2024 Conference Paper

Dynamic Epistemic Logic of Resource Bounded Information Mining Agents

Vitaliy Dolgorukov
Rustam Galimullin
Maksim Gladyshev

Logics for resource-bounded agents have been getting more and more attention in recent years since they provide us with more realistic tools for modelling and reasoning about multi-agent systems. While many existing approaches are based on the idea of agents as imperfect reasoners, who must spend their resources to perform logical inference, this is not the only way to introduce resource constraints into logical settings. In this paper we study agents as perfect reasoners, who may purchase a new piece of information from a trustworthy source. For this purpose we propose dynamic epistemic logic for semi-public queries for resource-bounded agents. In this logic (groups of) agents can perform a query (ask a question) about whether some formula is true and receive a correct answer. These queries are called semi-public, because the very fact of the query is public, while the answer is private. We also assume that every query has a cost and every agent has a budget constraint. Finally, our framework allows us to reason about group queries, in which agents may share resources to obtain a new piece of information together. We demonstrate that our logic is complete, decidable and has an efficient model checking procedure.

PDF

AAMAS Conference 2024 Conference Paper

Synthesizing Social Laws with ATL Conditions

Rustam Galimullin
Louwe B. Kuijer

We introduce a formalism called SLAM (Social Laws on ATL Models) for defining social laws. Such social laws can constrain the behaviour of a multi-agent system. Importantly, these social laws can use any ATL formula as the condition under which an action is allowed. We show that the synthesis problem for these social laws is NP-complete. This generalizes a known result that synthesis of social laws that use only Boolean conditions is NP-complete.

PDF

AAMAS Conference 2023 Conference Paper

(Arbitrary) Partial Communication

Rustam Galimullin
Fernando R. Velázquez-Quesada

Communication within groups of agents has been lately the focus of research in dynamic epistemic logic (DEL). This paper studies a recently introduced form of partial (more precisely, topic-based) communication. This type of communication allows for modelling scenarios of multi-agent collaboration and negotiation, and it is particularly well-suited for situations in which sharing all information is not feasible/advisable. After presenting results on invariance and complexity of model checking, the paper compares partial communication to public announcements, probably the most well-known type of communication in DEL. It is shown that the settings are, update-wise, incomparable: there are scenarios in which the effect of a public announcement cannot be replicated by partial communication, and vice versa. Then, the paper shifts its attention to strategic topic-based communication. It does so by extending the language with a modality that quantifies over the topics the agents can ‘talk about’. For this new framework, it provides a complete axiomatisation, showing also that the new language’s model checking problem is PSPACE-complete. The paper closes showing that, in terms of expressivity, this new language of arbitrary partial communication is incomparable to that of arbitrary public announcements.

PDF

JAAMAS Journal 2023 Journal Article

Quantifying over information change with common knowledge

Thomas Ågotnes
Rustam Galimullin

Abstract Public announcement logic (PAL) extends multi-agent epistemic logic with dynamic operators modelling the effects of public communication. Allowing quantification over public announcements lets us reason about the existence of an announcement that reaches a certain epistemic goal. Two notable examples of logics of quantified announcements are arbitrary public announcement logic (APAL) and group announcement logic (GAL). While the notion of common knowledge plays an important role in PAL, and in particular in characterisations of epistemic states that an agent or a group of agents might make come about by performing public announcements, extensions of APAL and GAL with common knowledge still haven’t been studied in detail. That is what we do in this paper. In particular, we consider both conservative extensions, where the semantics of the quantifiers is not changed, as well as extensions where the scope of quantification also includes common knowledge formulas. We compare the expressivity of these extensions relative to each other and other connected logics, and provide sound and complete axiomatisations. Finally, we show how the completeness results can be used for other logics with quantification over information change.

Details DOI

TARK Conference 2023 Conference Paper

Satisfiability of Arbitrary Public Announcement Logic with Common Knowledge is Σ11-hard

Rustam Galimullin
Louwe B. Kuijer

Arbitrary Public Announcement Logic with Common Knowledge (APALC) is an extension of Public Announcement Logic with common knowledge modality and quantifiers over announcements. We show that the satisfiability problem of APALC on S5-models, as well as that of two other related logics with quantification and common knowledge, is $\Sigma^1_1$-hard. This implies that neither the validities nor the satisfiable formulas of APALC are recursively enumerable. Which, in turn, implies that APALC is not finitely axiomatisable.

Details DOI

LORI Conference 2021 Conference Paper

Dynamic Coalition Logic: Granting and Revoking Dictatorial Powers

Rustam Galimullin
Thomas Ågotnes

Abstract One of the classic formalisms for reasoning about multi-agent coalitional ability is coalition logic (CL). In CL it is possible to express what a coalition can achieve in the next step no matter what agents outside of the coalition do at the same time. We propose an extension of CL with dynamic operators that allow us to grant dictatorial powers to agents or to revoke them. In such a way we are able to reason about the dynamics of coalitional ability. We also discuss some logical properties of the proposed formalisms and compare their relative expressive power.

Details

LAMAS&SR Workshop 2021 Workshop Paper

How Groups Can Help Coalitions

Rustam Galimullin

In this extended abstract we present the themes and results of a recent paper [11]1. We omit many definitions in order to make the abstract more readable, and for technicalities and pointers to the literature the reader is invited to consult the full paper. Moreover, in order to prevent excessive citing of [11], we refer to it as ‘the paper’.

PDF Details

TARK Conference 2021 Conference Paper

No Finite Model Property for Logics of Quantified Announcements

Hans van Ditmarsch
Tim French 0002
Rustam Galimullin

Quantification over public announcements shifts the perspective from reasoning strictly about the results of a particular announcement to reasoning about the existence of an announcement that achieves some certain epistemic goal. Depending on the type of the quantification, we get different formalisms, the most known of which are arbitrary public announcement logic (APAL), group announcement logic (GAL), and coalition announcement logic (CAL). It has been an open question whether the logics have the finite model property, and in the paper we answer the question negatively. We also discuss how this result is connected to other open questions in the field.

Details DOI

AAMAS Conference 2021 Conference Paper

Quantified Announcements and Common Knowledge

Rustam Galimullin
Thomas Ågotnes

Public announcement logic (PAL) extends multi-agent epistemic logic with dynamic operators modelling the effects of public communication. Allowing quantification over public announcements lets us reason about the existence of an announcement to reach a certain epistemic goal. Two notable examples of logics of quantified announcements are arbitrary public announcement logic (APAL) and group announcement logic (GAL). The notion of common knowledge plays an important role in PAL, and in particular in characterisations of epistemic states that an agent or a group of agents might make come about by performing public announcements. In this paper, we study extensions of APAL and GAL with common knowledge, which has not been done before. We consider both conservative extensions where the semantics of the quantifiers is not changed, as well as extensions where the scope of quantification also includes common knowledge formulas. We compare the expressivity of these extensions relative to each other and other connected logics, and provide sound and complete axiomatisations.

PDF

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.

Details

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.

PDF

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.

Details

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.

Details DOI