Uppaal Coshy: Automatic Synthesis of Compact Shields for Hybrid Systems

## Контекст Исследование посвящено проблеме автоматического синтеза безопасных стратегий, называемых **shields**, для гибридных систем. Такие системы объединяют динамики продолжительных данных (continuous) с дискретными отдельными событиями, что делает их моделирование и анализ важными для приложений в самолётах, медицине, автомобилях, и др. В существующих гибридных системах, ошибки могут привести к серьёзным последствиям. Стратегии-shields предотвращают их ошибки за счёт предсказания и предотвращения негативных эффектов, основываясь на моделировании и анализе возможных сценариев. Однако, существующие алгоритмы для синтеза shields имеют проблемы с масштабированием и точностью. Uppaal Coshy предлагает решение для этих проблем, сочетая методы разбиения пространства состояний с эффективными алгоритмами решения задач безопасности. ## Метод Uppaal Coshy работает над **Markov Decision Processes (MDPs)** в пространстве продолжительных состояний. Она делит пространство состояний на **простые части**, и для каждой из них выполняет решение задачи **безопасности (safety game)**. Это решение заключается в том, чтобы обеспечить независимое преодоление двумя игроками — динамическим событием (системной) и стратегическим действием (shield). Uppaal Coshy использует **решение задачи reachability** для достижения безопасного состояния, которая сама по себе является нетривиальной задачей для гибридных систем. Для уменьшения размера хранимых моделей и эффективного хранения решений, Uppaal Coshy включает в себя алгоритм **Caap**, который преобразует решения в **компактные решения в виде деревьев решений (decision tree)**. Это подход использует **аппроксимацию** и **суперпозицию** для уменьшения количества данных, необходимых для хранения. ## Результаты Используя данные, полученные из **собственных экспериментов**, Uppaal Coshy продемонстрировала силу своего подхода в синтезе shields для гибридных систем. Сравнение с другими методами показало, что точность и масштабируемость Uppaal Coshy значительно превышают те, что имеются в существующих системах. Общие результаты показали, что Uppaal Coshy может эффективно решать задачи безопасности для гибридных систем даже при увеличении сложности и размера гибридных моделей. ## Значимость Uppaal Coshy предоставляет **значительное преимущество** в синтезе shields для гибридных систем, которые могут использоваться в приложениях, требующих высокой надежности, таких как автомобили, медицинские устройства, и другие контролируемые системы. Эффективность подхода включает в себя уменьшение размера хранимых моделей без потери точности, что делает Uppaal Coshy привлекательным для реального использования в приложениях,