跨链协议度量时态特性的分布式验证
Distributed Runtime Verification of Metric Temporal Properties for Cross-Chain Protocols
摘要：
涉及多个区块链的交易通过跨链协议实现。这些协议基于智能合约，即在区块链上运行的程序，由计算机网络执行。由于智能合约可以在不信任的各方之间自动转移加密货币，电子证券和其他有价值资产的所有权，因此验证智能合约的运行时正确性是一个具有实际意义的问题。这种验证具有挑战性，因为智能合约的执行是时间敏感的，并且不同区块链上的时钟可能无法完全同步。本文描述了一种用于区块链执行的运行时监控方法。首先，我们提出了一个广义的运行时验证技术，验证部分同步分布式计算的度量时序逻辑（MTL），利用有界偏斜时钟同步。其次，我们介绍了一个基于进展的公式重写计划监测\MTL规格采用SMT解决技术和报告的实验结果。
英文摘要：
Transactions involving multiple blockchains are implemented by cross-chain protocols. These protocols are based on smart contracts, programs that run on blockchains, executed by a network of computers. Because smart contracts can automatically transfer ownership of cryptocurrencies, electronic securities, and other valuable assets among untrusting parties, verifying the runtime correctness of smart contracts is a problem of compelling practical interest. Such verification is challenging since smart contract execution is time-sensitive, and the clocks on different blockchains may not be perfectly synchronized. This paper describes a method for runtime monitoring of blockchain executions. First, we propose a generalized runtime verification technique for verifying partially synchronous distributed computations for the metric temporal logic (MTL) by exploiting bounded-skew clock synchronization. Second, we introduce a progression-based formula rewriting scheme for monitoring \MTL specifications which employ SMT solving techniques and report experimental results.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
