基于合约与时态逻辑的账本管理系统形式化模型

区块链技术的一个关键组成部分是账本，即一种不同于标准数据库、如同公证档案般为任何未来检验保留完整历史交易的数据库。在以太坊等第二代区块链中，账本与智能合约相耦合，实现了金融或商业性质协议相关交易的自动化。智能合约与账本的耦合为去中心化自治组织（DAOs）、首次代币发行（ICOs）和去中心化金融（DeFi）等极具创新性的应用领域提供了技术基础，这些领域将区块链推向了超越加密货币（如比特币等第一代区块链的唯一焦点）的范畴。然而，当前将智能合约作为任意编程构造的实现方式使其易受可被恶意利用的危险漏洞影响，并使其语义偏离法律合约。我们在此提议通过形式化一种建模为有限状态自动机的合约概念来重塑分裂并恢复数据库的可靠性，该合约具有源自面向行动者资源分配编码的明确计算特征，作为基于编程方法的替代方案。为完善工作，我们采用时态逻辑作为抽象查询语言的基础，该语言有效契合账本所保存信息的历史特性。