Consensus protocols are used to coordinate the activity of nodes in a distributed network, ensuring reliability in the face of faulty behaviour by some of the nodes of the network. Originating in fault tolerant flight control systems in avionics, they have more recently become the basis for blockchain and cryptocurrency platforms.
Protocols of this type are conceptually complex, and reasoning about their correctness has been challenging. Formal logics for reasoning about knowledge were shown in the 1980's to provide a helpful level of abstraction for dealing with this complexity, by providing formal representations of concepts such as common knowledge that capture the state of information under which certain actions can be taken. In knowledge-based programs such concepts are used as conditions in conditional statements (e.g, if-statemnents and while-loopps). However, this representation does not tell us how an agent should compute whether an assertion about its knowledge is true, so knowledge-based programs cannot be directly executed. To execute a knowledge-based program, one first needs to find concrete predicates of the agent's local state that are equivalent to the knowledge conditions in the program.
More recently, work on automation of reasoning for logics of knowledge has developed tools such as MCK that can automatically verify that protocols satisfy specifications concerning the knowledge of agents, as well as automatically synthesize concrete predicates implementing the the abstract conditions about knowledge in knowledge-based programs.
In this project, we are investigating the application of MCK to verification and synthesis of knowledge-based programs for fault-tolerant consensus protocols.
Prof. Ron van der Meyden (CSE), Prof. Joseph Y. Halpern (Cornell), Kaya Alpturer (Cornell)
This project is supported by grants from DST (Australia) and AFOSR (USA) under the AFOSR/DST Australia Autonomy Initiative.