Аннотация:
Рассматриваются методы анализа и моделирования блокчейн-среды, основанные
на теоретико-автоматных моделях, в первую очередь на
так называемых «автоматах с метками
времени» (timed automata). Также предлагается новая версия автоматов с метками времени, позволяющая избежать некоторых неудобств моделирования с помощью классических автоматов с метками времени, а при моделировании блокчейн-среды
на основе последних приходится использовать
переменные разных типов, действительные и булевы, что вызывает ряд сложностей
как теоретического, так и практического характера. Предлагаемый подход основан
на применении 2-адического анализа, что дает возможность использовать переменные
одного и того же типа, а именно булева.
Ключевые слова:блокчейн-среда, смарт-контракт, автомат с метками времени.