A Logic of Blockchain Updates
Kai Br\"unnler, Dandolo Flumini, Thomas Studer

TL;DR
This paper introduces BCL, a formal logic framework for reasoning about blockchain updates, providing a foundational tool for analyzing blockchain dynamics.
Contribution
It presents the first logic-based model for blockchains, establishing soundness and completeness of BCL with respect to a basic blockchain model.
Findings
BCL is sound and complete for blockchain reasoning.
Provides a formal framework for blockchain updates.
Lays groundwork for further logical analysis of blockchain systems.
Abstract
Blockchains are distributed data structures that are used to achieve consensus in systems for cryptocurrencies (like Bitcoin) or smart contracts (like Ethereum). Although blockchains gained a lot of popularity recently, there is no logic-based model for blockchains available. We introduce BCL, a dynamic logic to reason about blockchain updates, and show that BCL is sound and complete with respect to a simple blockchain model.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, Reasoning, and Knowledge · Distributed systems and fault tolerance · Semantic Web and Ontologies
