Как мы ускорили анализ дискретных систем в миллион раз и что из этого получилось

Проблема: почему анализ систем — это боль

Представьте, что у вас есть система, которая может находиться в разных состояниях.

Вот примеры из реальной жизни:

• Банк — состояние: обычный пользователь, оператор, администратор

• Автопилот БПЛА — состояние: взлёт, набор высоты, патрулирование, возврат, авария

• Сетевое соединение — состояние: установка связи, передача данных, ошибка, закрытие

• Смарт-контракт — состояние: ожидание, выполнение, заблокирован

• Лифт в небоскрёбе — состояние: этаж, открыты/закрыты двери, есть ли вызовы

Главный вопрос, который постоянно нужно задавать:

«Если система сейчас в состоянии X, может ли она когда-нибудь попасть в состояние Y?»

Зачем это нужно знать:

• Банку — может ли пользователь получить права администратора? (взлом безопасности)

• Атомной станции — может ли реактор попасть в опасный режим? (предотвращение катастрофы)

• БПЛА — может ли миссия войти в аварийный цикл? (спасение дрона)

• Смарт-контракту — можно ли навсегда заблокировать средства? (аудит безопасности)

В чём проблема:

Состояний может быть миллионы, миллиарды. Каждый раз запускать поиск в ширину (BFS) или глубину (DFS) — слишком долго. А если нужно задать миллион таких вопросов? А если система меняется в реальном времени?

Как решают сегодня (классический подход):

// Классика: BFS из начального состоянияbool CanReachBad(int start, bool[] bad, int[][] graph){    var queue = new Queue<int>();    var visited = new bool[n];    queue.Enqueue(start);    visited[start] = true;        while (queue.Count > 0)    {        int u = queue.Dequeue();        if (bad[u]) return true;        foreach (int v in graph[u])            if (!visited[v])            {                visited[v] = true;                queue.Enqueue(v);            }    }    return false;}// Для каждого запроса — новый BFS (очень медленно!)foreach (var start in thousandQueries){    bool answer = CanReachBad(start, badStates, graph);}

Сложность: O(Q × (V+E)). Для миллиона запросов на графе из миллиона вершин — это миллиарды операций.

Идея: а что если один раз всё предвычислить?

Мы рассуждали так:

Если система детерминированная (из каждого состояния ровно один переход), то можно предвычислить таблицы прыжков — как в быстром возведении в степень, но для переходов между состояниями.

Тогда вопрос «где будет система через N шагов?» решается за O(log N) вместо O(N). Ускорение — тысячи раз.

Если система недетерминированная (из состояния несколько выходов), то можно один раз построить обратный индекс достижимости — как поисковый индекс Google, только для графов состояний.

Тогда миллионы запросов «достижимо ли B из A?» отвечаются за O(1) — просто проверкой массива.

Аналогия из жизни:

Без предвычисления — как искать книгу в библиотеке, каждый раз проходя между рядами и просматривая каждую полку.

С предвычислением — как Google: один раз проиндексировали все книги, а потом поиск занимает доли секунды.

Что получилось: платформа SymFSM

Мы построили платформу, которая умеет:

1. Принимать на вход любую дискретную систему — протокол, программу, робота, БПЛА, цифровой двойник

2. Строить индекс — один раз, тяжело (секунды для миллионов состояний)

3. Отвечать на вопросы — миллионы раз, легко (наносекунды)

Типы вопросов:

Как это выглядит в коде:

// Клиент загружает автоматvar e = new SymFsmEngine(stateCount, symbolCount);e.SetTransitionTable(symbol, transitions);e.BuildJumpTables(24);  // один раз построили индекс// Анализ достижимости (недетерминированный случай)var ra = new ReachabilityAnalyzer(succ);bool[] canReachBad = ra.ReverseReachable(badStates);// Миллионы запросов — мгновенноforeach (var start in queries){    bool dangerous = canReachBad[start];  // O(1) — наносекунды!    int distance = dist[start];}

Как мы тестировали: не синтетика, а реальные системы

Мы не использовали случайные графы — они могут давать завышенные результаты. Вместо этого мы взяли реальные системы из промышленности:

• Протоколы: TLS 1.3, QUIC (HTTP/3), HTTP/2, OPC-UA (промстандарт), MQTT (IoT)

• Алгоритмы синхронизации: Peterson, Bakery, Обедающие философы (классика OS)

• Кибербезопасность: Snort (100 000 сигнатур), Suricata, CFG вредоносного ПО

• Компиляторы: DFA регулярных выражений, LR/LALR парсеры, лексеры

• Робототехника: мобильные роботы, манипуляторы, складские рои

• БПЛА: миссии дронов, рои из 10 000 дронов, перехват целей

• Оборона: многоэшелонированная ПВО, радиолокация, РЭБ

• Цифровые двойники: энергосети, ж/д сети, заводы

Всего — 47 бенчмарков, от 5 состояний (MQTT) до 4.8 миллионов состояний (14 философов).

Результаты тестирования

Первые тесты (без RaaS)

Мы начали с простых вещей — проверили ускорение на классических задачах: DFA, Aho-Corasick, сетевые протоколы, Game of Life.

Вот что получилось:

Ключевые выводы первых тестов:

• Детерминированные системы (DFA, Life, протоколы) ускоряются в сотни тысяч раз за счёт jump-таблиц

• Недетерминированные системы (reachability) ускоряются в десятки тысяч раз за счёт амортизации

• Даже на малых размерах (Aho-Corasick, парсеры) ускорение стабильно держится на уровне тысяч раз

Оборонные и аэрокосмические системы

Мы подумали: а что если проверить на том, где каждая миллисекунда на счету? Взяли автопилот БПЛА, системы ПВО, рои дронов.

Результаты:

Что это значит для оборонки:

SymFSM позволяет за миллисекунды доказывать безопасность систем, где раньше требовались часы и дни верификации. Автопилот БПЛА — безопасен (посадка достижима). Радиоканал — опасен (потеря связи из любого состояния). Промышленный контроллер — опасен (авария из любого состояния).

Код проверки автопилота:

// Построение модели автопилота (64 состояния)var flightController = BuildFlightControllerModel();var fsm = new SymFsmEngine(64, 1);fsm.SetTransitionTable(0, flightController);fsm.BuildJumpTables(24);// Проверка: достижима ли посадка через 16 млн шагов?int state = 0;  // INITint finalState = fsm.Jump(0, 16_777_216, 0);bool landingReachable = (finalState & 7) == 7;  // DONE = 7

Сенсорные и трекинговые системы

Потом проверили системы, которые следят за целями — радары, сенсорная интеграция, обнаружение роев.

Результаты:

Код предсказания роя дронов:

// Построение модели роя (1 млн дронов)var swarmModel = BuildSwarmModel(1_000_000);var fsm = BuildFN(swarmModel, 20);// Распределение после миллиона тактовvar distribution = new int[8];for (int i = 0; i < 100000; i++){    int startState = random.Next(1_000_000);    int finalState = fsm.Jump(startState, 1_000_000, 0);    distribution[finalState & 7]++;  // 3 бита фазы}// Результат: ph0:18%, ph1:16%, ph2:11%, ph3:8%, ph4:6%, ph5:10%, ph6:14%, ph7:16%

Reachability-as-a-Service (RaaS) — главный результат

И вот тут началось самое интересное. Мы поняли, что платформа может больше, чем просто ускорять отдельные задачи. Она может стать сервисом, который отвечает на любые вопросы о будущем системы.

Что такое RaaS:

Облачная платформа, которая принимает на вход граф состояний (FSM, протокол, программу, робота, БПЛА), один раз строит индекс, а затем отвечает на миллиарды запросов о достижимости, расстоянии, аттракторах и будущем состоянии.

Четыре типа запросов, которые поддерживает RaaS:

Код RaaS для клиента:

// Клиент загружает автомат (1 млн состояний)var e = new SymFsmEngine(stateCount, symbolCount);e.SetTransitionTable(symbol, transitions);e.BuildJumpTables(24);  // один раз построили индекс// Анализ достижимости (недетерминированный случай)var ra = new ReachabilityAnalyzer(succ);bool[] canReachBad = ra.ReverseReachable(badStates);int[] distanceToBad = ra.ReverseDistance(badStates);// Миллионы запросов — наносекундыforeach (var start in millionQueries){    bool dangerous = canReachBad[start];    int steps = distanceToBad[start];    var attractor = e.GetAttractor(start, 0);    int future = e.Jump(start, 1_000_000_000_000L, 0);}

Результаты RaaS-тестирования (47 бенчмарков):

A. Ядро RaaS (масштабируемость)

B. Model Checking (SPIN) — верификация алгоритмов

C. Сетевые протоколы

D. Кибербезопасность

E. Компиляторы

F. Программный код (CFG, LLVM, Smart Contracts)

G. Робототехника

H. БПЛА и оборона

I. Цифровые двойники

Флагманские демонстрации RaaS

Демо 1: 1 миллиард запросов за 29 секунд

Построили индекс на 4 млн состояний (0.9 секунды). Затем выполнили 1 000 000 000 (миллиард) запросов четырёх типов (Reach, Distance, Attractor, Future).

Результат: 1 миллиард запросов за 28.93 секунды. Пропускная способность — 34.6 млн запросов в секунду. Средняя латенси — 28.9 наносекунды.

// 1 миллиард запросов за 29 секундfor (long q = 0; q < 1_000_000_000; q++){    int a = probe[q & mask];    switch (q & 3)    {        case 0: answer = reach[a]; break;           // Reach        case 1: answer = dist[a]; break;            // Distance        case 2: answer = e.GetAttractor(a, 0); break; // Attractor        case 3: answer = e.Jump(a, 1_000_000, 0); break; // Future    }}

Демо 2: «Поисковик по будущему» (10¹² шагов вперёд)

Отвечаем на вопрос «где будет система через 1 триллион (10¹²) шагов?» — 5.28 млн запросов в секунду. Классический подход физически невозможен: триллион итераций никто не будет ждать.

Демо 3: Универсальный API для всех систем

Один и тот же API запускается на 9 разнородных системах — от DFA до роя дронов. Везде работает одинаково.

Итоговая сводка

Общая статистика

Что мы доказали

1. Детерминированные системы (DFA, протоколы, трекинг) — jump-таблицы дают ускорение до 1.4 миллиона раз. Вопрос «где будет система через 16 млн шагов?» — ответ за 100 наносекунд.

2. Недетерминированные системы (NFA, SPIN, CFG, оборона) — амортизация индекса даёт ускорение до 1.38 миллиона раз. Один предварительный обход (секунды), затем миллионы запросов за наносекунды.

3. RaaS как сервис — миллиард запросов к базе достижимости за 29 секунд. Это первый в мире «поисковик по будущему» для дискретных систем.

4. Универсальность — один API работает на всех типах систем: от протоколов до роёв дронов и ПВО.

Применение в реальном мире

Что дальше? Открыты к сотрудничеству

На данный момент библиотека SymFSM не опубликована в открытых репозиториях (NuGet, GitHub). Это связано с тем, что мы продолжаем активные исследования и доработки платформы.

Мы открыты к сотрудничеству в интересных и значимых проектах, где требуется:

• Верификация критических систем (атомная энергетика, авионика, медицинское ПО)

• Анализ безопасности (банки, блокчейн, кибербезопасность)

• Оптимизация высоконагруженных систем (сети, протоколы, компиляторы)

• Цифровые двойники и промышленная автоматизация

• Оборонные и аэрокосмические проекты

Если у вас есть задача, где:

• Есть конечный автомат, протокол, программа или любая другая дискретная система

• Нужно отвечать на миллионы вопросов о достижимости, расстоянии, циклах

• Классические BFS/DFS/SAT/SMT работают слишком медленно

Будем рады новым гипотезам и экспериментам.