13 citations · 30 across the 12 of their papers we have counts for
13 papers
History-Constrained Systems
Louwe B. Kuijer, David Purser, Henry Sinclair-Banks +1
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…
Modal Logic for Simulation, Refinement, and Mutual Ignorance
Hans van Ditmarsch, Tim French, Rustam Galimullin +1
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 sim…
The Size of Interpolants in Modal Logics
Balder ten Cate, Louwe Kuijer, Frank Wolter
We start a systematic investigation of the size of Craig interpolants, uniform interpolants, and strongest implicates for (quasi-)normal modal logics. Our main upper bound states t…
Varieties of Distributed Knowledge
Rustam Galimullin, Louwe B. Kuijer
Distributed knowledge is one of the better known group knowledge modalities. While its intuitive idea is relatively clear, there is ample room for interpretation of details. We inv…
Separation and Definability in Fragments of Two-Variable First-Order Logic with Counting
Louwe Kuijer, Tony Tan, Frank Wolter +1
For fragments L of first-order logic (FO) with counting quantifiers, we consider the definability problem, which asks whether a given L-formula can be equivalently expressed by a f…
Satisfiability of Arbitrary Public Announcement Logic with Common Knowledge is -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…
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…
HyperLTL Satisfiability Is Highly Undecidable, HyperCTL is Even Harder
Marie Fortin, Louwe B. Kuijer, Patrick Totzke +1
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 H…
HyperLTL Satisfiability is -complete, HyperCTL* Satisfiability is -complete
Marie Fortin, Louwe B. Kuijer, Patrick Totzke +1
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 H…
Strengthening Gossip Protocols using Protocol-Dependent Knowledge
Hans van Ditmarsch, Malvin Gattinger, Louwe B. Kuijer +1
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…
Arrow Update Synthesis
Hans van Ditmarsch, Wiebe van der Hoek, Barteld Kooi +1
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 interpr…
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…
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 that uses an arbitrary arrow update modality to quantify over all arrow updates. Some properties of this logic have already be…