Монадическая логика второго порядка - Monadic second-order logic

В математическая логика, монадическая логика второго порядка (MSO) является фрагментом логика второго порядка где количественная оценка второго порядка ограничивается количественной оценкой по множествам.[1] Это особенно важно в логика графиков, потому что Теорема Курселя, который предоставляет алгоритмы для вычисления монадических формул второго порядка над графами ограниченного ширина дерева.

Логика второго порядка позволяет количественную оценку более предикаты. Однако MSO - это фрагмент в котором количественная оценка второго порядка ограничена монадическими предикатами (предикатами, имеющими один аргумент). Это часто называют квантификацией «множеств», потому что монадические предикаты эквивалентны по выразительной силе множествам (множеству элементов, для которых предикат истинен).

Вычислительная сложность оценки

Экзистенциальная монадическая логика второго порядка (EMSO) - это фрагмент MSO, в котором все кванторы над множествами должны быть экзистенциальные кванторы вне любой другой части формулы. Кванторы первого порядка не ограничены. По аналогии с Теорема Феджина, согласно которому экзистенциальная (немонадическая) логика второго порядка улавливает именно описательная сложность класса сложности НП, класс проблем, которые могут быть выражены в экзистенциальной монадической логике второго порядка, был назван монадической NP. Ограничение монадической логикой позволяет доказать разделения в этой логике, которые остаются недоказанными для немонадической логики второго порядка. Например, в логика графиков, проверка того, является ли график отключен принадлежит монадическому NP, так как тест может быть представлен формулой, описывающей существование собственного подмножества вершин без ребер, соединяющих их с остальной частью графа; однако дополнительная проблема - проверка связности графа - не принадлежит монадической NP.[2][3] Существование аналогичной пары дополнительных задач, только одна из которых имеет экзистенциальную формулу второго порядка (без ограничения на монадические формулы), эквивалентно неравенству NP и coNP, открытый вопрос вычислительной сложности.

Напротив, когда мы хотим проверить, удовлетворяется ли логическая формула MSO входным конечным дерево, эта проблема может быть решена за линейное время в дереве, переводя булеву формулу MSO в древовидный автомат[4] и оцениваем автомат на дереве. Однако с точки зрения запроса сложность этого процесса обычно неэлементарный.[5] Благодаря Теорема Курселя, мы также можем вычислить логическую формулу MSO за линейное время на входном графе, если ширина дерева графа ограничена константой.

Для формул MSO, которые имеют свободные переменные, когда входные данные представляют собой дерево или имеют ограниченную ширину дерева, эффективные алгоритмы перебора произвести набор всех решений[6], гарантируя, что входные данные предварительно обрабатываются за линейное время и что каждое решение затем создается с задержкой, линейной по размеру каждого решения, то есть с постоянной задержкой в ​​общем случае, когда все свободные переменные запроса являются переменными первого порядка. (т.е. они не представляют собой наборы). Также существуют эффективные алгоритмы подсчета количества решений формулы MSO в этом случае.[7]

Разрешимость и сложность выполнимости

Проблема выполнимости для монадической логики второго порядка в общем случае неразрешима, потому что эта логика включает Логика первого порядка.

Монадическая теория бесконечного полного двоичное дерево, называемый S2S, является разрешимый[8]. Как следствие этого результата, разрешимы следующие теории:

  • Монадическая теория деревьев второго порядка.
  • Монадическая теория второго порядка под преемником (S1S).
  • wS2S и wS1S, которые ограничивают количественное определение конечными подмножествами (слабая монадическая логика второго порядка). Обратите внимание, что для двоичных чисел (представленных подмножествами) сложение можно определить даже в wS1S.

Для каждой из этих теорий (S2S, S1S, wS2S, wS1S) сложность проблемы принятия решения равна неэлементарный[5][9].

Использование выполнимости MSO на деревьях при проверке

Монадическая логика деревьев второго порядка находит применение в Проверка программного обеспечения и, в более широком смысле, Формальная проверка благодаря своей разрешимости и значительной выразительной силе. Реализованы процедуры принятия решения об удовлетворенности[10][11][12]. Такие процедуры использовались для доказательства свойств программ, управляющих связанными структурами данных.[13], как форма Анализ формы (программный анализ) а также для символических рассуждений при проверке оборудования[14].

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

  1. ^ Курсель, Бруно; Энгельфриет, Йост (01.01.2012). Структура графа и монадическая логика второго порядка: теоретико-языковой подход. Издательство Кембриджского университета. ISBN  978-0521898331. Получено 2016-09-15.
  2. ^ Феджин, Рональд (1975), "Монадические обобщенные спектры", Zeitschrift für Mathematische Logik und Grundlagen der Mathematik, 21: 89–96, Дои:10.1002 / malq.19750210112, Г-Н  0371623.
  3. ^ Феджин, Р.; Штокмейер, Л.; Варди, М. Ю. (1993), «О монадической NP против монадической совместной NP», Труды восьмой ежегодной конференции по теории сложности, Институт инженеров по электротехнике и радиоэлектронике, Дои:10.1109 / sct.1993.336544.
  4. ^ Тэтчер, Дж. В .; Райт, Дж. Б. (1968-03-01). «Обобщенная теория конечных автоматов с приложением к проблеме решения логики второго порядка». Математическая теория систем. 2 (1): 57–81. Дои:10.1007 / BF01691346. ISSN  1433-0490.
  5. ^ а б Мейер, Альберт Р. (1975). Парих, Рохит (ред.). «Слабая монадическая теория последователей второго порядка не является элементарно-рекурсивной». Коллоквиум по логике. Конспект лекций по математике. Springer Berlin Heidelberg: 132–154. Дои:10.1007 / bfb0064872. ISBN  9783540374831.
  6. ^ Баган, Гийом (2006). Эсик, Золтан (ред.). «Запросы MSO на древовидных разложимых структурах вычислимы с линейной задержкой». Логика информатики. Конспект лекций по информатике. Springer Berlin Heidelberg. 4207: 167–181. Дои:10.1007/11874683_11. ISBN  9783540454595.
  7. ^ Арнборг, Стефан; Лагергрен, Йенс; Зее, Детлеф (1991-06-01). «Простые задачи для древовидных графов». Журнал алгоритмов. 12 (2): 308–340. Дои:10.1016 / 0196-6774 (91) 90006-К. ISSN  0196-6774.
  8. ^ Рабин, Майкл О. (1969). «Разрешимость теорий и автоматов второго порядка на бесконечных деревьях». Труды Американского математического общества. 141: 1–35. Дои:10.2307/1995086. ISSN  0002-9947.
  9. ^ Стокмейер, Ларри; Мейер, Альберт Р. (2002-11-01). «Космологическая нижняя оценка схемной сложности небольшой логической задачи». Журнал ACM. 49 (6): 753–784. Дои:10.1145/602220.602223. ISSN  0004-5411.
  10. ^ Henriksen, Jesper G .; Дженсен, Якоб; Йоргенсен, Майкл; Кларлунд, Нильс; Пейдж, Роберт; Раухе, Тайс; Сандхольм, Андерс (1995). Brinksma, E .; Cleaveland, W. R .; Ларсен, К. Г .; Маргария, Т .; Штеффен, Б. (ред.). «Мона: монадическая логика второго порядка на практике». Инструменты и алгоритмы построения и анализа систем. Конспект лекций по информатике. Берлин, Гейдельберг: Springer: 89–110. Дои:10.1007/3-540-60630-0_5. ISBN  978-3-540-48509-4.
  11. ^ Федор, Томаш; Холик, Лукаш; Ленгал, Ондржей; Войнар, Томаш (01.04.2019). «Вложенные антицепи для WS1S». Acta Informatica. 56 (3): 205–228. Дои:10.1007 / s00236-018-0331-z. ISSN  1432-0525.
  12. ^ Трайтель, Дмитрий; Нипков, Тобиас (25 сентября 2013 г.). «Проверенные процедуры принятия решений для MSO по словам, основанным на производных от регулярных выражений». Уведомления ACM SIGPLAN. 48 (9): 3–12. Дои:10.1145/2544174.2500612. ISSN  0362-1340.
  13. ^ Мёллер, Андерс; Шварцбах, Майкл И. (2001-05-01). "Механизм логики утверждения указателя". Материалы конференции ACM SIGPLAN 2001 по разработке и реализации языков программирования.. PLDI '01. Сноуберд, Юта, США: Ассоциация вычислительной техники: 221–231. Дои:10.1145/378795.378851. ISBN  978-1-58113-414-8.
  14. ^ Басин, Дэвид; Кларлунд, Нильс (1 ноября 1998 г.). «Символьные рассуждения на основе автоматов в аппаратной проверке». Формальные методы в системном дизайне. 13 (3): 255–288. Дои:10.1023 / А: 1008644009416. ISSN  0925-9856.