Author name cluster

Louwe B. Kuijer

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.

19 papers

2 author rows

FM Conference 2026 Conference Paper

History-Constrained Systems

Louwe B. Kuijer
David Purser
Henry Sinclair-Banks
Patrick Totzke

Abstract We study verification problems for history-constrained systems (HCS), a model of guarded computation that uses nested systems. An outer system describes the process architecture in which a sequence of actions represents the communication between sub-systems through a global bus. Actions are either permitted or blocked locally by guards; these guards read and decide based on the sequence of actions so far in the global bus. When HCS have both the outer systems and the local guard controllers modelled by finite automata, we show they have the same expressive power as regular languages and finite automata, but they are exponentially more succinct. We also analyse games on this model, representing the interaction between environment and controller, and show that solving such games is -complete, where the lower bound already holds for reachability/safety games and the upper bound holds for any $$\omega $$ ω -regular winning condition. Finally, we consider HCS with guards of greater expressive power, Vector Addition Systems with States (VASS). We show that with deterministic coverability-VASS guards the reachability problem is -complete, while with reachability-VASS the problem is undecidable.

DOI

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

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

LORI Conference 2023 Conference Paper

An Arrow-Based Dynamic Logic of Normative Systems and Its Decidability

Hans van Ditmarsch
Louwe B. Kuijer
Mo Liu 0002

Abstract Normative arrow update logic (NAUL) is a logic that combines normative temporal logic (NTL) and arrow update logic (AUL). In NAUL, norms are interpreted as arrow updates on labeled transition systems with a CTL-like logic. We show that the satisfiability problem of NAUL is decidable with a tableau method and it is in EXPSPACE.

Details

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

TARK Conference 2023 Conference Paper

Simple Axioms for Local Properties

Philippe Balbiani
Wiebe van der Hoek
Louwe B. Kuijer

Correspondence theory allows us to create sound and complete axiomatizations for modal logic on frames with certain properties. For example, if we restrict ourselves to transitive frames we should add the axiom $\square \phi \rightarrow \square\square\phi$ which, among other things, can be interpreted as positive introspection. One limitation of this technique is that the frame property and the axiom are assumed to hold globally, i. e. , the relation is transitive throughout the frame, and the agent's knowledge satisfies positive introspection in every world. In a modal logic with local properties, we can reason about properties that are not global. So, for example, transitivity might hold only in certain parts of the model and, as a result, the agent's knowledge might satisfy positive introspection in some worlds but not in others. Van Ditmarsch et al. (2012) introduced sound and complete axiomatizations for modal logics with certain local properties. Unfortunately, those axiomatizations are rather complex. Here, we introduce far simpler axiomatizations for a wide range of local properties.

Details DOI

AIJ Journal 2022 Journal Article

Reasoning about general preference relations

Davide Grossi
Wiebe van der Hoek
Louwe B. Kuijer

Preference relations are at the heart of many fundamental concepts in artificial intelligence, ranging from utility comparisons, to defeat among strategies and relative plausibility among states, just to mention a few. Reasoning about such relations has been the object of extensive research and a wealth of formalisms exist to express and reason about them. One such formalism is conditional logic, which focuses on reasoning about the “best” alternatives according to a given preference relation. A “best” alternative is normally interpreted as an alternative that is either maximal (no other alternative is preferred to it) or optimal (it is at least as preferred as all other alternatives). And the preference relation is normally assumed to satisfy strong requirements (typically transitivity and some kind of well-foundedness assumption). Here, we generalize this existing literature in two ways. Firstly, in addition to maximality and optimality, we consider two other interpretations of “best”, which we call unmatchedness and acceptability. Secondly, we do not inherently require the preference relation to satisfy any constraints. Instead, we allow the relation to satisfy any combination of transitivity, totality and anti-symmetry. This allows us to model a wide range of situations, including cases where the lack of constraints stems from a modeled agent being irrational (for example, an agent might have preferences that are neither transitive nor total nor anti-symmetric) or from the interaction of perfectly rational agents (for example, a defeat relation among strategies in a game might be anti-symmetric but not total or transitive). For each interpretation of “best” (maximal, optimal, unmatched or acceptable) and each combination of constraints (transitivity, totality and/or anti-symmetry), we study the sets of valid inferences. Specifically, in all but one case we introduce a sound and strongly complete axiomatization, and in the one remaining case we show that no such axiomatization exists.

Details DOI

MFCS Conference 2021 Conference Paper

HyperLTL Satisfiability Is Σ₁¹-Complete, HyperCTL* Satisfiability Is Σ₁²-Complete

Marie Fortin
Louwe B. Kuijer
Patrick Totzke
Martin Zimmermann 0002

Temporal logics for the specification of information-flow properties are able to express relations between multiple executions of a system. The two most important such logics are HyperLTL and HyperCTL*, which generalise LTL and CTL* by trace quantification. It is known that this expressiveness comes at a price, i. e. satisfiability is undecidable for both logics. In this paper we settle the exact complexity of these problems, showing that both are in fact highly undecidable: we prove that HyperLTL satisfiability is Σ₁¹-complete and HyperCTL* satisfiability is Σ₁²-complete. These are significant increases over the previously known lower bounds and the first upper bounds. To prove Σ₁²-membership for HyperCTL*, we prove that every satisfiable HyperCTL* sentence has a model that is equinumerous to the continuum, the first upper bound of this kind. We prove this bound to be tight. Finally, we show that the membership problem for every level of the HyperLTL quantifier alternation hierarchy is Π₁¹-complete.

Details

I&C Journal 2020 Journal Article

Arrow update synthesis

Hans van Ditmarsch
Wiebe van der Hoek
Barteld Kooi
Louwe B. Kuijer

In this contribution we present arbitrary arrow update model logic (AAUML). This is a dynamic epistemic logic or update logic. In update logics, static/basic modalities are interpreted on a given relational model whereas dynamic/update modalities induce transformations (updates) of relational models. In AAUML the update modalities formalize the execution of arrow update models, and there is also a modality for quantification over arrow update models. Arrow update models are an alternative to the well-known action models. We provide an axiomatization of AAUML. The axiomatization is a rewrite system allowing to eliminate arrow update modalities from any given formula, while preserving truth. Thus, AAUML is decidable and equally expressive as the base multi-agent modal logic. Our main result is to establish arrow update synthesis: if there is an arrow update model after which φ, we can construct (synthesize) that model from φ. We also point out some pregnant differences in update expressivity between arrow update logics, action model logics, and refinement modal logic.

Details DOI

KR Conference 2020 Conference Paper

Logics of Preference when There Is No Best

Davide Grossi
Wiebe van der Hoek
Louwe B. Kuijer

Well-behaved preferences (e. g. , total pre-orders) are a cornerstone of several areas in artificial intelligence, from knowledge representation, where preferences typically encode likelihood comparisons, to both game and decision theories, where preferences typically encode utility comparisons. Yet weaker (e. g. , cyclical) structures of comparison have proven important in a number of areas, from argumentation theory to tournaments and social choice theory. In this paper we provide logical foundations for reasoning about this type of preference structures where no obvious best elements may exist. Concretely, we compare and axiomatize a number of ways in which the concepts of maximality and optimality can be generalized in this general class of preferences. We thereby expand the scope of the long-standing tradition of the logical analysis of preference.

PDF Details DOI

AIJ Journal 2020 Journal Article

The logic of gossiping

Hans van Ditmarsch
Wiebe van der Hoek
Louwe B. Kuijer

The so-called gossip problem is a formal model of peer-to-peer communication. In order to perform such communication efficiently, it is important to keep track of what agents know about who holds what information at a given point in time. The knowledge that the agents possess depends strongly on the particular type of communication that is used. Here, we formally define a large number of different variants of the gossip problem, that differ in the extent to which communication is private (observable, synchronous or asynchronous), the direction of the flow of information (caller to callee, callee to caller or both) and whether the agents become aware of the exact set of information possessed by their communication partner. We consider a number of formulas that represent interesting properties that a gossip situation may or may not enjoy, and show for which variants they are valid. Additionally, we show that the model checking and validity checking problems for each variant are decidable, and we introduce sound and complete proof systems for them.

Details DOI

FLAP Journal 2019 Journal Article

Strengthening Gossip Protocols using Protocol-Dependent Knowledge.

Hans van Ditmarsch
Malvin Gattinger
Louwe B. Kuijer
Pere Pardo

Distributed dynamic gossip is a generalization of the classic telephone problem in which agents communicate to share secrets, with the additional twist that also telephone numbers are exchanged to determine who can call whom. Recent work focused on the success conditions of simple protocols such as “Learn New Secrets” (LNS) wherein an agent a may only call another agent b if a does not know b’s secret. A protocol execution is successful if all agents get to know all secrets. On partial networks these protocols sometimes fail because they ignore information available to the agents that would allow for better coordination. We study how epistemic protocols for dynamic gossip can be strengthened, using epistemic logic as a simple protocol language with a new operator for protocol-dependent knowledge. We provide definitions of different strengthenings and show that they perform better than LNS, but we also prove that there is no strengthening of LNS that always terminates successfully. Together, this gives us a better picture of when and how epistemic coordination can help in the dynamic gossip problem in particular and distributed systems in general.

Details

LORI Conference 2019 Conference Paper

Who Should Be My Friends? - Social Balance from the Perspective of Game Theory

Wiebe van der Hoek
Louwe B. Kuijer
Yì N. Wáng

Abstract We define balance games, which describe the formation of friendships and enmity in social networks. We show that if the agents give high priority to future profits over short term gains, all Pareto optimal strategies will eventually result in a balanced network. If, on the other hand, agents prioritize short term gains over the long term, every Nash equilibrium eventually results in a network that is stable but that might not be balanced.

Details

AIJ Journal 2018 Journal Article

Second-order propositional modal logic: Expressiveness and completeness results

Francesco Belardinelli
Wiebe van der Hoek
Louwe B. Kuijer

In this paper we advance the state-of-the-art on the application of second-order propositional modal logic (SOPML) in the representation of individual and group knowledge, as well as temporal and spatial reasoning. The main theoretical contributions of the paper can be summarised as follows. Firstly, we introduce the language of (multi-modal) SOPML and interpret it on a variety of different classes of Kripke frames according to the features of the accessibility relations and of the algebraic structure of the quantification domain of propositions. We provide axiomatisations for some of these classes, and show that SOPML is unaxiomatisable on the remaining classes. Secondly, we introduce novel notions of (bi)simulations and prove that they indeed preserve the interpretation of formulas in (the universal fragment of) SOPML. Then, we apply this formal machinery to study the expressiveness of Second-order Propositional Epistemic Logic (SOPEL) in representing higher-order knowledge, i. e. , the knowledge agents have about other agents' knowledge, as well as graph-theoretic notions (e. g. , 3-colorability, Hamiltonian paths, etc.). The final outcome is a rich formalism to represent and reason about relevant concepts in artificial intelligence, while still having a model checking problem that is no more computationally expensive than that of the less expressive quantified boolean logic.

Details DOI

AIJ Journal 2017 Journal Article

Arbitrary arrow update logic

Hans van Ditmarsch
Wiebe van der Hoek
Barteld Kooi
Louwe B. Kuijer

In this paper we introduce arbitrary arrow update logic (AAUL). The logic AAUL takes arrow update logic, a dynamic epistemic logic where the accessibility relations of agents are updated rather than the set of possible worlds, and adds a quantifier over such arrow updates. We investigate the relative expressivity of AAUL compared to other logics, most notably arbitrary public announcement logic (APAL). Additionally, we show that the model checking problem for AAUL is PSPACE-complete. Finally, we introduce a proof system for AAUL, and prove it to be sound and complete.

Details DOI

TARK Conference 2017 Conference Paper

Arbitrary Arrow Update Logic with Common Knowledge is neither RE nor co-RE

Louwe B. Kuijer

Arbitrary Arrow Update Logic with Common Knowledge (AAULC) is a dynamic epistemic logic with (i) an arrow update operator, which represents a particular type of information change and (ii) an arbitrary arrow update operator, which quantifies over arrow updates. By encoding the execution of a Turing machine in AAULC, we show that neither the valid formulas nor the satisfiable formulas of AAULC are recursively enumerable. In particular, it follows that AAULC does not have a recursive axiomatization.

Details DOI

TCS Journal 2017 Journal Article

The undecidability of arbitrary arrow update logic

Hans van Ditmarsch
Wiebe van der Hoek
Louwe B. Kuijer

Arbitrary Arrow Update Logic is a dynamic modal logic with a modality to quantify over arrow updates. Some properties of this logic have already been established, but until now it remained an open question whether the logic's satisfiability problem is decidable. Here, we show by a reduction of the tiling problem that the satisfiability problem of Arbitrary Arrow Update Logic is co-RE hard, and therefore undecidable.

Details DOI

TIME Conference 2016 Conference Paper

On the Length and Depth of Temporal Formulae Distinguishing Non-bisimilar Transition Systems

Valentin Goranko
Louwe B. Kuijer

We investigate the minimal length and nesting depth of temporal formulae that distinguish two given non-bisimilar finite pointed transition systems. We show that such formula can always be constructed in length at most exponential in the combined number of states of both transition systems, and give an example with exponential lower bound, for several common temporal languages. We then show that by using renamings of subformulae or explicit assignments the length of the distinguishing formula can always be reduced to one that is bounded above by a cubic polynomial on the combined size of both transition systems. This is also a bound for the size obtained by using DAG representation of formulae. We also prove that the minimal nesting depth for such formula is less than the combined size of the two state spaces and obtain some tight upper bounds.

Details

LORI Conference 2013 Conference Paper

Sequent Systems for Nondeterministic Propositional Logics without Reflexivity

Louwe B. Kuijer

Abstract In order to deal with ambiguity in statements made in a natural language I introduce nondeterministic semantics for propositional logic with an arbitrary set C of connectives. The semantics are based on the idea that Γ entails $\varDelta$ if and only if every possible deterministic disambiguation of Γ entails every possible deterministic disambiguation of $\varDelta$. I also introduce a cut-free sequent style proof system S C that is sound and complete for the given semantics. Finally I show that while the semantics and proof system do not satisfy reflexivity they do allow certain kinds of substitution of equivalents.

Details