Coalition Logic for Specification and Verification of Smart Contract Upgrades
Original version
In: R. Aydoğan, N. Criado, J. Lang, V. Sanchez-Anguix, M. Serramia (eds.), PRIMA 2022: Principles and Practice of Multi-Agent Systems 24th International Conference, Valencia, Spain, November 16–18, 2022, Proceedings, 563–572. https://doi.org/10.1007/978-3-031-21203-1_34Abstract
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.