Автоматы на бесконечных объектах

Автоматы на бесконечных объектах считывают бесконечные входные данные, такие как бесконечные слова или бесконечные деревья, и принимают их в зависимости от того, какие состояния или переходы посещаются бесконечно часто, обеспечивая математический аппарат для рассуждений о непрерывных, нетерминирующих системах.

Definition

Омега-автомат — это конечный автомат, чьи прогоны бесконечны, с приёмкой, определяемой условием на множестве состояний, посещаемых бесконечно часто; такие автоматы распознают множества бесконечных слов или деревьев, называемые омега-регулярными языками.

Scope

Эта тема охватывает автоматы Бюхи, Мюллера, Рабина и паритетные автоматы над бесконечными словами, условия приёмки, которые их различают, результаты детерминизации и дополнения, автоматы над бесконечными деревьями, а также глубокие связи между этими автоматами, монадической логикой второго порядка и бесконечными играми, используемыми в синтезе и верификации.

Core questions

• Как конечная машина может принимать или отклонять бесконечные входные данные?
• Почему недетерминированные и детерминированные автоматы Бюхи различаются по выразительной мощности?
• Как автоматы над бесконечными объектами связаны с логиками для спецификации поведения системы?
• Что делает дополнение этих автоматов сложным и почему это важно?

Key theories

Приёмка Бюхи и омега-регулярные языки

Автомат Бюхи принимает бесконечное слово, когда некоторое принимающее состояние посещается бесконечно часто, и распознаваемые таким образом языки, омега-регулярные языки, совпадают с теми, которые определимы в монадической логике второго порядка над натуральными числами.

Детерминизация и условие паритета

Недетерминированные автоматы Бюхи, как правило, не могут быть детерминированы без изменения условия приёмки, но конструкция Сафры преобразует их в детерминированные автоматы Рабина или паритетные автоматы, что важно для дополнения и для решения игр.

Clinical relevance

Омега-автоматы являются алгоритмической основой проверки моделей (model checking): реактивная система и свойство темпоральной логики переводятся в автоматы над бесконечными словами, а проверка свойства сводится к тесту на пустоту, что позволяет автоматизировать верификацию аппаратного обеспечения, протоколов и параллельного программного обеспечения.

History

Бюхи ввёл автоматы на бесконечных словах около 1960 года для решения монадической теории второго порядка натуральных чисел, Макнотон показал, как их детерминировать с более строгими условиями приёмки, а Рабин расширил теорию на бесконечные деревья. Эти результаты стали центральными для верификации после того, как темпоральная логика вошла в информатику в конце 1970-х годов.

Key figures

• J. Richard Büchi
• Robert McNaughton
• Michael Rabin
• Shmuel Safra

Seminal works

• thomas1990
• graedel2002

Frequently asked questions

Как машина может принять бесконечные входные данные?

Приёмка определяется не достижением конечного состояния в конце, поскольку конца нет, а тем, какие состояния повторяются. Автомат Бюхи, например, принимает, когда он проходит через обозначенное принимающее состояние бесконечно часто во время своего бесконечного прогона.

Почему эти автоматы важны для верификации?

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