ﻻ يوجد ملخص باللغة العربية
The notion of knowledge-based program introduced by Halpern and Fagin provides a useful formalism for designing, analysing, and optimising distributed systems. This paper formulates the two phase commit protocol as a knowledge-based program and then an iterative process of model checking and counter-example guided refinement is followed to find concrete implementations of the program for the case of perfect recall semantic in the Byzantine failures context with synchronous reliable communication. We model several different kinds of Byzantine failures and verify different strategies to fight and mitigate them. We address a number of questions that have not been considered in the prior literature, viz., under what circumstances a sender can know that its transmission has been successful, and under what circumstances an agent can know that the coordinator is cheating, and find concrete answers to these questions. The paper describes also a methodology based on temporal-epistemic model checking technology that can be followed to verify the shortest and longest execution time of a distributed protocol and the scenarios that lead to them.
The paper describes an abstraction for protocols that are based on multiple rounds of Chaums Dining Cryptographers protocol. It is proved that the abstraction preserves a rich class of specifications in the logic of knowledge, including specification
We identify a subproblem of the model-checking problem for the epistemic mu-calculus which is decidable. Formulas in the instances of this subproblem allow free variables within the scope of epistemic modalities in a restricted form that avoids embod
The Byzantine agreement problem requires a set of $n$ processes to agree on a value sent by a transmitter, despite a subset of $b$ processes behaving in an arbitrary, i.e. Byzantine, manner and sending corrupted messages to all processes in the syste
Ensuring reliable communication despite possibly malicious participants is a primary objective in any distributed system or network. In this paper, we investigate the possibility of reliable broadcast in a dynamic network whose topology may evolve wh
In this paper, we consider the problem of cross-chain payment whereby customers of different escrows -- implemented by a bank or a blockchain smart contract -- successfully transfer digital assets without trusting each other. Prior to this work, cros