David Fernández–Duque

Philippe Balbiani, Martín Diéguez, David Fernández-Duque et al.

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ödel--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.

Juan Pablo Aguilera, Martín Diéguez, David Fernández-Duque et al.

We investigate a version of linear temporal logic whose propositional fragment is Gödel-Dummett logic (which is well known both as a superintuitionistic logic and a t-norm fuzzy logic). We define the logic using two natural semantics: first a real-valued semantics, where statements have a degree of truth in the real unit interval and second a `bi-relational' semantics. We then show that these two semantics indeed define one and the same logic: the statements that are valid for the real-valued semantics are the same as those that are valid for the bi-relational semantics. This Gödel temporal logic does not have any form of the finite model property for these two semantics: there are non-valid statements that can only be falsified on an infinite model. However, by using the technical notion of a quasimodel, we show that every falsifiable statement is falsifiable on a finite quasimodel, yielding an algorithm for deciding if a statement is valid or not. Later, we strengthen this decidability result by giving an algorithm that uses only a polynomial amount of memory, proving that Gödel temporal logic is PSPACE-complete. We also provide a deductive calculus for Gödel temporal logic, and show this calculus to be sound and complete for the above-mentioned semantics, so that all (and only) the valid statements can be proved with this calculus.

Philippe Balbiani, Joseph Boudou, Martín Diéguez et al.

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.

Philippe Balbiani, David Fernández-Duque, Emiliano Lorini

We present a family of logics for reasoning about agents' positions and motion in the plane which have several potential applications in the area of multi-agent systems (MAS), such as multi-agent planning and robotics. The most general logic includes (i) atomic formulas for representing the truth of a given fact or the presence of a given agent at a certain position of the plane, (ii) atomic programs corresponding to the four basic orientations in the plane (up, down, left, right) as well as the four program constructs of propositional dynamic logic (sequential composition, nondeterministic composition, iteration and test). As this logic is not computably enumerable, we study some interesting decidable and axiomatizable fragments of it. We also present a decidable extension of the iteration-free fragment of the logic by special programs representing motion of agents in the plane.

Esteban Landerreche, David Fernández-Duque

In the Russian cards problem, Alice, Bob and Cath draw $a$, $b$ and $c$ cards, respectively, from a publicly known deck. Alice and Bob must then communicate their cards to each other without Cath learning who holds a single card. Solutions in the literature provide weak security, where Cath does not know with certainty who holds each card that is not hers, or perfect security, where Cath learns no probabilistic information about who holds any given card from Alice and Bob's exchange. We propose an intermediate notion, which we call $\varepsilon$-strong security, where the probabilities perceived by Cath may only change by a factor of $\varepsilon$. We then show that a mild variant of the so-called geometric strategy gives $\varepsilon$-strong safety for arbitrarily small $\varepsilon$ and appropriately chosen values of $a,b,c$.

David Fernández-Duque

We study a general scenario where confidential information is distributed among a group of agents who wish to share it in such a way that the data becomes common knowledge among them but an eavesdropper intercepting their communications would be unable to obtain any of said data. The information is modelled as a deck of cards dealt among the agents, so that after the information is exchanged, all of the communicating agents must know the entire deal, but the eavesdropper must remain ignorant about who holds each card. Valentin Goranko and the author previously set up this scenario as the secure aggregation of distributed information problem and constructed weakly safe protocols, where given any card $c$, the eavesdropper does not know with certainty which agent holds $c$. Here we present a perfectly safe protocol, which does not alter the eavesdropper's perceived probability that any given agent holds $c$. In our protocol, one of the communicating agents holds a larger portion of the cards than the rest, but we show how for infinitely many values of $a$, the number of cards may be chosen so that each of the $m$ agents holds more than $a$ cards and less than $2m^2a$.

David Fernández-Duque, Valentin Goranko

We consider the generic problem of Secure Aggregation of Distributed Information (SADI), where several agents acting as a team have information distributed among them, modeled by means of a publicly known deck of cards distributed among the agents, so that each of them knows only her cards. The agents have to exchange and aggregate the information about how the cards are distributed among them by means of public announcements over insecure communication channels, intercepted by an adversary "eavesdropper", in such a way that the adversary does not learn who holds any of the cards. We present a combinatorial construction of protocols that provides a direct solution of a class of SADI problems and develop a technique of iterated reduction of SADI problems to smaller ones which are eventually solvable directly. We show that our methods provide a solution to a large class of SADI problems, including all SADI problems with sufficiently large size and sufficiently balanced card distributions.

Johan van Benthem, David Fernández-Duque, Eric Pacuit

The intuitive notion of evidence has both semantic and syntactic features. In this paper, we develop an {\em evidence logic} for epistemic agents faced with possibly contradictory evidence from different sources. The logic is based on a neighborhood semantics, where a neighborhood $N$ indicates that the agent has reason to believe that the true state of the world lies in $N$. Further notions of relative plausibility between worlds and beliefs based on the latter ordering are then defined in terms of this evidence structure, yielding our intended models for evidence-based beliefs. In addition, we also consider a second more general flavor, where belief and plausibility are modeled using additional primitive relations, and we prove a representation theorem showing that each such general model is a $p$-morphic image of an intended one. This semantics invites a number of natural special cases, depending on how uniform we make the evidence sets, and how coherent their total structure. We give a structural study of the resulting `uniform' and `flat' models. Our main result are sound and complete axiomatizations for the logics of all four major model classes with respect to the modal language of evidence, belief and safe belief. We conclude with an outlook toward logics for the dynamics of changing evidence, and the resulting language extensions and connections with logics of plausibility change.

Andrés Cordón-Franco, Hans van Ditmarsch, David Fernández-Duque et al.

In the generalized Russian cards problem, the three players Alice, Bob and Cath draw a,b and c cards, respectively, from a deck of a+b+c cards. Players only know their own cards and what the deck of cards is. Alice and Bob are then required to communicate their hand of cards to each other by way of public messages. The communication is said to be safe if Cath does not learn the ownership of any specific card; in this paper we consider a strengthened notion of safety introduced by Swanson and Stinson which we call k-safety. An elegant solution by Atkinson views the cards as points in a finite projective plane. We propose a general solution in the spirit of Atkinson's, although based on finite vector spaces rather than projective planes, and call it the `geometric protocol'. Given arbitrary c,k>0, this protocol gives an informative and k-safe solution to the generalized Russian cards problem for infinitely many values of (a,b,c) with b=O(ac). This improves on the collection of parameters for which solutions are known. In particular, it is the first solution which guarantees $k$-safety when Cath has more than one card.