Skip to main content
SpringerLink
Log in

Our Approach to Formal Verification of Token Economy Models

  • Conference paper
  • First Online:
Information and Communication Technologies in Education, Research, and Industrial Applications (ICTERI 2019)

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 1175))

Abstract

The tokenomic modeling is one of the most efficient approaches for understanding and prediction of its subject’s behavior. There are many tools for simulation modeling of behavior in different domains but there is lack of examples in literature on the usage for tokenomic modeling. The paper considers the formal methods approach for tokenomic modeling. Thus, this article provides a brief description of the technology and the methods and tools developed by the authors for token economy modeling and for the analysis and study of its properties. The article also describes the formalization of the tokenomics model on the example of the SKILLONOMY project and presents the specific and symbolic SKILLONOMY models and its simulation results. The formalization and properties analysis is considered with usage of insertion modeling platform.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Kampakis, S.: Three case studies in tokenomics. J. Br. Blockchain. Assoc. 1(2), 79–82 (2018)

    Google Scholar 

  2. Token Engineering Fundamentals. https://www.slideshare.net/MichaelZargham/tokenengineering-presentation-5-1318

  3. ABM. https://github.com/ShrutiAppiah/Simulating-an-Economy-ABM

  4. Appiah, S.: Decentralized organizations as multi-agent systems - a complex systems perspective. Technical report (2017)

    Google Scholar 

  5. Letichevsky, A., Letychevskyi, O., Peschanenko, V.: Insertion modeling and its applications. Comput. Sci. J. Moldova 24(3), 357–370 (2016)

    MathSciNet  MATH  Google Scholar 

  6. SKILLONOMY. https://SKILLONOMY.org/ru

  7. Letichevsky, A., Gilbert, D.: A model for interaction of agents and environments. In: Bert, D., Choppy, C., Mosses, P.D. (eds.) WADT 1999. LNCS, vol. 1827, pp. 311–328. Springer, Heidelberg (2000). https://doi.org/10.1007/978-3-540-44616-3_18

    Chapter  Google Scholar 

  8. Baranov, S., Jervis, C., Kotlyarov, V., Letichevsky, A., Weigert, T.: Leveraging UML to deliver correct telecom applications. In: Lavagno, L., Martin, G., Selic, B. (eds.) UML for Real: Design of Embedded Real-Time Systems, pp. 323–342. Kluwer Academic Publishers, Amsterdam (2003)

    Google Scholar 

  9. Kapitonova, J., Letichevsky, A., Volkov, V., Weigert, T.: Validation of embedded systems. In: Zurawski, R. (ed.) The Embedded Systems Handbook. CRC Press, Miami (2005)

    MATH  Google Scholar 

  10. Letichevsky, A.A., et al.: System specification with basic protocols. Cybern. Syst. Anal. 41(4), 479–493 (2005)

    Article  MathSciNet  Google Scholar 

  11. Omega: a solver for quantifier-free problems in Presburger Arithmetic. https://coq.inria.fr/refman/addendum/omega.html

  12. CVC3. https://cs.nyu.edu/acsys/cvc3/

  13. Z3Prover. https://github.com/Z3Prover/z3

  14. Mathsat. http://mathsat.fbk.eu/

  15. ITU-T Recommendation, Z.151, User Requirements Notation (URN) – Language definition. https://www.itu.int/rec/T-REC-Z.151/en

  16. Letichevsky, A., Kapitonova, J., Letichevsky Jr., A., Volkov, V., Baranov, S., Weigert, T.: Basic protocols, message sequence charts, and the verification of requirements specifications. Comput. Netw. 49(5), 661–675 (2005)

    Article  Google Scholar 

  17. Gruda AI BV. https://www.garuda.ai

  18. Letichevsky, A.A., et al.: Insertion modeling in distributed system design. Probl. Program. 4, 13–38 (2008)

    Google Scholar 

  19. APS & IMS. https://www.apsystem.org.ua

  20. Letychevskyi, O., Peschanenko, V., Radchenko, V., Poltoratskyi, M., Tarasich, Yu.: Formalization and algebraic modeling of tokenomics projects. In: Proceedings of the 15th International Conference on ICTERI, Workshops, Kherson, Ukraine, vol. 2, pp. 577–584 (2019)

    Google Scholar 

Download references

Acknowledgements

We would like to thank the company garuda.ai [17] for the opportunity to work with the platform for modeling, formal verification and testing of Blockchain/DLT systems behavior and cybersecurity research for our research and experiments in the modeling area. We are also grateful to the Glushkov Institute of Cybernetics of NAS of Ukraine for the theoretical and practical results in the field of verification that were used as a basis for our studies of formalization and algebraic modeling in the tokenomics projects area and to the Kherson State University for the active supporting of Insertion Modeling System.

Author information

Authors and Affiliations

  1. Garuda AI V.B., Het Poortgebouw, Beech Avenue 54-62, 1119 PW, Schiphol, The Netherlands

    Oleksandr Letychevskyi & Volodymyr Peschanenko

  2. Kherson State University, Universytets’ka St. 27, Kherson, 73000, Ukraine

    Maksym Poltoratskyi & Yuliia Tarasich

Authors
  1. Oleksandr Letychevskyi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Volodymyr Peschanenko
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Maksym Poltoratskyi
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Yuliia Tarasich
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Maksym Poltoratskyi .

Editor information

Editors and Affiliations

  1. Zaporizhzhia National University, Zaporizhzhia, Ukraine

    Vadim Ermolayev

  2. Université Cote d’Azur, Nice, France

    Frédéric Mallet

  3. University of Warmia and Mazury in Olsztyn, Olsztyn, Poland

    Vitaliy Yakovyna

  4. University of Klagenfurt, Klagenfurt am Wörthersee, Austria

    Heinrich C. Mayr

  5. Kherson State University, Kherson, Ukraine

    Aleksander Spivakovsky

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Letychevskyi, O., Peschanenko, V., Poltoratskyi, M., Tarasich, Y. (2020). Our Approach to Formal Verification of Token Economy Models. In: Ermolayev, V., Mallet, F., Yakovyna, V., Mayr, H., Spivakovsky, A. (eds) Information and Communication Technologies in Education, Research, and Industrial Applications. ICTERI 2019. Communications in Computer and Information Science, vol 1175. Springer, Cham. https://doi.org/10.1007/978-3-030-39459-2_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-39459-2_16

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-39458-5

  • Online ISBN: 978-3-030-39459-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation