Проблема динамической топологии в мультиагентных системах
Планирование действий множества агентов (роботов, дронов) сталкивается с серьезным вызовом: необходимо учитывать не только где и когда агент должен находиться, но и как он взаимодействует с другими. Эти взаимодействия описываются топологическими графами (сенсорными, коммуникационными, рабочими), которые могут меняться во времени. Традиционные подходы часто не справляются с такой сложностью, поэтому команда исследователей во главе с Шерил Пол (Sheryl Paul) предложила использовать формализм STL-GO (Spatio-Temporal Logic with Graph Operators).
Два подхода к кодированию: MIP против SMT
Авторы разработали и сравнили два математических метода для решения задачи планирования путей, удовлетворяющих спецификациям STL-GO. Оба метода обладают гарантиями корректности (soundness). Первый метод основан на смешанном целочисленном программировании (MIP), второй — на удовлетворимости теорий (SMT). Предоставлен единый интерфейс для задания ограничений агентов, их топологий и спецификаций, что позволяет легко переключаться между методами.
Результаты бенчмарка: Поиск и спасение (Search-and-Rescue)
Эксперименты проводились на задаче поиска и спасения с использованием беспилотных летательных аппаратов (UAV). Исследователи варьировали размер команды и сложность графов взаимодействий, чтобы оценить масштабируемость и выразительность предложенных кодировок. Ниже приведена сравнительная характеристика подходов:
| Характеристика | MIP (Mixed-Integer Programming) | SMT (Satisfiability Modulo Theory) |
|---|---|---|
| Основной метод | Оптимизация линейных/нелинейных ограничений | Логический вывод с учетом теорий |
| Гарантии | Звуковость (Soundness) | Звуковость (Soundness) |
| Интерфейс | Единый унифицированный интерфейс для спецификаций STL-GO | |
| Ключевая метрика | Выразительность при динамических графовых взаимодействиях | |
Значение для индустрии
Работа, принятая к публикации на конференции Formal Methods for Computer-Aided Design 2026 (FM-CAD 2026), закрывает важный пробел в области формальной верификации мультиагентных систем. Возможность строгого математического описания топологии взаимодействий (например, когда дрон должен оставаться в зоне связи с базой или избегать столкновений с другими дронами в реальном времени) критически важна для применения автономных систем в опасных условиях, таких как тушение пожаров или инспекция промышленных объектов.
Источник: arXiv cs.AI ↗