Автомат с бесконечным деревом - Infinite-tree automaton

В информатике и математической логике автомат с бесконечным деревом - это конечный автомат, который имеет дело с бесконечными древовидными структурами . Его можно рассматривать как расширение нисходящих автоматов с конечным деревом до бесконечных деревьев или как расширение автоматов с бесконечным числом слов до бесконечных деревьев.

Конечный автомат, работающий на бесконечном дереве, впервые был использован Майклом Рабином для доказательства разрешимости монадической логики второго порядка . Далее было замечено, что древовидные автоматы и логические теории тесно связаны, и это позволяет свести проблемы решения в логике к проблемам решения для автоматов.

Определение

Автоматы с бесконечными деревьями работают на деревьях с метками . Есть много немного разных определений; вот один. (Недетерминированный) автомат с бесконечным деревом - это набор со следующими компонентами. ${\ displaystyle \ Sigma}$${\ Displaystyle A = (\ Sigma, D, Q, q_ {0}, \ delta, F)}$

• ${\ displaystyle \ Sigma}$это алфавит. Этот алфавит используется для обозначения узлов входного дерева.
• ${\ Displaystyle D \ подмножество \ mathbb {N}}$- конечный набор разрешенных степеней ветвления входного дерева. Например, если входное дерево должно быть двоичным деревом, или если , то каждый узел имеет 1, 2 или 3 потомка.${\ Displaystyle D = \ {2 \}}$${\ Displaystyle D = \ {1,2,3 \}}$
• ${\ displaystyle Q}$- конечный набор состояний; начальный.${\ displaystyle q_ {0}}$
• ${\ displaystyle \ delta: Q \ times \ Sigma \ times D \ rightarrow 2 ^ {Q ^ {*}}}$- это отношение перехода, которое отображает состояние автомата , входную букву и степень в набор -наборов состояний.${\ displaystyle q \ in Q}$${\ Displaystyle \ sigma \ in \ Sigma}$${\ displaystyle d \ in D}$${\ displaystyle d}$
• ${\ Displaystyle F \ substeq Q ^ {\ omega}}$ является условием принятия.

Бесконечное дерево автомат детерминированный , если для каждого , и , перехода отношение имеет ровно один -кратное. ${\ displaystyle q \ in Q}$${\ Displaystyle \ sigma \ in \ Sigma}$${\ displaystyle d \ in D}$${\ displaystyle \ delta (q, \ sigma, d)}$${\ displaystyle d}$

Бегать

Интуитивно понятно, что запуск древовидного автомата на входном дереве присваивает состояния автомата узлам дерева таким образом, чтобы удовлетворять отношению перехода автомата. Чуть более формально, запуск древовидного автомата над деревом с меткой- меткой является деревом с меткой-меткой следующим образом. Предположим, что автомат достиг узла входного дерева и в настоящее время находится в состоянии . Пусть узел будет помечен и быть его ветвление степени. Затем автомат выбирает кортеж из набора и клонирует себя в копии. Для каждого одна копия автомата переходит в узел и меняет свое состояние на . Это производит прогон, который представляет собой дерево с меткой. Формально запуск входного дерева удовлетворяет следующим двум условиям. ${\ displaystyle A}$${\ displaystyle \ Sigma}$${\ Displaystyle (Т, В)}$${\ displaystyle Q}$${\ displaystyle (T_ {r}, r)}$${\ displaystyle t}$${\ displaystyle q}$${\ displaystyle t}$${\ Displaystyle \ sigma \ in \ Sigma}$${\ displaystyle d (t)}$${\ displaystyle (q_ {1}, ..., q_ {d (t)})}$${\ Displaystyle \ дельта (д, \ сигма, d (т))}$${\ displaystyle d (t)}$${\ Displaystyle 0 <я \ Leq d (т)}$${\ displaystyle ti}$${\ displaystyle q_ {i}}$${\ displaystyle Q}$${\ displaystyle (T_ {r}, r)}$

• ${\ Displaystyle г (\ эпсилон) = q_ {0}}$.
• Для каждого with существует такое, что для каждого мы имеем и .${\ displaystyle t \ in T_ {r}}$${\ Displaystyle г (т) = д}$${\ Displaystyle (q_ {1}, ..., q_ {d (t)}) \ in \ delta (q, V (t), d (t))}$${\ Displaystyle 0 <я \ Leq d (т)}$${\ displaystyle ti \ in T_ {r}}$${\ Displaystyle г (ti) = q_ {я}}$

Если автомат недетерминирован, на одном входном дереве может быть несколько разных прогонов; для детерминированных автоматов запуск уникален.

Условие приема

В пробеге бесконечный путь помечается последовательностью состояний. Эта последовательность состояний образует бесконечное слово над состояниями. Если все эти бесконечные слова принадлежат условию принятия , то прогон считается принимающим . Интересными условиями приема являются Büchi , Rabin , Streett , Muller и паритет . Если для дерева , помеченного входом , существует принимающий прогон, то входное дерево принимается автоматом. Множество всех принятых деревьев с метками называется языком дерева, которое распознается автоматом дерева . ${\ displaystyle (T_ {r}, r)}$${\ displaystyle F}$${\ displaystyle \ Sigma}$${\ Displaystyle (Т, В)}$${\ displaystyle \ Sigma}$${\ Displaystyle {\ mathcal {L}} (А)}$${\ displaystyle A}$

Выразительная сила условий приема

Недетерминированные автоматы Мюллера, Рабина, Стритта и дерева четности распознают один и тот же набор языков деревьев и, следовательно, обладают одинаковой выразительной способностью. Но недетерминированные древовидные автоматы Бюхи строго слабее, т. Е. Существует язык деревьев, который может быть распознан деревом Рабина, но не может быть распознан никаким древовидным автоматом Бюхи. (Например, не существует древовидного автомата Бюхи, который распознает множество -меченных деревьев, каждый путь которых имеет только конечное число s, см., Например). Кроме того, детерминированные древовидные автоматы (Мюллера, Рабина, Стритта, четность, Бюхи, зацикливание) строго менее выразительны, чем их недетерминированные варианты. Например, не существует детерминированного древовидного автомата, распознающего язык двоичных деревьев, левый или правый дочерний элемент которых отмечен значком в корне . Это резко контрастирует с автоматами на бесконечных словах , где недетерминированные ω-автоматы Бюхи обладают такой же выразительной способностью, как и другие. ${\ Displaystyle \ {а, Ь \}}$${\ displaystyle a}$${\ displaystyle a}$

Языки недетерминированных автоматов Мюллера / Рабина / Стритта / дерева четности замкнуты относительно объединения, пересечения, проекции и дополнения.

Ссылки

• Вольфганг Томас (1990). «Автоматы на бесконечных объектах». В Яне ван Леувене (ред.). Формальные модели и семантика . Справочник по теоретической информатике. B . Эльзевир. С. 133–191.В частности: Часть II « Автоматы на бесконечных деревьях» , стр. 165–185.
• А. Сауди и П. Бониццони (1992). «Автоматы на бесконечных деревьях и рациональное управление». В книге Мориса Нива и Андреаса Подельски (ред.). Древовидные автоматы и языки . Исследования в области компьютерных наук и искусственного интеллекта. 10 . Амстердам: Северная Голландия. С. 189–200.