Formal semantics and analysis of tokenomics properties

O. O. Letychevskyi, V. S. Peschanenko, M. Yu. Poltorackiy, Yu.H. Tarasich, M.O. Vinnyk


Today we are witnessing the rapid development of products and services based on blockchain technology. Cryptocurrencies and tokens are becoming an integral part of a person’s daily life. One of the main and, at the same time, the most difficult task for each project is the creation of a self-governing token economy. The violation of properties, such as equilibrium and decentralization, can result in the failure of a project and financial losses.

Using the math and formal methods is a simple and efficient way to create self-sustainable token economies right at the stage of MVP development. Despite the rapid development of tokenomics, its popularity, and the rapid pace of implementing blockchain technology in various business areas, only a small number of works have examined formal models of tokenomics.

In this study, we present an algebraic approach to analyzing the properties of tokenomics. The algebraic modeling approach is implemented within the framework of the Insertion Modeling System (IMS) that was developed at the Glushkov Institute of Cybernetics of the National Academy of Sciences of Ukraine under the guidance of an Academician of the National Academy of Sciences of Ukraine, Professor A.A. Letichevsky. The algebraic modeling methods prove the properties of safety and liveness. Insertion modeling is an approach for modeling complex distributed systems, which is based on the theory of interaction between agents and environments. The modeling algorithm is based on the historical data of exchange trading and the liquidity of tokens - which allows us to make accurate predictions and show possible outcomes.

The interaction of tokenomics agents and their behavior, represented by the equations of behavioral algebra, is considered. The use of the algebraic approach to tokenomics development for the Internet of Things is considered, and the formal representations and methods of property analysis are presented. The obtained results allow us to discuss the possibility of using formal methods in the study of tokenomics.

Prombles in programming 2022; 3-4: 128-138


algebraic modeling; tokenomics; decentralization; tokenomic equilibrium; formal methods; insertion modeling

Full Text:



Letichevsky, A.: Algebra of behavior transformations and its applications. In: Kudryavtsev, V. B., Rosenberg, I. G., (eds.) Structural Theory of Automata, Semigroups, and Universal Algebra, NATO Science Series II. Mathematics, Physics and Chemistry, vol. 207, pp. 241-272. Springer (2005). CrossRef

Letichevsky, A., Gilbert, D.: A Model for Interaction of Agents and Environments. In: Bert, D., Choppy, C., Mosses, P.D. (eds) Recent Trends in Algebraic Development Techniques., WADT 1999, LNCS, vol. 1827, pp.311-328 (1999). CrossRef

Tokenomics formal methods and Tokenomics constructor,

Insertion model creator site,, last accessed 2022/02/16.

Modeling site,

cadCad site: [Accessed: 2022/02/16]

Tokesim site: [Accessed: 2022/02/16]

Guo, C., Zhang, P., Lin, B., Song, J. A: Dual Incentive Value-Based Paradigm for Improving the Business Market Profitability. Blockchain Token Economy. Mathematics 2022, 10, 439. CrossRef

Cong, Lin William, Ye, Li, Neng, Wang: Tokenomics: Dynamic adoption and valuation. The Review of Financial Studies 34(3), 1105-1155 (2021). CrossRef

Pardi, A-L, Paolucci, M. A.: Chemical Analysis of Hybrid Economic Systems-Tokens and Money. Mathematics 9(20):2607 (2021). CrossRef

Letychevskyi, O.: Two-Level Algebraic Method for Detection of Vulnerabilities in Binary Code. In: 10th IEEE International Conference on Intelligent Data Acquisition and Advanced Computing Systems: Technology and Applications (IDAACS), pp. 1074-1077. Metz, France (2019). CrossRef

Letichevsky, A., Letychevskyi, O., Peschanenko, V., and Weigert, T.: Insertion modeling and symbolic verification of large systems. In: Fischer J., Scheidgen M., Schieferdecker I., and Reed R., (eds.). SDL 2015: Model-Driven Engineering for Smart Cities, pp. 3-18, Springer, Cham, Switzerland (2015). CrossRef

Letychevskyi, O., Peschanenko, V., Poltoratskyi, M., Tarasich, Y.: Our Approach to Formal Verification of Token Economy Models, In: ICTERI: International Conference on Information and Communication Technologies in Education, Research, and Industrial Applications, pp. 348-363, Shpringer, Cham (2019). CrossRef

Letychevskyi, O., Peschanenko, V., Poltoratskyi, M., Kovalenko, P., Mogylko, S. Radchenko, V.: Formal Verification of Token Economy Models. In: IEEE Explore Digital Library, IEEE International Conference on Blockchain and Cryptocurrency(ICB), pp. 201- 204, Seoul, Korea (South) (2019). CrossRef



  • There are currently no refbacks.