# Distributed Runtime Verification of Metric Temporal Properties for Cross-Chain Protocols

arXiv: https://arxiv.org/abs/2204.09796 · HTML: https://mlsanity.com/paper/2204.09796/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 20 Apr 2022.

## Built on by (most cited first, 1 of 1)

- [FinML-Chain: A Blockchain-Integrated Dataset for Enhanced Financial Machine Learning](https://mlsanity.com/paper/2411.16277/) (2024)

## Abstract (arXiv)

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.