Abstract
It has been argued in the literature that logics for reasoning about strategic abilities, and in particular coalition logic (CL), are well-suited for verification of properties of smart contracts on a blockchain. Smart contracts, however, can be upgraded by providing a new version of a contract on a new block. In this paper, we extend one of the recent formalisms for reasoning about updating CL models with a temporal modality connecting a newer version of a model to the previous one. In such a way, we make a step towards verification of properties of smart contracts with upgrades. We also discuss some properties of the resulting logic and the complexity of its model checking problem.
Author supplied keywords
Cite
CITATION STYLE
Galimullin, R., & Ågotnes, T. (2023). Coalition Logic for Specification and Verification of Smart Contract Upgrades. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 13753 LNAI, pp. 563–572). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-21203-1_34
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
