Проблема с достижимостью
Достижимость — это фундаментальная проблема, которая возникает в нескольких различных контекстах: с конечным и бесконечным состоянием параллельные системы , вычислительные модели, такие как клеточные автоматы и сети Петри , анализ программ , дискретные и непрерывные системы , критические по времени системы, гибридные системы , системы переписывания , вероятностные и параметрические системы и открытые системы , моделируемые как игры . [1]
В общем случае проблему достижимости можно сформулировать следующим образом: для данной вычислительной системы (потенциально бесконечное состояние) с набором разрешенных правил или преобразований решить, достижимо ли определенное состояние системы из заданного начального состояния системы.
Варианты проблемы достижимости могут возникать в результате дополнительных ограничений на начальные или конечные состояния, особых требований к путям достижимости, а также итеративной достижимости или изменения вопросов на анализ выигрышных стратегий в бесконечных играх или неизбежности некоторой динамики.
Обычно для фиксированного описания системы, заданного в той или иной форме (правила редукции, системы уравнений , логические формулы и т. д.), проблема достижимости состоит в проверке того, можно ли достичь заданного набора целевых состояний, начиная с фиксированного набора начальных состояний. Набор целевых состояний может быть представлен явно или через некоторое неявное представление (например, систему уравнений, набор минимальных элементов относительно некоторого упорядочения состояний). Сложные количественные и качественные свойства часто можно свести к базовым вопросам достижимости. Границы разрешимости и сложности, алгоритмические решения и эффективная эвристика — все это важные аспекты, которые следует учитывать в этом контексте. Алгоритмические решения часто основаны на различных комбинациях стратегий исследования, символических манипуляциях с наборами состояний, свойствах декомпозиции или сведении к задачам линейного программирования , и они часто извлекают выгоду из аппроксимаций, абстракций, ускорений и эвристики экстраполяции. Специальные решения, а также решения общего назначения. Решатели ограничений и механизмы дедукции часто объединяются, чтобы сбалансировать эффективность и гибкость.
Варианты проблем достижимости
[ редактировать ]Конечный явный граф
[ редактировать ]Проблема достижимости в ориентированном графе, описанная явно, является NL-полной. Рейнгольд в статье 2008 года доказал, что проблема достижимости неориентированного графа находится в LOGSPACE. [2]
При проверке модели достижимость соответствует свойству живости.
Конечный неявный граф
[ редактировать ]В планировании , точнее, в классическом планировании, интересно узнать, можно ли достичь состояния из исходного состояния на основе описания действий. Описание действий определяет граф неявных состояний, размер которого экспоненциально зависит от размера описания.
При проверке символьной модели модель (основной граф) описывается с помощью символического представления, такого как двоичные диаграммы решений .
Сети Петри
[ редактировать ]Проблема достижимости в сети Петри разрешима. [3] С 1976 года известно, что эта задача является EXPSPACE-сложной. [4] Есть результаты о том, насколько реализовать эту задачу на практике. [5] В 2018 году было показано, что проблема является неэлементарной . [6] В 2022 году было показано, что он является полным для функции Аккермана временной сложности . [7] [8]
Системы векторного сложения
[ редактировать ]В 2022 году было показано, что достижимость в системах сложения векторов является аккермановской и, следовательно, неэлементарной проблемой . [9] [8]
Открытые проблемы
[ редактировать ]Этот раздел пуст. Вы можете помочь, добавив к нему . ( апрель 2013 г. ) |
Международная конференция по проблемам достижимости (RP)
[ редактировать ]Серия «Международные конференции по проблемам достижимости», ранее известная как « Семинар по проблемам достижимости» , представляет собой ежегодную научную конференцию, которая собирает вместе исследователей из разных дисциплин и слоев общества, интересующихся проблемами достижимости, возникающими в алгебраических структурах, вычислительных моделях, гибридных системах, бесконечных играх, логике. и проверка. Семинар пытается заполнить пробел между результатами, полученными в разных областях, но имеющими общую математическую структуру или концептуальные трудности.
Ссылки
[ редактировать ]- ^ Джорджио Дельзанно, Игорь Потапов (ред.): Проблемы достижимости - 5-й международный семинар, RP 2011, Генуя, Италия, 28–30 сентября 2011 г. Материалы. Конспект лекций по информатике 6945, Springer 2011, ISBN 978-3-642-24287-8
- ^ Рейнгольд, Омер (3 мая 2008 г.). «Ненаправленная связность в пространстве журналов» . omereingold.files.wordpress.com . Архивировано из оригинала 15 июня 2007 г. Проверено 9 декабря 2021 г.
- ^ Майр, Эрнст В. (11 мая 1981 г.). «Алгоритм решения общей проблемы достижимости сети Петри» . Материалы тринадцатого ежегодного симпозиума ACM по теории вычислений - STOC '81 . Нью-Йорк, штат Нью-Йорк, США: Ассоциация вычислительной техники. стр. 238–246. дои : 10.1145/800076.802477 . ISBN 978-1-4503-7392-0 . S2CID 15409115 .
- ^ Липтон, Р. (1976). Проблема достижимости требует экспоненциального пространства . Технический отчет 62. Факультет компьютерных наук Йельского университета.
- ^ Кюнгас, Пип (2005). «Проверка достижимости сети Петри является полиномиальной с оптимальными иерархиями абстракции» . В Цукере, Жан-Даниэль; Сайтта, Лоренца (ред.). Абстракция, переформулировка и аппроксимация . Конспекты лекций по информатике. Том. 3607. Берлин, Гейдельберг: Springer. стр. 149–164. дои : 10.1007/11527862_11 . ISBN 978-3-540-31882-8 .
- ^ Червинский, Войцех; Ласота, Славомир; Лазич, Ранко; Леру, Жером; Мазовецкий, Филип (11 апреля 2019 г.). «Проблема достижимости сетей Петри не элементарна». arXiv : 1809.07115 [ cs.FL ].
- ^ Леру, Жером (февраль 2022 г.). «Проблема достижимости сетей Петри не является примитивно-рекурсивной» . 62-й ежегодный симпозиум IEEE по основам информатики (FOCS) , 2021 г. IEEE. стр. 1241–1252. arXiv : 2104.12695 . дои : 10.1109/FOCS52979.2021.00121 . ISBN 978-1-6654-2055-6 .
- ^ Jump up to: а б Брубейкер, Бен (4 декабря 2023 г.). «Просто кажущаяся проблема дает числа, слишком большие для нашей Вселенной» . Журнал Кванта .
- ^ Червинский, Войцех; Орликовский, Лукаш (2021). Достижимость в системах сложения векторов является полной по Аккерману . 62-й ежегодный симпозиум IEEE по основам информатики (FOCS), 2021 г. arXiv : 2104.13866 .