Searcharxiv⌕ Search

arXiv subjects

Philippe Balbiani

Publications and source records attributed to Philippe Balbiani.

At least 19 recordsLinked to original sources
arXiv2026

Resolving Asynchronous Distributed Knowledge

There are by now various epistemic modal logics with intersection modalities for distributed knowledge and intersection update modalities for dynamic phenomena like agents sharing (all their) information, agents receiving information from other agents, and full information protocols. One of those is the logic of Resolving Distributed Knowledge, by Agotnes and Wang. It has distributed knowledge modalities for arbitrary subsets of the set of all agents and it also has so-called resolution modalities for arbitrary subsets of agents sharing their knowledge. In that logic, the agents not involved in the knowledge sharing are aware of the agents sharing knowledge, agents are memory-less, and the kind of dynamics represents synchronous updates, where there is common awareness of the global clock. In contrast, in this contribution we present a logic for Resolving Asynchronous Distributed Knowledge. It is an asynchronous generalization of the synchronous logic of resolving distributed knowledge. The logical semantics is history-based: truth is not only with respect to a given world in a model, but also with respect to a given history of prior resolutions, of which each individual agent can only observe a part. In particular, an agent is unaware of resolutions for groups of agents not including her. As is to be expected, this comes with many technical complications, for example concerning the axiomatization. The synchronous axioms relating resolution to distributed knowledge are now invalid. The modelling advantages of such an asynchronous novel logic, for distributed computing and similar areas, are however substantial and a major asset.

cs.LO↗
arXiv2026

Four intuitionistic modal connectives

We introduce the syntax and the semantics of intuitionistic modal logics based on a diamond connective \`a la Prenosil, its dual box connective, a diamond connective \`a la Wijesekera and its dual box connective. We analyze the modal definability of some elementary classes of frames. We study the complete axiomatizability of the sets of valid formulas determined by these classes of frames. We prove the decidability of the minimal intuitionistic modal logic determined by the class of all frames.

cs.LO↗
arXiv2025

Axiomatisation for an asynchronous epistemic logic with sending and receiving messages

We investigate a logic for asynchronous announcements wherein the sending of the messages by the environment is separated from their reception by the individual agents. Both come with different modalities. In the logical semantics, formulas are interpreted in a world of a Kripke model but given a history of prior announcements and receptions that already happened. An axiomatisation AA for such a logic has been given in prior work, for the formulas that are valid when interpreted in the Kripke model before any such announcements have taken place. This axiomatisation is a reduction system wherein one can show that every formula is equivalent to a purely epistemic formula without dynamic modalities for announcements and receptions. We propose a generalisation AA* of this axiomatisation, for the formulas that are valid when interpreted in the Kripke model given any history of prior announcements and receptions of announcements. It does not extend the axiomatisation AA, for example it is no longer valid that nobody has received any message. Unlike AA, this axiomatisation AA* is infinitary and it is not a reduction system.

cs.LO↗
arXiv2025

Intuitionistic modal logics: epistemic reasoning with distributed knowledge

In this article, we add a diamond to the parametrized box-based propositional language of intuitionistic doxastic logic and intuitionistic epistemic logic introduced by Artemov and Protopopescu. The main results of this article are the proofs of completeness with respect to their appropriate relational semantics of the resulting intuitionistic doxastic logic and intuitionistic epistemic logic with distributed knowledge.

cs.LO↗
arXiv2025

Modal definability in Euclidean modal logics

This paper is about the computability of the modal definability problem in classes of frames determined by Euclidean modal logics. We characterize those Euclidean modal logics such that the classes of frames they determine give rise to an undecidable modal definability problem.

cs.LO↗
arXiv2025

PSPACE-completeness of bimodal transitive weak-density logic

Windows have been introduce in \cite{BalGasq25} as a tool for designing polynomial algorithms to check satisfiability of a bimodal logic of weak-density. In this paper, after revisiting the ``folklore'' case of bimodal $\K4$ already treated in \cite{Halpern} but which is worth a fresh review, we show that windows allow to polynomially solve the satisfiability problem when adding transitivity to weak-density, by mixing algorithms for bimodal K together with windows-approach. The conclusion is that both satisfiability and validity are PSPACE-complete for these logics.

cs.LO↗
arXiv2025

Complexity of some modal logics of density (extended version)

By using a selective filtration argument, we prove that the satisfiability problem of the unimodal logic of density is in $EXPTIME$. By using a tableau-like approach, we prove that the satisfiability problem of the bimodal logic of weak density is in $PSPACE$.

cs.LO↗
arXiv2025

Intuitionistic modal logics: a minimal setting

We introduce an intuitionistic modal logic strictly contained in the intuitionistic modal logic IK and being an appropriate candidate for the title of ``minimal normal intuitionistic modal logic''.

math.LO↗
arXiv2024

Local Intuitionistic Modal Logics and Their Calculi

We investigate intuitionistic modal logics with locally interpreted $\square$ and $\lozenge$. The basic logic LIK is stronger than constructive modal logic WK and incomparable with intuitionistic modal logic IK. We propose an axiomatization of LIK and some of its extensions. We propose bi-nested calculi for LIK and these extensions, thus providing both a decision procedure and a procedure of finite countermodel extraction.

cs.LO↗
arXiv2024

Constructive S4 modal logics with the finite birelational frame property

The logics $\mathsf{CS4}$ and $\mathsf{IS4}$ are the two leading intuitionistic variants of the modal logic $\mathsf{S4}$. Whether the finite model property holds for each of these logics have been long-standing open problems. It was recently shown that $\mathsf{IS4}$ has the finite frame property and thus the finite model property. In this paper, we prove that $\mathsf{CS4}$ also enjoys the finite frame property. Additionally, we investigate the following three logics closely related to $\mathsf{IS4}$. The logic $\mathsf{GS4}$ is obtained by adding the G\"odel--Dummett axiom to $\mathsf{IS4}$; it is both a superintuitionistic and a fuzzy logic and has previously been given a real-valued semantics. We provide an alternative birelational semantics and prove strong completeness with respect to this semantics. The extension $\mathsf{GS4^c}$ of $\mathsf{GS4}$ corresponds to requiring a crisp accessibility relation on the real-valued semantics. We give $\mathsf{GS4^c}$ a birelational semantics corresponding to an extra confluence condition on the $\mathsf{GS4}$ birelational semantics and prove strong completeness. Neither of these two logics have the finite model property with respect to their real-valued semantics, but we prove that they have the finite frame property for their birelational semantics. Establishing the finite birelational frame property immediately establishes decidability, which was previously open for these two logics. Our proofs yield NEXPTIME upper bounds for $\mathsf{CS4}$, $\mathsf{GS4}$, and $\mathsf{GS4^c}$. The logic $\mathsf{S4I}$ is obtained from $\mathsf{IS4}$ by reversing the roles of the modal and relations intuitionistic in the birelational semantics. We also prove the finite frame property, and thereby decidability, for $\mathsf{S4I}$, although our proof does not yield an elementary complexity bound.

cs.LO↗
arXiv2023

A Natural Intuitionistic Modal Logic: Axiomatization and Bi-nested Calculus

We introduce FIK, a natural intuitionistic modal logic specified by Kripke models satisfying the condition of forward confluence. We give a complete Hilbert-style axiomatization of this logic and propose a bi-nested calculus for it. The calculus provides a decision procedure as well as a countermodel extraction: from any failed derivation of a given formula, we obtain by the calculus a finite countermodel of it.

cs.LO↗
arXiv2023

Simple Axioms for Local Properties

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 ϕ\rightarrow \square\squareϕ$ 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.

cs.LO↗
arXiv2021

Some constructive variants of S4 with the finite model property

The logics CS4 and IS4 are intuitionistic variants of the modal logic S4. Whether the finite model property holds for each of these logics has been a long-standing open problem. In this paper we introduce two logics closely related to IS4: GS4, obtained by adding the Godel-Dummett axiom to IS4, and S4I, obtained by reversing the roles of the modal and intuitionistic relations. We then prove that CS4, GS4, and S4I all enjoy the finite model property.

cs.LO↗
arXiv2021

Asynchronous Announcements

We propose a multi-agent epistemic logic of asynchronous announcements, where truthful announcements are publicly sent but individually received by agents, and in the order in which they were sent. Additional to epistemic modalities the logic contains dynamic modalities for making announcements and for receiving them. What an agent believes is a function of her initial uncertainty and of the announcements she has received. Beliefs need not be truthful, because announcements already made may not yet have been received. As announcements are true when sent, certain message sequences can be ruled out, just like inconsistent cuts in distributed computing. We provide a complete axiomatization for this \emph{asynchronous announcement logic} (AA). It is a reduction system that also demonstrates that any formula in $AA$ is equivalent to one without dynamic modalities, just as for public announcement logic. A detailed example modelling message exchanging processes in distributed computing in $AA$ closes our investigation.

cs.AI↗
arXiv2020

About the unification types of the modal logics determined by classes of deterministic frames

The unification problem in a propositional logic is to determine, given a formula F, whether there exists a substitution s such that s(F) is in that logic. In that case, s is a unifier of F. When a unifiable formula has minimal complete sets of unifiers, the formula is either infinitary, finitary, or unitary, depending on the cardinality of its minimal complete sets of unifiers. In this paper, we study the unification types of some modal logics determined by classes of deterministic frames.

cs.LO↗
arXiv2019

Intuitionistic Linear Temporal Logics

We consider intuitionistic variants of linear temporal logic with `next', `until' and `release' based on expanding posets: partial orders equipped with an order-preserving transition function. This class of structures gives rise to a logic which we denote $\iltl$, and by imposing additional constraints we obtain the logics $\itlb$ of persistent posets and $\itlht$ of here-and-there temporal logic, both of which have been considered in the literature. We prove that $\iltl$ has the effective finite model property and hence is decidable, while $\itlb$ does not have the finite model property. We also introduce notions of bounded bisimulations for these logics and use them to show that the `until' and `release' operators are not definable in terms of each other, even over the class of persistent posets.

cs.LO↗