Author name cluster

Roman Kuznets

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.

9 papers

2 author rows

GandALF Workshop 2023 Workshop Paper

On Two- and Three-valued Semantics for Impure Simplicial Complexes

Hans van Ditmarsch
Roman Kuznets
Rojo Randrianomentsoa

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.

PDF Details DOI

TARK Conference 2021 Conference Paper

Fire!

Krisztina Fruzsa
Roman Kuznets
Ulrich Schmid 0001

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.

Details DOI

FLAP Journal 2021 Journal Article

Justification Logic for Constructive Modal Logic.

Roman Kuznets
Sonia Marin
Lutz Straßburger

We provide a treatment of the intuitionistic 3 modality in the style of justification logic. We introduce a new type of terms, called satisfiers, that justify consistency, obtain justification analogs for the constructive modal logics CK, CD, CT, and CS4, and prove the realization theorem for them.

Details

TARK Conference 2019 Conference Paper

Causality and Epistemic Reasoning in Byzantine Multi-Agent Systems

Roman Kuznets
Laurent Prosperi
Ulrich Schmid 0001
Krisztina Fruzsa

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.

Details DOI

JELIA Conference 2016 Conference Paper

Proving Craig and Lyndon Interpolation Using Labelled Sequent Calculi

Roman Kuznets

Abstract 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.

Details

TARK Conference 2009 Conference Paper

Logical omniscience as a computational complexity problem

Sergei N. Artëmov
Roman Kuznets

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.

Details

CSL Conference 2006 Conference Paper

Logical Omniscience Via Proof Complexity

Sergei N. Artëmov
Roman Kuznets

Abstract 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 \(\mathcal{A}\) of type ‘ Fis known, ’ there is a proof of F in E, the complexity of which is bounded by some polynomial in the length of \(\mathcal{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.

Details

TCS Journal 2006 Journal Article

Making knowledge explicit: How hard it is

Vladimir Brezhnev
Roman Kuznets

Artemov's logic of proofs LP is a complete calculus of propositions and proofs, which is now becoming a foundation for the evidence-based approach to reasoning about knowledge. Additional atoms in LP have form t: F, read as “t is a proof of F” (or, more generally, as “t is an evidence for F”) for an appropriate system of terms t called proof polynomials. In this paper, we answer two well-known questions in this area. One of the main features of LP is its ability to realize modalities in any S 4 -derivation by proof polynomials thus revealing a statement about explicit evidences encoded in that derivation. We show that the original Artemov's algorithm of building such realizations can produce proof polynomials of exponential length in the size of the initial S 4 -derivation. We modify the realization algorithm to produce proof polynomials of at most quadratic length. We also found a modal formula, any realization of which necessarily requires self-referential constants of type c: A ( c ). This demonstrates that the evidence-based reasoning encoded by the modal logic S 4 is inherently self-referential.

Details DOI

CSL Conference 2000 Conference Paper

On the Complexity of Explicit Modal Logics

Roman Kuznets

Abstract 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 \( \mathcal{L}\mathcal{P} \) 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 \( \mathcal{S}4 \). In this paper we study the complexity of \( \mathcal{L}\mathcal{P} \) as well as the complexity of explicit counterparts of the modal logics \( \mathcal{K}, \mathcal{D}, \mathcal{T}, \mathcal{K}\mathcal{A}, \mathcal{D}4 \) found by V. Brezhnev. The main result: the satisfiability problem for each of these explicit modal logics belongs to the class ∑ 2 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.

Details