Publications

Mathematical logic provides a formal language to describe complex abstract phenomena whereby a finite formula written in a finite alphabet states a property of an object that may even be infinite. Thus, the complexity of the underlying objects is abstracted away to give way for a simple syntactic description, a kind of mathesis universalis. The complexity, however, continues affecting which ways of reasoning are valid.

Structural proof theory reasons using proof objects more complex than individual formulas. One of its goals is to find minimal additional structures, depending on the complexity of the underlying objects, sufficient for efficient and modular reasoning about them.

In this paper, we are primarily interested in both the global structure used for reasoning and the local part of this structure employed to justify single inference steps. We provide recently developed examples where adapting the global structure of the sequent to the local structure of (potentially infinite) Kripke models yielded both quantitative and qualitative benefits in establishing fundamental logical properties such as complexity and interpolation.

In this paper, we describe a novel constructive method of proving the Craig interpolation property (CIP) based on cut-free hypersequent calculi and apply the method to prove the CIP for the modal logic S5.

Epistemic Logic (EL) successfully models epistemic and doxastic attitudes of agents and groups in multi-agent systems, including distributed systems, via relational structures called Kripke models. Dynamic Epistemic Logic (DEL) adds communication in the form of model-transforming updates. Private communication is key in distributed systems as processes exchanging (potentially corrupted) information about their private local state may not be detectable by any other process. This focus on privacy clashes with the fact that updates are applied to the whole Kripke model, which is usually commonly known by all agents, potentially leading to information leakage. To avoid information leakage and to minimize the corruption of local states resulting from faulty information, we introduce a special stratified structure for Kripke models using a privatization operation that explicitly breaks the common knowledge of the model. To represent agent-to-agent communication we introduce a novel leakage-free update mechanism for solving the consistent update synthesis task: design an update that makes a given goal formula true while maintaining the consistency of agents’ beliefs, if possible.

Simplicial complexes are a convenient semantic primitive to reason about processes (agents) communicating with each other in synchronous and asynchronous computation. Impure simplicial complexes distinguish active processes from crashed ones, in other words, agents that are alive from agents that are dead. In order to rule out that dead agents reason about themselves and about other agents, three-valued epistemic semantics have been proposed where, in addition to the usual values true and false, the third value stands for undefined: the knowledge of dead agents is undefined and so are the propositional variables describing their local state. Other semantics for impure complexes are two-valued where a dead agent knows everything. Different choices in designing a semantics produce different three-valued semantics, and also different two-valued semantics. In this work, we categorize the available choices by discounting the bad ones, identifying the equivalent ones, and connecting the non-equivalent ones via a translation. The main result of the paper is identifying the main relevant distinction to be the number of truth values and bridging this difference by means of a novel embedding from three- into two-valued semantics. This translation also enables us to highlight quite fundamental modeling differences underpinning various two- and three-valued approaches in this area of combinatorial topology. In particular, pure complexes can be defined as those invariant under the translation.

Byzantine fault-tolerant distributed systems are designed to provide resiliency despite arbitrary faults, i.e., even in the presence of agents who do not follow the common protocol and/or despite compromised communication. It is, therefore, common to focus on the perspective of correct agents, to the point that the epistemic state of byzantine agents is completely ignored. Since this view relies on the assumption that faulty agents may behave arbitrarily adversarially, it is overly conservative in many cases. In blockchain settings, for example, dishonest players are usually not malicious, but rather selfish, and thus just follow some “hidden” protocol that is different from the protocol of the honest players. Similarly, in high-availability large-scale distributed systems, software updates cannot be globally instantaneous, but are rather performed node-by-node. Consequently, updated and non-updated nodes may simultaneously be involved in a protocol for solving a distributed task like consensus or transaction commit. Clearly, the usual assumption of common knowledge of the protocol is inappropriate in such a setting. On the other hand, joint protocol execution and, sometimes, even basic communication becomes problematic without this assumption: How are agents supposed to interpret each other’s messages without knowing their mutual communication protocols? We propose a novel epistemic modality creed for epistemic reasoning in heterogeneous distributed systems with agents that are uncertain of the actual communication protocol used by their peers. We show that the resulting logic is quite closely related to modal logic S5, the standard logic of epistemic reasoning in distributed systems. We demonstrate the utility of our approach by several examples .

We introduce a Gentzen-style framework, called layered sequent calculi, for modal logic K5 and its extensions KD5, K45, KD45, KB5, and S5 with the goal to investigate the uniform Lyndon interpolation property (ULIP), which implies both the uniform interpolation property and the Lyndon interpolation property. We obtain complexity-optimal decision procedures for all logics and present a constructive proof of the ULIP for K5, which to the best of our knowledge, is the first such syntactic proof. To prove that the interpolant is correct, we use model-theoretic methods, especially bisimulation modulo literals.

In this paper we demonstrate decidability for the intuitionistic modal logic S4 first formulated by Fischer Servi. This solves a problem that has been open for almost thirty years since it had been posed in Simpson's PhD thesis in 1994. We obtain this result by performing proof search in a labelled deductive system that, instead of using only one binary relation on the labels, employs two: one corresponding to the accessibility relation of modal logic and the other corresponding to the order relation of intuitionistic Kripke frames. Our search algorithm outputs either a proof or a finite counter-model, thus, additionally establishing the finite model property for intuitionistic S4, which has been another long-standing open problem in the area.

Knowledge has long been identified as an inherent component of agents' decision-making in distributed systems. However, for agents in fault-tolerant distributed systems with fully byzantine agents, achieving knowledge is, in most cases, unrealistic. If agents can both lie and themselves be mistaken, then a message received is generally not sufficient to create knowledge. This problem is adequately addressed by an epistemic modality named hope, which has already been axiomatized. In this paper, we propose an alternative complete axiomatization for the hope modality by removing the reliance on designated atoms denoting correctness of individual agents and show that hope can be described as a KB4_n system. This additionally bringsa more streamlined presentation of the common hope modality (the hope analog of common knowledge). We also combine KB4_n hope modalities with S5_n knowledge modalities traditionally used in the epistemic analysis of fault-free distributed systems and present a logic enriched with both common knowledge and common hope. In these logics we formalize as frame-characterizable axioms some of the main properties of fully byzantine distributed systems: bounds on the number of faulty agents and the epistemic limitations due to agents' inability to rule out brain-in-a-vat scenarios.

A modular proof-theoretic framework was recently developed to prove Craig interpolation for normal modal logics based on generalizations of sequent calculi (e.g., nested sequents, hypersequents, and labelled sequents). In this paper, we turn to uniform interpolation, which is stronger than Craig interpolation. We develop a constructive method for proving uniform interpolation via nested sequents and apply it to reprove the uniform interpolation property for normal modal logics K, D, and T. While our method is proof-theoretic, the definition of uniform interpolation for nested sequents also uses semantic notions, including bisimulation modulo an atomic proposition.

In this paper, we provide an epistemic analysis of a simple variant of the fundamental consistent broadcasting primitive for byzantine fault-tolerant asynchronous distributed systems. Our Firing Rebels with Relay (FRR) primitive enables agents with a local preference for acting/not acting to trigger an action (FIRE) at all correct agents, in an all-or-nothing fashion. By using the epistemic reasoning framework for byzantine multi-agent systems introduced in our TARK'19 paper, we develop the necessary and sufficient state of knowledge that needs to be acquired by the agents in order to FIRE. It involves eventual common hope (a modality related to belief), which we show to be attained already by achieving eventual mutual hope in the case of FRR. We also identify subtle variations of the necessary and sufficient state of knowledge for FRR for different assumptions on the local preferences.

We extend a recently introduced epistemic reasoning framework for multi-agent systems with byzantine faulty asynchronous agents by incorporating features like reliable communication, time-bounded communication, multicasting, synchronous and lockstep synchronous agents. We use this extension framework for analyzing fault detection abilities of synchronous and lockstep synchronous agents and show that even perfectly synchronized clocks cannot be used to avoid “brain-in-a-vat” scenarios.

We introduce a novel comprehensive framework for epistemic reasoning in multi-agent systems where agents may behave asynchronously and may be byzantine faulty. Extending Fagin et al.'s classic runs-and-systems framework to agents who may arbitrarily deviate from their protocols, it combines epistemic and temporal logic and incorporates fine-grained mechanisms for specifying distributed protocols and their behaviors. Besides our framework's ability to express any type of faulty behavior, from fully byzantine to fully benign, it allows to specify arbitrary timing and synchronization properties. As a consequence, it can be adapted to any message-passing distributed computing model we are aware of, including synchronous processes and communication, (un-)reliable uni-/multi-/broadcast communication, and even coordinated action. The utility of our framework is demonstrated by formalizing the brain-in-a-vat scenario, which exposes the substantial limitations of what can be known by asynchronous agents in fault-tolerant distributed systems. Given the knowledge of preconditions principle, this restricts preconditions that error-prone agents can use in their protocols. In particular, it is usually necessary to relativize preconditions with respect to the correctness of the acting agent.

Causality is an important concept both for proving impossibility results and for synthesizing efficient protocols in distributed computing. For asynchronous agents communicating over unreliable channels, causality is well studied and understood. This understanding, however, relies heavily on the assumption that agents themselves are correct and reliable. We provide the first epistemic analysis of causality in the presence of byzantine agents, i.e., agents that can deviate from their protocol and, thus, cannot be relied upon. Using our new framework for epistemic reasoning in fault-tolerant multi-agent systems, we determine the byzantine analog of the causal cone and describe a communication structure, which we call a multipede, necessary for verifying preconditions for actions in this setting.

The goal of this paper is extending to intermediate logics the constructive proof-theoretic method of proving Craig and Lyndon interpolation via hypersequents and nested sequents developed earlier for classical modal logics. While both Jankov and Gödel logics possess hypersequent systems, we show that our method can only be applied to the former. To tackle the latter, we switch to linear nested sequents, demonstrate syntactic cut elimination for them, and use it to prove interpolation for Gödel logic. Thereby, we answer in the positive the open question of whether Gödel logic enjoys the Lyndon interpolation property.

Interpolation is a fundamental logical property with applications in mathematics, computer science, and artificial intelligence. In this paper, we develop a general method of translating a semantic description of modal logics via Kripke models into a constructive proof of the Lyndon interpolation property (LIP) via labelled sequents. Using this method we demonstrate that all frame conditions representable as Horn formulas imply the LIP and that all 15 logics of the modal cube, as well as the infinite family of transitive Geach logics, enjoy the LIP.

The proof-theoretic method of proving the Craig interpolation property was recently extended from sequents to nested sequents and hypersequents. There the notations were formalism-specific, obscuring the underlying common idea, which is presented here in a general form applicable also to other similar formalisms, e.g., prefixed tableaus. It describes requirements sufficient for using the method on a proof system for a logic, as well as additional requirements for certain types of rules. The applicability of the method, however, does not imply its success. We also provide examples from common proof systems to highlight various types of interpolant manipulations that can be employed by the method. The new results are the application of the method to a recent formalism of grafted hypersequents (in their tableau version), the general treatment of external structural rules, including the analytic cut, and the method's extension to the Lyndon interpolation property.

Justification logics were introduced by Artemov in 1995 to provide intuitionistic logic with a classical provability semantics, a problem originally posed by Gödel. Justification logics are refinements of modal logics and formally connected to them by so-called realization theorems. A constructive proof of a realization theorem typically relies on a cut-free sequent-style proof system for the corresponding modal logic. A uniform realization theorem for all the modal logics of the so-called modal cube, i.e., for the extensions of the basic modal logic K with any subset of the axioms d, t, b, 4, and 5, has been proven using nested sequents. However, the proof was not modular in that some realization theorems required postprocessing in the form of translation on the justification logic side. This translation relied on additional restrictions on the language of the justification logic in question, thus, narrowing the scope of realization theorems. We present a fully modular proof of the realization theorems for the modal cube that is based on modular nested sequents introduced by Marin and Straßburger.

We introduce a justification logic with a novel constructor for evidence terms, according to which the new information itself serves as evidence for believing it. We provide a sound and complete axiomatization for belief expansion and minimal change and explain how the minimality can be graded according to the strength of reasoning. We also provide an evidential analog of the Ramsey axiom.

Justification logics are propositional modal-like logics that instead of statements A is known include statements of the form A is known for reason t where the term t can represent an informal justification for A or a formal proof of A. In our present work, we introduce model-theoretic tools, namely: filtrations and a certain form of generated submodels, in the context of justification logic in order to obtain decidability results. Apart from reproving already known results in a uniform way, we also prove new results. In particular, we use our submodel construction to establish decidability for a justification logic with common knowledge for which so far no decidability proof was available.

An ontologically transparent semantics for justifications that interprets justifications as sets of formulas they justify has been recently presented by Artemov. However, this semantics of modular models has only been studied for the case of the basic justification logic J, corresponding to the modal logic K. It has been left open how to extend and relate modular models to the already existing symbolic and epistemic semantics for justification logics with additional axioms, in particular, for logics of knowledge with factive justifications.

We introduce modular models for extensions of J with any combination of the axioms (jd), (jt), (j4), (j5), and (jb), which are the explicit counterparts of standard modal axioms. After establishing soundness and completeness results, we examine the relationship of modular models to more traditional symbolic and epistemic models. This comparison yields several new semantics, including symbolic models for logics of belief with negative introspection (j5) and models for logics with the axiom (jb). Besides pure justification logics, we also consider logics with both justifications and a belief/knowledge modal operator of the same strength. In particular, we use modular models to study the conditions under which the addition of such an operator to a justification logic yields a conservative extension.

Justification logic is an epistemic framework that provides a way to express explicit justifications for the agent's belief. In this paper, we present OPAL, a dynamic justification logic that includes term operators to reflect public announcements on the level of justifications. We create dynamic epistemic semantics for OPAL. We also elaborate on the relationship of dynamic justification logics to Gerbrandy–Groeneveld's PAL by providing a partial realization theorem.

Justification logics are refinements of modal logics where modalities are replaced by justification terms. They are connected to modal logics via so-called realization theorems. We present a syntactic proof of a single realization theorem that uniformly connects all the normal modal logics formed from the axioms d, t, b, 4, and 5 with their justification counterparts. The proof employs cut-free nested sequent systems together with Fitting’s realization merging technique. We further strengthen the realization theorem for KB5 and S5 by showing that the positive introspection operator is superfluous.

It is not clear what a system for evidence-based common knowledge should look like if common knowledge is treated as a greatest fixed point. This paper is a preliminary step towards such a system. We argue that the standard induction rule is not well suited to axiomatize evidence-based common knowledge. As an alternative, we study two different deductive systems for the logic of common knowledge. The first system makes use of an induction axiom whereas the second one is based on co-inductive proof theory. We show the soundness and completeness for both systems.

The logical omniscience feature assumes that an epistemic agent knows all logical consequences of her assumptions. This paper offers a general theoretical framework that views logical omniscience as a computational complexity problem. We suggest the following approach: we assume that the knowledge of an agent is represented by an epistemic logical system E; we call such an agent not logically omniscient if for any valid knowledge assertion A of type F is known, a proof of F in E can be found in polynomial time in the size of A. We show that agents represented by major modal logics of knowledge and belief are logically omniscient, whereas agents represented by justification logic systems are not logically omniscient with respect to t is a justification for F.

Justification Logic studies epistemic and provability phenomena by introducing justifications/proofs into the language in the form of justification terms. Pure justification logics serve as counterparts of traditional modal epistemic logics, and hybrid logics combine epistemic modalities with justification terms. The computational complexity of pure justification logics is typically lower than that of the corresponding modal logics. Moreover, the so-called reflected fragments, which still contain complete information about the respective justification logics, are known to be in NP for a wide range of justification logics, pure and hybrid alike. This paper shows that, under reasonable additional restrictions, these reflected fragments are NP-complete, thereby proving a matching lower bound.

The principal result of Justification Logic is the Realization Theorem, which states that behind major epistemic modal logics there are corresponding systems of evidence/justification terms sufficient for reading all provable knowledge assertions as statements about justifications. A knowledge/belief modality is self-referential if there are modal sentences that cannot be realized without using self-referential evidence of type “t is a proof of A(t).” Building on an earlier result that S4 and its justification counterpart LP describe knowledge that is self-referential, we show that the same is true for K4, D4, and T with their justification counterparts whereas for K and D self-referentiality can be avoided. Therefore, no single modal axiom from the standard axiomatizations of these logics is responsible for self-referentiality.

The problem of the identity criteria for proofs can be traced to Hilbert and Prawitz. One of the approaches, which uses the concept of generality of proofs, was suggested in 1968 by Lambek. Following his ideas, we propose a language and a logic to represent Hilbert-style proofs for classical propositional logic by adapting the Logic of Proofs (LP) introduced by Artemov in 1994. We prove that proof polynomials, the objects representing Hilbert derivations in LP, are sufficient to realize all propositional derivations, with or without hypotheses. We also show that proof polynomials respect the ideas of generality and provide an algorithm for determining whether two given proof polynomials represent the same proof. These results naturally extend similar properties of combinatory logic demonstrated by Hindley. The language of LP allows us to formally capture more structure of Hilbert-style proofs. In particular, we show how the well-known phenomenon of proof composition in classical logic manifests itself in the case of Hilbert proofs.

The Hintikka-style modal logic approach to knowledge contains a well-known defect of logical omniscience, i.e., the unrealistic feature that an agent knows all logical consequences of her assumptions. In this paper, we suggest the following Logical Omniscience Test (LOT): an epistemic system E is not logically omniscient if for any valid in E knowledge assertion A of type ‘F is known,’ there is a proof of F in E, the complexity of which is bounded by some polynomial in the length of A. We show that the usual epistemic modal logics are logically omniscient (modulo some common complexity assumptions). We also apply LOT to evidence-based knowledge systems, which, along with the usual knowledge operator K_i(F) (‘agent i knows F’), contain evidence assertions t:F (‘t is a justification for  F’). In evidence-based systems, the evidence part is an appropriate extension of the Logic of Proofs LP, which guarantees that the collection of evidence terms t is rich enough to match modal logic. We show that evidence-based knowledge systems are logically omniscient w.r.t. the usual knowledge and are not logically omniscient w.r.t. evidence-based knowledge.

A system of evidence-based knowledge S4LP was recently proposed by Artemov and Nogina. It combines epistemic modal operator with explicit evidence represented by evidence terms similar to those of Artemov's Logic of Proofs. This logic S4LP and its generalizations promise a new approach to common knowledge and to the logical omniscience problem. In this paper, we show that this logic is PSPACE-complete. Thus adding explicit evidence to S4 does not seem to increase the complexity of the logic.

Explicit modal logic was introduced by S. Artemov. Whereas the traditional modal logic uses atoms ☐F with a possible semantics “F is provable”, the explicit modal logic deals with atoms of form t:F, where t is a proof polynomial denoting a specific proof of a formula F. Artemov found the explicit modal logic LP in this new format and built an algorithm that recovers explicit proof polynomials corresponding to modalities in every derivation in K. Gödel’s modal provability calculus S4. In this paper we study the complexity of LP as well as the complexity of explicit counterparts of the modal logics K, D, T, K4, D4 found by V. Brezhnev. The main result: the satisfiability problem for each of these explicit modal logics belongs to the class Σ^p_2 of the polynomial hierarchy. Similar problem for the original modal logics is known to be PSPACE-complete. Therefore, explicit modal logics have much better upper complexity bounds than the original modal logics.

We provide an epistemic logical language and semantics for the modeling and analysis of byzantine fault-tolerant multi-agent systems. This not only facilitates reasoning about the agents' fault status but also supports model updates for implementing repair and state recovery. For each agent, besides the standard knowledge modality our logic provides an additional modality called hope, which is capable of expressing that the agent is correct (not faulty), and also dynamic modalities enabling change of the agents' correctness status. These dynamic modalities are interpreted as model updates that come in three flavours: fully public, more private, or involving factual change. We provide complete axiomatizations for all these variants in the form of reduction systems: formulas with dynamic modalities are equivalent to formulas without. Therefore, they have the same expressivity as the logic of knowledge and hope. Multiple examples are provided to demonstrate the utility and flexibility of our logic for modeling a wide range of repair and state recovery techniques that have been implemented in the context of fault-detection, isolation, and recovery (FDIR) approaches in fault-tolerant distributed computing with byzantine agents.

Standard epistemic logic is concerned with describing agents' epistemic attitudes given the current set of alternatives the agents consider possible. While distributed systems can (and often are) discussed without mentioning epistemics, it has been well established that epistemic phenomena lie at the heart of what agents, or processes, can and cannot do. Dynamic epistemic logic (DEL) aims to describe how epistemic attitudes of the agents/processes change based on the new information they receive, e.g., based on their observations of events and actions in a distributed system. In a broader philosophical view, this appeals to an a posteriori kind of reasoning, where agents update the set of alternatives considered possible based on their "experiences."

Until recently, there was little incentive to formalize a priori reasoning, which plays a role in designing and maintaining distributed systems, e.g., in determining which states must be considered possible by agents in order to solve the distributed task at hand, and consequently in updating these states when unforeseen situations arise during runtime. With systems becoming more and more complex and large, the task of fixing design errors "on the fly" is shifted to individual agents, such as in the increasingly popular self-adaptive and self-organizing (SASO) systems. Rather than updating agents' a posteriori beliefs, this requires modifying their a priori beliefs about the system's global design and parameters.

The goal of this paper is to provide a formalization of such a priori reasoning by using standard epistemic semantic tools, including Kripke models and DEL-style updates, and provide heuristics that would pave the way to streamlining this inherently non-deterministic and ad hoc process for SASO systems.

We propose a logic of knowledge for impure simplicial complexes. Impure simplicial complexes represent synchronous distributed systems under uncertainty over which processes are still active (are alive) and which processes have failed or crashed (are dead). Our work generalizes the logic of knowledge for pure simplicial complexes, where all processes are alive, by Goubault et al. In our semantics, given a designated face in a complex, a formula can only be true or false there if it is defined. The following are undefined: dead processes cannot know or be ignorant of any proposition, and live processes cannot know or be ignorant of factual propositions involving processes they know to be dead. The semantics are therefore three-valued, with undefined as the third value. We propose an axiomatization that is a version of the modal logic S5. We also show that impure simplicial complexes correspond to certain Kripke models where agents' accessibility relations are equivalence relations on a subset of the domain only. This work extends a WoLLIC 21 conference publication with the same title.

We present an extension incorporating Byzantine agents into the epistemic runs-and-systems framework for modeling distributed systems introduced by Fagin et al. Our framework relies on a careful separation of concerns for various actors involved in the evolution of a message-passing distributed system: the agents' protocols, the underlying computational model, and the adversary controlling Byzantine faulty behavior, with each component adjustable individually. This modularity will allow our framework to be eventually extended to most existing distributed computing models. The main novelty of our framework is its ability to reason about knowledge of Byzantine agents who need not follow their protocols and may or may not be aware of their own faultiness.

We demonstrate the utility of this framework by first reproducing the standard results regarding Lamport's happened-before causal relation and then identifying its Byzantine analog representing the necessary communication structure for attaining knowledge in asynchronous systems with Byzantine faulty agents.

We discuss the choices that the local view suggests for impure simplicial complexes, i.e., complexes where some of the agents may have crashed. We settle on a three-valued semantics with the third value being "undefined" and provide a sound and complete axiomatization by means of a novel canonical simplicial model construction.

Several intuitionistic versions of classical modal logics have been introduced in the literature, by adding modal operators to intuitionistic, instead of classical, propositional logic. We are here interested in logic IS4, which results from combining intuitionistic logic with classical modal logic S4, characterized by reflexive and transitive frames. The logic, proposed by Fischer Servi (1984) and Plotkin and Stirling (1986), has two independent modalities and is interpreted over birelational Kripke models. The problem of decidability of IS4 has been open for almost thirty years, since it has been posed in Simpson’s PhD thesis in 1994. We present a decision procedure for IS4, obtained by defining a proof-search algorithm based on a labelled sequent calculus, which explicitly incorporates the two accessibility relations of Kripke models for the logic. The search algorithm outputs either a proof or a finite countermodel, thus additionally establishing the finite model property for IS4.