Cryptographic protocols are structured sequences of messages that are used for exchanging information in a hostile environment. Many protocols have epistemic goals: a successful run of the protocol is intended to cause a participant to hold certain beliefs. As such, epistemic logics have been employed for the verification of cryptographic protocols. Although this approach to verification is explicitly concerned with changing beliefs, formal belief change operators have not been incorporated in previous work. In this preliminary paper, we introduce a new approach to protocol verification by combining a monotonic logic with a nonmonotonic belief change operator. In this context, a protocol participant is able to retract beliefs in response to new information and a protocol participant is able to postulate the most plausible event explaining new information. Hence, protocol participants may draw conclusions from received messages in the same manner conclusions are drawn in formalizations of commonsense reasoning. We illustrate that this kind of reasoning is particularly important when protocol participants have incorrect beliefs.
We introduce a new semantics for a logic of explicit and implicit beliefs based on the concept of multi-agent belief base. Differently from existing Kripke-style semantics for epistemic logic in which the notions of possible world and doxastic/epistemic alternative are primitive, in our semantics they are non-primitive but are defined from the concept of belief base. We provide a complete axiomatization and a decidability result for our logic.
We formalize reasoning about fuzzy belief and fuzzy common belief, especially incomparable beliefs, in multi-agent systems by using a logical system based on Fitting's many-valued modal logic, where incomparable beliefs mean beliefs whose degrees are not totally ordered. Completeness and decidability results for the logic of fuzzy belief and common belief are established while implicitly exploiting the duality-theoretic perspective on Fitting's logic that builds upon the author's previous work. A conceptually novel feature is that incomparable beliefs and qualitative fuzziness can be formalized in the developed system, whereas they cannot be formalized in previously proposed systems for reasoning about fuzzy belief. We believe that belief degrees can ultimately be reduced to truth degrees, and we call this "the reduction thesis about belief degrees", which is assumed in the present paper and motivates an axiom of our system. We finally argue that fuzzy reasoning sheds new light on old epistemic issues such as coordinated attack problem.
We consider the two-fold problem of representing collective beliefs and aggregating these beliefs. We propose a novel representation for collective beliefs that uses modular, transitive relations over possible worlds. They allow us to represent conflicting opinions and they have a clear semantics, thus improving upon the quasi-transitive relations often used in social choice. We then describe a way to construct the belief state of an agent informed by a set of sources of varying degrees of reliability. This construction circumvents Arrow's Impossibility Theorem in a satisfactory manner by accounting for the explicitly encoded conflicts. We give a simple set-theory-based operator for combining the information of multiple agents. We show that this operator satisfies the desirable invariants of idempotence, commutativity, and associativity, and, thus, is well-behaved when iterated, and we describe a computationally effective way of computing the resulting belief state. Finally, we extend our framework to incorporate voting.