PPTL model checking for blockchains
Weijun Zhu · 2020 IEEE 5th Information Technology and Mechatronics Engineering Conference (ITOEC) · 2020
How to model and verify the actions with true concurrency in a blockchain? This is an open issue. To this end, Propositional Projection Temporal Logic (PPTL) is employed to model a blockchain. And then, the existing PPTL model checking algorithm is employed to check some temporal properties in the blockchain. As a result, a new method for modeling and verification of blockchains is formed. Compared with the existing approaches, the new one has ability of deal with true concurrency (synchronization mechanism) in a blockchain, in the process of formal verification.