Real-Time Model Checking for Closed-Loop Robot Reactive Planning
2508.19186v1
cs.RO, cs.AI, cs.FL, I.2.9; I.2; D.2.4
2025-08-28
Авторы:
Christopher Chandler, Bernd Porr, Giulia Lafratta, Alice Miller
Резюме на русском
Здесь я приведу подробное резюме структурированным образом, как указано в задании. Однако, так как текст статьи вашего исходного сообщения не предоставлен, я буду использовать предоставленную аннотацию как основу.
## Контекст
Исследование сосредоточено на применении моделирования систем (model checking) для реализации реального времени мульти-шагового планирования и обхода препятствий на реальном автономном роботе. Существующие проблемы в области автономного планирования фокусируются на трудностях в достижении эффективного многошагового планирования с использованием реактивных агентов, которые обычно ограничены одним-двумя шагами планирования. Мотивация заключается в развитии метода, позволяющего роботу действовать в локальном окружении с минимальным вмешательством внешних систем, чтобы обеспечить безопасность и эффективность.
## Метод
Методология основывается на моделировании систем с использованием встроенного, целесообразного алгоритма для реального времени, который генерирует планы на месте, используя "ядро" знаний и внимания, аналогичное природным системам. Техническим решением является дискретизация данных LiDAR в 2D, которая чувствительна к изменениям в локальной среде. Метод реализует планирование с помощью моделирования систем посредством глубокого поиска вперед (depth-first search) для мульти-шагового планирования. Архитектура включает в себя временные системы управления, которые активируются для компенсации локальных динамических возмущений.
## Результаты
Проведенные эксперименты продемонстрировали реальное времени планирование и обход препятствий в сценариях типа cul-de-sac и площадки для игр. Использовались реальные данные LiDAR для съемки окружения. Результаты показали, что метод эффективнее реактивных агентов, которые могут планировать только один шаг вперед. Также были получены неформальные доказательства двух основных свойств: (1) возможность генерации эффективных многошаговых планов для обхода препятствий и (2) улучшение производительности реактивного агента.
## Значимость
Это приложение моделирования систем может быть применено в различных областях, включая безопасность автономных транспортных средств, а также в искусстве и науке для разработки безопасных и удобных автономных систем. Основное преимущество заключается в том, что данный подход обеспечивает безопасность и эффективность в реальном времени, используя минимальные ресурсы. Это может вести к повышению надежности и удобства в разработке автономных роботов, особенно в условиях сложных локальных окружений.
## Выводы
Основные достижения состо
Abstract
We present a new application of model checking which achieves real-time
multi-step planning and obstacle avoidance on a real autonomous robot. We have
developed a small, purpose-built model checking algorithm which generates plans
in situ based on "core" knowledge and attention as found in biological agents.
This is achieved in real-time using no pre-computed data on a low-powered
device. Our approach is based on chaining temporary control systems which are
spawned to counteract disturbances in the local environment that disrupt an
autonomous agent from its preferred action (or resting state). A novel
discretization of 2D LiDAR data sensitive to bounded variations in the local
environment is used. Multi-step planning using model checking by forward
depth-first search is applied to cul-de-sac and playground scenarios. Both
empirical results and informal proofs of two fundamental properties of our
approach demonstrate that model checking can be used to create efficient
multi-step plans for local obstacle avoidance, improving on the performance of
a reactive agent which can only plan one step. Our approach is an instructional
case study for the development of safe, reliable and explainable planning in
the context of autonomous vehicles.