%  11-Oct-2008
\documentclass[12pt]{article}
\usepackage{amsmath,amsthm}
\usepackage{russcorr}
\sloppy
\title{Детерминизация ординальных автоматов}
\author{Андрей Мучник
(24.02.1958--18.03.2007)\thanks{Доказательство основного результата
настоящей работы было рассказано автором Н.К.
Верещагину и записано
последним в середине 1980-ых годов. Сам результат был видимо получен
автором в первой половине 1980-ых годов. Введение, составляющее первый
раздел, было добавлено в 2008 году.}}

\newcommand{\too}{\longrightarrow}
%\newcommand{\to}{\rightarrow}
\newcommand{\equ}{\leftrightarrow}
\newcommand{\pair}[1]{\langle #1\rangle}
\newcommand{\perems}[2]{#1_{1},\dots, #1_{#2}}

\newtheorem{theorem}{Теорема}
\newtheorem{lemma}{Лемма}

\begin{document}
\maketitle
\begin{abstract}
В настоящей работе доказано, что
для любого недетерминированного ординального автомата
существует детерминированный автомат,
эквивалентный ему для любых счетных ординалов.
Количество состояний детерминированного автомата оценивается
сверху двойной экспонентой от количества
состояний недетерминированного автомата.
\end{abstract}

\section{Введение}
Словом над данным алфавитом называется конечная последовательность букв
этого алфавита, а  сверхсловом ---  бесконечная последовательность букв.
Существует два вида конечных автоматов, получающих на вход слова
над данным алфавитом: детерминированные, и обобщающие
их, недетерминированные. Как доказано в~\cite{rabin-scott59},
они эквивалентны по силе: для каждого недетерминированного конечного
автомата существует эквивалентный ему детерминированный конечный автомат,
то есть, автомат, допускающий в точности те же слова. При этом,
если недетерминированный автомат имеет $N$ состояний, то
эквивалентный ему детерминированный автомат имеет не более
$2^N$ состояний. Эта оценка не улучшаема: для всех $N$
существует недетерминированный автомат с $N$ состояниями, для которого нет
эквивалентного ему недетерминированного автомата с менее чем
$2^N$ состояниями~\cite{subb}.


Детерминированному конечному автомату можно подать на вход не только слово, но и
сверслово. В результате чтения сверхслова возникает бесконечная
последовательность состояний автомата, называемая ходом автомата на данном
сверхслове. Скажем,
что автомат допускает данное сверхслово, если хотя бы одно
из его заключительных состояний встречается в ходе
бесконечно много раз. Таким образом мы получаем опредение
автоматов Бюхи на сверхсловах~\cite{buchi60,buchi62}.

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

В настоящей работе мы рассматриваем более общий вид
автоматов на сверхсловах  ---
автоматы Мюллера~\cite{muller63}.
Автомат Мюллера задается конечным автоматом на конечных словах
и некоторым семейством подмножеств его множества состояний.
Состояния из этого семейства называются заключительными макросостояниями.
Детерминированный автомат Мюллера допускает сверхслово, если
множество состояний, встречающихся в его ходе на сверхслове
бесконечно много раз, является заключительным макросостоянием.
Для недетерминированных автоматов Мюллера определение
аналогично: автомат допускает сверхслово, если существует
его ход на этом сверслове, для  которого
множество состояний, встречающихся в этом ходе
бесконечно много раз, является заключительным макросостоянием.



Автоматы Мюллера являются обобщением автоматов Бюхи:
можно сказать, что автоматы Бюхи --- это такие автоматы Мюллера, в которых
множество заключительных макросостояний состоит из всех макросостояний,
пересекающихся с некоторым фиксированным макросостоянием (множеством заключительных
состояний автомата Бюхи).
Нетрудно убедиться, однако, что множество сверхъязыков,
допускаемых недетерминированными автоматами Бюхи и Мюллера совпадают.
Для детерминированных автоматов это уже неверно:
детерминированные автоматы Бюхи слабее детерминированных автоматов Мюллера.
Более того,
детерминированные
автоматы Мюллера эквивалентны по силе недетерминированным автоматам Мюллера (а значит
и недетерминированным автоматам Бюхи).
Это доказал Макнотон в работе~\cite{mcn}.
Ввиду важности этой теоремы, впоследствии
было изобретено много разных конструкций детерминированного автомата Мюллера,
эквивалентного данному недетерминированному
автомату (Мюллера или Бюхи)~\cite{rabin72,buchi73,sch73,tb73,%
eilenberg74,choueka74,thomas81,safra88}.
Особый интерес представляет количество состояний детерминированного автомата, как
функция количества состояний исходного
недетерминированного автомата.
Наилучшая оценка получена в работе~\cite{safra88}:
если исходный недетерминированный автомат Бюхи имеет $N$
состояний, то существует эквивалентный ему детерминированный автомат Мюллера
с  $N^{O(N)}$ состояниями. Следствием этого результата является
дважды экспоненциальная оценка количества состояний детерминированного
автомата Мюллера, эквивалентного данному недетерминированному
автомату Мюллера. Действительно, для данного недетерминированного
автомата Мюллера с $N$ состояниями нетрудно построить эквивалентный
недетерминированный автомат
Бюхи с $O(N^22^N)$ состояниями. Эквивалентный ему детерминированный автомат
Мюллера будет иметь $2^{O(N^32^N)}$ состояний.

%Есть и другие виды автоматов на сверхсловах~\cite{rabin69,streett82,el85},
%но мы не будем здесь о них говорить.

Ординальным словом над данным алфавитом
называется любое отображение из некоторого ординала в этот алфавит.
Позднее Бюхи~\cite{buchi65} распространил автоматы Мюллера на
ординальные слова.
(Бюхи не ссылался на работу Мюллера, что видимо означает, что
он пришел к этому понятию независимо.)
В дальнейшем мы будем называть автоматы Мюллера-Бюхи
\emph{ординальными автоматами}.
Детерминированный ординальный автомат --- это детерминированный автомат Мюллера,
в котором дополнительно указана некоторая функция, сопоставляющая каждому
макросостоянию (подмножеству множества состояний) некоторое состояние.
Эта функция определяет состояние автомата, в котором он приступает
к чтению буквы с индексом $\alpha$,
являющимся предельным ординалом. Чтобы определить это состояние,
мы применяем эту функцию к множеству всех состояний, которые
неограниченно часто встречались в ходе до момента $\alpha$.

Недетерминированные ординальные автоматы определяются аналогичным образом.
Целью настоящей работы является доказательство теоремы о детерминизации
для ординальных автоматов в случае счетных ординалов:
для любого недетерминированного
ординального автомата существует детерминированный
ординальный автомат, эквивалентный ему для \emph{любых счетных} ординалов.
%Детерминированный автомат не будет зависеть от ординала.
%Для случая несчетных ординалов, мы не знаем верна ли теорема о детерминизации.
%Мы также не знаем, верно ли это,
%если разрешить автомату зависеть от ординала.

В следующем разделе мы даем определения и формулируем результат.
В разделе~\ref{s:omega} мы демонстрируем метод доказательства на примере
сверхслов. В разделе~\ref{s:ordinal} мы доказываем сам результат.

\section{Определения и формулировка результата}
\emph{Сверхсловом} над алфавитом
$\Sigma$ называется любая бесконечная последовательность
букв $a_1,a_2,a_3,\dots$ алфавита
$\Sigma$ (алфавит предполагается конечным).

\emph{Недетерминированный автомат Мюллера на сверхсловах} над
$\Sigma$ задается конечным множеством состояний $Q$,
среди которых выделено множество \emph{начальных} состояний,
множеством троек вида
$q\stackrel{a}{\to}q'$ (где $q,q'$ состояния, а $a$ буква), называемых
\emph{переходами} автомата, и множеством
\emph{заключительных   макросостояний}
(макростостояниями называется подмножества $Q$).
Автомат называется \emph{детерминированным}, если
начальное состояние единственно и
для любой пары $\pair{q,a}$, состоящей из состояния и буквы,
существует и притом единственное состояние $s$, для которого
тройка $q\stackrel{a}{\to}s$ является переходом автомата.

Пусть задан недетерминированный автомат
на сверхсловах и слово или сверхслово $a_1,a_2,a_3,\dots$.
\emph{Ходом} автомата на нем называется любая бесконечная
последовательность состояний
$q_0,q_1,q_2,q_3,\dots$ такая, что $q_0$ --- начальное состояние автомата и
для всех $i$ тройка
$q_{i-1}\stackrel{a_i}{\to}q_i$
является переходом автомата.
Состояние $q_i$ называется состоянием автомата в момент $i$.
Если автомат детерминирован, то ход на любом сверхслове единствен.
Иначе ходов может быть много или не быть вовсе.
\emph{Предельным  макростоянием} хода автомата на данном сверхслове
называется множество,
состоящее из всех состояний,
встречающихся в ходе бесконечно много раз.
Ход называется \emph{допускающим}, если его предельное макросостояние
заключительно. Сверхслово \emph{допускается} автоматом,
если на нем имеется допускающий ход автомата.
Два автомата называются \emph{эквивалентными}, если они допускают
одни и те же сверхслова.

Теорема Макнотона~\cite{mcn} утверждает, что для любого
автомата на сверхсловах
существует эквивалентный ему детерминированный автомат.
%Мы приводим новое доказательство этого результата, а также
%верхнюю оценку количества состояний детерминированного автомата,
%как функции от количества состояний исходного
%недетерминированного автомата,

%Обобщим понятие сверхслова над  $\Sigma$ следующим образом.
Пусть $\rho$ некоторый ординал. Назовем
$\rho$-словом любое отображение из $\rho$ в $\Sigma$
(каждый ординал равен множеству меньших ординалов).

Теперь определим понятие (недетерминированного) ординального автомата.
Для того, чтобы задать недетерминированный ординальный автомат, надо задать некоторый
недетерминированный автомат Мюллера,
\emph{предельные переходы}  и \emph{заключительные состояния}.
Каждый предельный переход является
парой вида $S\to q$, где $S$ обозначает непустое подмножество $Q$,
а $q$ обозначает некоторое состояние.
(Такие переходы выполняются на предельных
шагах: $S$ здесь обозначает предельное макросостояние
хода на шагах, предшествующих предельному ординалу $\alpha\in \rho$,
а $q$ --- состояние автомата в момент $\alpha$.)
%Таким образом, ординальный автомат задается некоторым автоматом
%на сверхсловах, множеством предельных переходов и множеством
%заключительных состояний.
Никаких ограничений на выбор предельных переходов и заключительных
состояний нет.

\emph{Ходом} ординального автомата на сверхслове
$a:\rho\to\Sigma$ называется любое отображение
$P:\rho\to Q$, удовлетворяющее следующим  двум условиям.\\ \label{items}
(1) Для всех $n\in\rho$ (кроме наибольшего элемента $\rho$, если он существует)
тройка $P(n)\stackrel{a_{n+1}}{\too}P(n+1)$
является переходом автомата.\\
(2)
Для всех
предельных
$\alpha\in \rho$ определим $P_\alpha$ как множество тех
состояний $q$, для которых
множество $\{n<\alpha\mid P(n)=q\}$ не ограничено сверху в $\alpha$
(множество $P_\alpha$ называется \emph{предельным макросостоянием сужения
хода $P$ на}
$\alpha$). Требуется, чтобы пара
$P_\alpha\to P(\alpha)$ являлась переходом автомата для всех
предельных $\alpha\in \rho$.

В пункте (2) следует обратить внимание на то, что мы определяем
предельное макросостояние через неограниченость, а не бесконечность,
множества $P_\alpha$.
Из неограниченности следует бесконечность, но не обратно.

Определим понятие допускающего хода. Предположим сначала, что
ординал  $\rho$ не является предельным и обозначим через
$n$ наибольший элемент $\rho$.
Ход автомата $P$ на $\rho$-слове
называется допускающим, если его последнее состояние $P(n)$
заключительно. Если же ординал $\rho$ предельный, то
ход автомата $P$ на $\rho$-слове
называется допускающим, если его \emph{предельное
макросостояние} $P_\rho$ заключительно.

Ординальный автомат называется \emph{детерминированным}, если
автомат Мюллера, задающий его,
детерминирован, и для каждого непустого множества состояний $S$
существует единственное $q$, для которого пара
$S\to q$ является предельным переходом автомата.
Целью настоящей работы является обобщение теоремы Макнотона на любые счетные
ординалы.



\begin{theorem}             \label{th2}
Для любого недетерминированного ординального автомата
существует детерминированный ординальный автомат,
эквивалентный ему на $\rho$-словах для любого счетного ординала $\rho$.
Если исходный автомат имеет $N$ состояний, то детерминированный
автомат имеет $2^{2^{O(N)}}$ состояний.
\end{theorem}

В оставшейся части работы доказывается эта теорема. Чтобы
легче было понять конструкцию, мы сначала применяем ее к автоматам на
сверхсловах.

\section{Автоматы на сверхсловах}\label{s:omega}

\begin{theorem} \label{th1}
Для любого недетерминированного автомата Мюллера
существует эквивалентный ему детерминированный автомат Мюллера.
Если исходный автомат имеет $N$ состояний, то детерминированный
автомат имеет не более $2^{2^{O(N)}}$ состояний.
\end{theorem}

\begin{proof}
Вспомним, как доказывается теорема о детерминизации
автоматов на конечных словах.
Детерминированный автомат,
прочитав начало $y$ длины $n$ входного слова $x$, хранит множество $Q(n)$,
состоящее из всех последних
состояний ходов исходного (недетерминированного) автомата на слове $y$.
(Будем такие состояния в дальнейшем называть \emph{достижимыми в момент} $n$.)
Зная $n$-ую букву слова $x$ и $Q(n-1)$ можно найти $Q(n)$.
С другой стороны, имея $Q(|x|)$,
мы можем узнать, допускает ли недетерминированный автомат слово $x$.

В случае сверхслов
нам недостаточно этой информации, поскольку
последовательность множеств $Q(0),Q(1),Q(2),\dots$ не определяет однозначно
предельные макросостояния всевозможных ходов.
Допустим сначала, что исходный недетерминированный автомат имеет единственное заключительное
макросостояние $F$.
Зафиксируем произвольное сверхслово
$a_1,a_2,a_3,\dots$.
Будем пары вида $\langle$натуральное число, состояние исходного автомата$\rangle$
называть \emph{точками}.
Проведем от точки $\pair{i,q}$ дуги ко всем точкам
вида $\pair{i+1,s}$ таким, что
автомат имеет переход $q\stackrel{a_{i+1}}{\too}s$.
В результате мы получим ориентированный граф.
Мы будем рассматривать конечные и бесконечные пути в этом графе.
Ходам исходного автомата на сверхслове $a_1,a_2,a_3,\dots$
соответствуют бесконечные пути в этом графе, начинающиеся
в точках вида $\langle$0, начальное состояние$\rangle$.

Пусть $P=(\pair{m,q_m},\pair{m+1,q_{m+1}},\dots,\pair{n,q_{n}})$ ---
произвольный путь в этом графе.
Числа $m,n$ называются \emph{начальным и конечным моментами} пути,
а состояния $q_m$ и $q_n$ --- \emph{начальным и конечным состояниями} пути.

%если существует ход автомата на слове $a_1,a_2,\dots,a_i$,
%заканчивающийся состоянием $q$.
%Пусть $P$ --- произвольная
%функция, определенная на сегменте вида $[m,n]$ множества натуральных
%чисел или сегменте вида $[m,+\infty)$, со значениями в множестве
%состояний.
%Будем называть $P$ \emph{путем}, если $P$ можно доопределить до хода
%автомата на сверхслове
%$a_1,a_2,a_3,\dots$ или его начале.
%Числа $m,n$ называются началом и концом пути,
%а состояния $P(m)$ и $P(n)$ --- начальным и конечным состояниями пути.

Будем называть точку $\pair{m,q}$ достижимой, если
существует путь с началом в некоторой точке
вида $\langle$0, начальное состояние$\rangle$
и концом в точке $\pair{m,q}$.
Пусть $\pair{m,q}$ --- произвольная достижимая точка и $q\in F$.
Сначала мы построим
вспомогательный детерминированный автомат, который читает буквы исходного сверхслова
$a_{m+1},a_{m+2},\dots $ и выясняет, существует ли путь,
который выходит из точки $\pair{m,q}$, проходит только по состояниям
из $F$, причем каждое состояние из $F$ посещает бесконечно много раз.
Для этого определим понятия пучка.
%, а $F$ ---
%произвольное подмножество $Q$.
\emph{Пучком} путей с \emph{начальной точкой} $\pair{m,q}$ называется
множество, состоящее из  всех конечных и бесконечных путей
вида $\pair{m,q},\pair{m+1,q_{m+1}},\pair{m+2,q_{m+2}},\dots$
таких, что все состояния $q_{m+1},q_{m+2}\dots$ принадлежат $F$,
а также сужений таких путей на любые отрезки времени.
%и точка $\pair{k,q_k}$ достижима в графе из точки $\pair{m,q}$
%путем, который проходит только по состояниям из $F$.
%(состояние $q$ может и не принадлежать $F$).
Множество $F$ называется \emph{ограничителем} пучка.
Множество $Q(n)$, состоящее из всех
конечных состояний путей с концом $n$, принадлежащих пучку,
будем называть \emph{тенью пучка в момент} $n$.
То есть, $Q(n)$ состоит из всех состояний
$s$, для которых в пучке имеется путь вида
$\pair{m,q},\pair{m+1,q_{m+1}},\pair{m+2,q_{m+2}},\dots,\pair{n,s}$.
%Пучок с начальной точкой  $\pair{m,q}$ обычно обозначается через $\Pi_{mq}$.

Зафиксируем некоторый линейный
порядок на множестве состояний исходного автомата.
\emph{Накоплением конечного пути}
$\pair{k,q_k},\pair{k+1,q_{k+1}},,\dots,\pair{n,q_n}$
называется наибольшее $c$ такое,
что $q_{n_1}=f_1,\dots,q_{n_c}=f_c$
для некоторых $n_1<\dots<n_c$, где $f_1,\dots,f_c$ ---
первые $c$ состояний из $F$ в зафиксированном порядке на множестве состояний.


Теперь построим упоминавшийся вспомогательный
детерминированный автомат $A_q$.
Этот автомат, читая буквы $a_{m+1},a_{m+2},\dots$,
последовательно вычисляет тени пучка
$Q(m+1),Q(m+2),\dots$, начальная точка которого равна $\pair{m,q}$.
Кроме того, для каждого состояния $s$
из $Q(m+i)$ он хранит его \emph{накопление в пучке} ---
наибольшее накопление путей из пучка
с конечной точкой $\pair{m+i,s}$.
Как только для некоторого $n_1$
накопление всех состояний из $Q(n_1)$
станет максимальным (то есть, равным $|F|$)
и при этом $Q(n_1)$ не пусто,
автомат делает \emph{сброс},
обнуляя все накопления, и продолжает вычислять
$Q(n_1+1),Q(n_1+2),\dots$. Это означает, что
при $n>n_1$ автомат определяет
накопление каждого состояния $s$ из $Q(n)$
как наибольшее накопление путей из пучка с начальным моментом $n_1+1$
и конечной точкой $\pair{n,s}$.
И опять, как только для некоторого $n_2>n_1$ окажется, что
накопление всех состояний из $Q(n_2)$
максимально и  $Q(n_1)$ не пусто, происходит сброс. И так далее.

Таким образом, состояниями автомата $A_q$
являются кортежи вида
$T=\pair{R,i_1,\dots,i_{|R|}}$, где $R$ некоторое множество состояний
исходного недетерминированного
автомата, а $i_j$ --- натуральные числа, не превосходящие $|F|$.
Число $i_j$ называется \emph{накоплением $j$-ого}
(в зафиксированном порядке на $Q$) \emph{состояния} из $R$.
Мы говорим, что состояние автомата $A_q$
имеет \emph{максимальное накопление}, если $R$ непусто и
$i_1=\dots=i_{|R|}=|F|$.
Начальным состоянием является кортеж
$\pair{\{q\},0}$.
\footnote{Нуль
надо заменить на единицу, если $q$ является
наименьшим состоянием из $F$.}
Переходы автомата $A_q$
таковы. Пусть автомат $A_q$ находится в состоянии
$T=\pair{S,i_1,\dots,i_{|S|}}$ и читает букву $a$.
Тогда новое состояние $T'=\pair{S',j'_1,\dots,j'_{|S'|}}$ определяется так.
Множество $S'$ состоит из всех состояний $s\in F$ таких,
что исходный недетерминированный автомат имеет переход
$q\stackrel{a}{\too}s$ для некоторого $q\in S$.
Числа  $j'_1,\dots,j'_{|S'|}$
определяются по следующему правилу.
Если  $T$ имеет максимальное накопление, то накопления всех
состояния $s$ в $S'$ равны $0$
за исключением наименьшего состояния из $F$ (если оно принадлежит $S'$),
накопление которого равно $1$.
Если $T$ не имеет максимального накопления, то накопление
состояния $s$ в $S'$ равно максимуму по всем
переходам $q\stackrel{a}{\too}s$, $q\in R$,
накопления $q$ в $T$. Если оказалось, что так посчитанное накопление
ровно на 1 меньше порядкового номера $s$ в $F$, то накопление
$s$ в $S'$ равно его порядковому номеру в  $F$.

Состояние автомата $A_q$ после прочтения
слова $a_{m+1},a_{m+2},\dots, a_n$ будем называть
\emph{срезом} пучка с начальной точкой $\pair{m,q}$ в момент $n$.
То есть, срезом пучка является его тень вместе с накоплениями всех
состояний из его тени.
Будем говорить, что пучок $\Pi$
\emph{насыщен}, если для бесконечно многих
$n$ срез пучка в момент $n$ имеет максимальное накопление (то, есть
автомат $A_q$ при прочтении сверхслова $a_{m+1},a_{m+2},\dots$
делает бесконечно много сбросов).
%Определим заключительные макросостояния $A_q$ как те, в которых
%содержится хотя бы одно состояние автомата $A_q$ с максимальным накоплением.
%По построению предельное макросостояние хода $A_q$
%на сверхcлове $a_{m+1},a_{m+2},\dots$ заключительно
%тогда и только тогда, когда пучок $\Pi_{m,q}$ имеет бесконечно много сбросов.
%Автоматы вида $A_q$ будет основным компонентами детерминированного автомата,
%который мы построим.
Использование пучков основано на следующей лемме.

\begin{lemma}  \label{l1}
(1) Пусть $P$ --- ход автомата на зафиксированном сверхслове, предельное
макросостояние которого равно $F$.
Для каждого натурального $m$ рассмотрим пучок
$\Pi_m$, начальной точкой которого является точка $\pair{m,P(m)}$.
Тогда для всех достаточно больших $m$
пучок $\Pi_m$ насыщен.

(2) Любой насыщенный пучок содержит бесконечный путь,
предельное макросостояние которого равно $F$.
\end{lemma}

\begin{proof}
(1) Определим отношение
эквивалентности на натуральных числах: $i\sim j$, если
для некоторого $n>i,j$ срезы
пучков $\Pi_i$ и $\Pi_j$  в момент $n$
совпадают. При любом фиксированном $n$,
чем меньше $i$, тем больше
срез пучка $\Pi_i$ в момент $n$.
Поэтому, если $i<j<k$ и $i\sim k$, то все три числа $i,j,k$
эквивалентны.
Количество классов эквивалентности
конечно (не превосходит $2^{|F|}$).\footnote{И даже $|F|+1$.
Действительно,
если бы числа  $i_1<i_2<\dots<i_{|F|+2}$ были попарно неэквивалентны,
то для любого $n$, большего всех этих чисел срезы пучков с
начальными точками $\pair{i_j,P(i_j)}$ образовывали бы
$|F|+2$ различных подмножества $F$, линейно упорядоченных отношением включения.}
Поэтому существует число $k$,
эквивалентное всем б\'ольшим него числам.
Зафиксируем любое такое $k$ и докажем, что для всех $m>k$
пучок $\Pi_m$ насыщен.

Рассуждая от противного допустим, что для некоторого
$m>k$ количество сбросов пучка $\Pi_m$ конечно,
а значит после некоторого момента $i$ сбросов в нем нет.
Зафиксируем любые такие $m,i$.
Поскольку предельное макросостояние  пути $P$ равно $F$,
для некоторого $j>i$ сужение $P[i,j]$ пути
$P$ на сегмент $[i,j]$ имеет максимальное накопление.
Зафиксируем любое такое $j$.
Поскольку $j\sim m$, для некоторого $n>j$ срезы $Q_m(n)$ и
$Q_j(n)$ пучков $\Pi_m$ и $\Pi_j$ в момент $n$ совпадают.
Мы утверждаем, что $n$ является моментом сброса пучка $\Pi_m$
вопреки предположению.
%,что моментов сброса больших $i$ нет.
Для этого рассмотрим
произвольное состояние $s$ из $Q_m(n)$.
Нам надо доказать, что его накопление в момент $n$ максимально.
Поскольку моментов сброса между $i$ и $n$ по предположению нет,
нам достаточно найти путь в пучке, имеющий максимальное накопление,
с начальной точкой $\pair{i,P(i)}$ и конечной точкой $\pair{n,s}$.
Для этого возьмем
путь $P[i,j]$ (он уже имеет максимальное накопление)
и продолжим до точки $\pair{n,s}$. Почему его можно
продолжить до этой точки? Поскольку
$Q_m(n)=Q_j(n)$, состояние $s$ принадлежит также
$Q_j(n)$, а это и означает, что имеется путь в пучке
из точки $\pair{j,P(j)}$ в точку $\pair{n,s}$.

(2) Нам понадобится
лемма Кёнига (любое бесконечное корневое дерево,
в котором каждая вершина имеет лишь конечное число сыновей,
имеет бесконечную ветвь).

Пусть дан пучок $\Pi$ с началом в момент $m$ и бесконечным числом сбросов.
Рассмотрим дерево, вершинами которого являются пути
$P$ из пучка $\Pi$, начинающиеся в момент $m$ и кончающиеся
в точках сброса пучка, и
такие, что промежутки $P$ между любыми последовательными точками сброса
имеют максимальное накопление.
Путь $P$ является сыном пути $S$ если $P$ является продолжением $S$
и конечный момент $P$ есть следующая после конца $S$ точка сброса.
Корнем дерева является путь нулевой длины, состоящий из начальной точки пучка.

Докажем, что это дерево бесконечно. Пусть $n$ --- любая точка
сброса пучка  $\Pi$, а $s$ любое состояние
этого пучка в момент $n$. Докажем, что существует путь
$P$ в дереве с конечной точкой $\pair{n,s}$. Такой
путь можно построить, идя от конца к началу.
Действительно, по условию в пучке существует путь
$S$ с концом в предшествующей $n$ точке сброса в точку
$\pair{n,s}$, имеющий максимальное накопление.
Далее,  в пучке
есть путь
$R$ с концом в начальной точке пути $S$, и началом в предыдущей точке сброса и т.д.
Конкатенация всех этих путей и будет искомым путем $P$.

По лемме Кенига построенное дерево имеет бесконечную ветвь, которая и задает
бесконечный путь в пучке, предельное макросостояние которого равно $F$.
\end{proof}

Теперь мы можем построить детерминированный автомат, эквивалентный исходному
недетерминированному автомату.
По доказанной лемме нам достаточно построить детерминированный автомат $B$,
который допускает данное сверхслово тогда и только тогда, когда
существует насыщенный пучок.

Неформально говоря, автомат $B$, прочтя начало исходного слова длины
$m$, запускает копию автомата $A_q$
для всех достижимых в момент $m$ состояний $q\in F$
(для этого он в каждый момент помнит множество достижимых состояний). Автомат
$B$ хранит последовательность, состоящую из текущих
состояний запущенных копий автомата $A_q$, то есть, в каждый момент
он хранит непустые срезы всех пучков.
Срезы новых пучков записываются в конец
этой последовательности.
Чтобы зафиксировать в каком порядке это делается, скажем что пучок
с начальной точкой $\pair{m,q}$ \emph{меньше} пучка с начальной точкой
$\pair{m',q'}$ если $m<m'$, либо $m=m'$ и $q<q'$.
Срезы пучков будут храниться в порядке возрастания пучков.

Количество пучков бесконечно, поэтому
нам придется выбрасывать срезы некоторых пучков.
А именно, как только срезы двух разных пучков
совпадут, мы вычеркиваем срез большего из них.
Кроме того, автомат вычеркивает срезы, ставшие пустыми.
Таким образом, состояниями детерминированного автомата
$B$ являются кортежи вида $\pair{S,T_1,\dots,T_k}$, где
$S\subset Q$ и $T_i$ различные непустые срезы.
Для  начального состояния автомата $B$ множество
$S$ равно множеству начальных
состояний исходного недетерминированного автомата, $k$ равно мощности $S\cap F$,
а $T_i$ равно начальному состоянию автомата $A_{q_i}$,
где $q_i$ есть $i$-ое состояние из $S\cap F$.
Переходы автомата $B$ определяются так, чтобы он функционировал,
как описано выше. А именно,
состояние, в которое он переходит из состояния
$U=\pair{S,T_1,\dots,T_k}$ при прочтении буквы $a$ определяется
последовательным применением к $U$ трех преобразований:
Обновления, Добавления и Сокращения.

Обновление: заменяем $S$ на множество тех состояний, в которые
исходный автомат может перейти из некоторого состояния
из $S$ при
чтении буквы $a$; затем заменяем каждое $T_i$ на состояние
в которое переходит автомат $A_q$ из $T_i$ при чтении буквы
$a$ (переходы автомата  $A_q$ не зависят от
$q$, поэтому $q$ можно не запоминать).
Обозначим получившееся состояние через
$U'=\pair{S',T'_1,\dots,T'_{k}}$

Добавление: добавляем (в любом порядке)
в конец получившейся в результате обновления
последовательности $U'$ начальные состояния автоматов $A_q$ для
всех $q\in S'\cap F$ в порядке увеличения $q$. Обозначим получившееся состояние через
$U''=\pair{S',T'_1,\dots,T'_{k'}}$

Сокращение: для всех $i\le k'$ вычеркиваем $T'_i$, если оно пусто или
существует $j<i$ для которого $T'_j=T'_i$.


Итак, после прочтения $n$ первых букв данного
сверхслова построенный нами детерминированный автомат
$B$ приходит в состояние, которое содержит:
(1) множество достижимых в момент $n$ состояний исходного (недетерминированного)
автомата и
(2) срезы всех $n$-минимальных пучков, начальные моменты которых не
превосходят $n$ (пучок называется \emph{$n$-минимальным},
если его срез в момент $n$ не пуст и не совпадает со срезом
никакого меньшего пучка).

%Обозначим через $\pair{S(n),T_1(n),\dots,T_{k(n)}(n)}$
%состояние, в которое приходит
%автомат $B$ после прочтения $n$ первых букв данного
%сверхслова.
%По построению для каждого пучка $\Pi$ с начальным моментом $m\le n$
%существует и притом единственное $i\le k(n)$, для которого $T_i(n)$
%есть срез пучка $\Pi$ в момент $n$. Это $i$ мы будем называть
%номером пучка в момент $n$. И обратно, для всех
%$i\le k(n)$ множество $T_i(n)$ есть срез
%некоторого пучка, с началом $m\le n$.

Нам осталось определить заключительные макросостояния
автомата $B$. По Лемме~\ref{l1} исходный автомат допускает
сверхслово тогда и только тогда, когда существует насыщенный пучок.
Поэтому представляется
разумным объявить макросостояние автомата $B$ заключительным,
если оно содержит хотя бы одно состояние $\pair{S,T_1,\dots,T_k}$,
в котором для некоторого $i\le k$ срез $T_i$
имеет максимальное накопление.
\footnote{Забегая вперед, можно сразу заметить, что
это не сработает по следующей причине. Полученный автомат был бы автоматом Бюхи,
а недетерминированные автоматы Мюллера строго сильнее
детерминированных автоматов Бюхи.}
Так определенный детерминированный автомат будет
допускать все сверхслова, допускаемые исходным
недетерминированным автоматом.
Действительно, пусть исходный автомат
допускает данное сверхслово. Тогда по Лемме~\ref{l1} существует
насыщенный пучок $\Pi$.
Обозначим через $i(n)$ номер среза этого пучка (среди хранимых срезов)
в момент $n$.
За счет Сокращения число $i(n)$
может уменьшаться с ростом $n$. Поскольку бесконечно уменьшаться оно
не может, начиная с некоторого
момент оно достигает своего предельного
значения, которое мы обозначим через $i$. Поскольку в пучке  $\Pi$
бесконечно много сбросов, для бесконечно
многих $n$ накопление $i$-ого среза максимально.
А значит в хотя бы одном из состояний $\pair{S,T_1,\dots,T_k}$, встречающееся
в ходе $B$ бесконечно много раз,
$T_{i}$ имеет максимальное накопление.

Однако обратное неверно: построенный автомат может допускать лишние сверхслова.
Чтобы объяснить причину, приведем следующий пример.
Пусть автомат имеет состояния $s<t$ и переходы $s\stackrel{a,b}{\to}s$,
$s\stackrel{a}{\to}t$. Начальное состояние ---
$s$,  а заключительное макросостояние ---
синглетон $\{t\}$. Рассмотрим поведение построенного
автомата на сверхслове $ababab\dots$, которое исходным автоматом отвергается.
Начальное состояние равно
$\pair{s}$  (единственное достижимое состояние есть
$s$, ни одного пучка пока нет).
После чтения первой буквы $a$ детерминированный
автомат переходит в состояние
$\pair{st;t1}$ (достижимые состояния --- $s,t$, и имеется один пучок
с тенью $\{t\}$, причем накопление единственного состояния тени равно 1).
Затем, прочитав букву $b$, автомат приходит в состояние
$\pair{s}$ и далее по циклу
$\pair{st;t1}$,
$\pair{s}$. Таким образом,
состояния  $\pair{st;t1}$,
$\pair{s}$ (и только они) входят в предельное макросостояние хода.
При этом срез $t1$ имеет маскимальное накопление, поэтому предельное макросостояние
заключительно.

Причина ошибки в том, что срез $t1$
хоть и встречается среди срезов бесконечно много раз, однако
не встречается ни в каком фиксированном пучке бесконечное число раз.
Действительно он встречается по одному разу в каждом из пучков
с начальными точками $(1,t), (3,t), (5,t),\dots$.


Чтобы решить эту проблему мы включим  в состав состояния автомата
$B$ некоторую дополнительную информацию, которая позволит в пределе
отсечь ``паразитные'' срезы, встречающиеся
в каждом пучке лишь конечное число раз.
Пусть состояние $\pair{S',T'_1,\dots,T'_{k''}}$ автомата $B$ в момент $n>0$
было получено из его состояния $\pair{S,T_1,\dots,T_k}$
в момент $n-1$ описанным выше способом
с помощью Обновления, Добавления и Сокращения.
Пусть перед процедурой сокращения  состояние автомата $B$ было
равно $\pair{S',T'_1,\dots,T'_{k'}}$.
Назовем \emph{зоной неподвижности срезов
в момент} $n$ наибольшее такое $i$, что при сокращении ни одно
из $T'_1,\dots,T'_i$ не было удалено.
Будем включать в состояние автомата $B$ также и зону неподвижности
(для начального состояния определим
зону неподвижности произвольным образом, скажем, положим равной 0).
Нетрудно изменить переходы автомата $B$ так, чтобы
его состояние в момент $n$ включало в себя и  зону неподвижности
в момент $n$.

Итак, состояниями автомата $B$
являются кортежи вида $\pair{S,j,T_1,\dots,T_k}$, где
$S\subset Q$, $j\le k$ и $T_i$ --- различные срезы.
Как следует определить, какие макросостояния автомата $B$ заключительны?
Для того, чтобы понять это, запустим автомат $B$
на данном сверхслове и назовем \emph{предельной зоной неподвижности} его
хода на этом сверхслове нижний предел зон неподвижности срезов.
Предельную зону неподвижности мы будем обозначать
через $\lim$. Говоря неформально, паразитные срезы --- это те,
номера которых в последовательности хранимых срезов превосходят $\lim$.

Точнее, для каждого пучка $\Pi$ существует
$i\le \lim$, для которого для всех достаточно больших
$n$ срез пучка $\Pi$ в моментов $n$ совпадает
с $i$-ым хранимым срезом в этот момент
(в качестве $i$ надо взять предел при $n\to\infty$ номера среза
пучка $\Pi$ в момент $n$ среди хранимых срезов).
И обратно, для каждого
$i\le \lim$ найдется пучок с этим свойством.
Действительно, зафиксируем любое $n$ такое, что
во все моменты позже $n$ никаких сокращений среди
первых  $\lim$ срезов не происходит. В момент $n$
$i$-ый хранимый срез равен срезу некоторого пучка $\Pi$.
Этот пучок и есть искомый.

Таким образом, исходный автомат
допускает сверхслово тогда и только тогда, когда
хотя бы одно из состояний автомата $B$, встречающееся
в его ходе бесконечно много раз, обладает следующим свойством: для некоторого $i\le \lim$
его $i$-ый срез имеет максимальное накопление.

Заметим, что предельная зона неподвижности
$\lim$ может быть найдена по предельному макросостоянию
$B$ как наименьшая из зон
неподвижности состояний из предельного макросостояния.
Руководствуясь этим, объявим макросостояние автомата $B$
заключительным, если в нем есть состояние
$\pair{S,j,T_1,\dots,T_k}$, в котором
некоторое $T_i$ имеет максимальное накопление, причем
$i$ не превосходит зон неподвижности \emph{всех}
состояний, входящих в это предельное макросостояние.

%Заметим, что построенный автомат уже не является автоматом Бюхи (но конечно, является
%автоматом Мюллера). Если исходный автомат допускает
%данное сверхслово, то по построению автомат $B$ также допускает
%его. Теперь нам нужно убедиться в обратном.

%Пусть ход автомата $B$ на данном сверхслове обладает следующим свойством:
%в нем бесконечное число раз повторяется некоторое  состояние
%$\pair{S,j,T_1,\dots,T_k}$ и
%для некоторого $i$, не превосходящего
%предельной зоны неподвижности этого хода, состояние
%$T_i$ имеет максимальное накопление. Нам нужно доказать, что исходный
%автомат допускает данное сверхслово. Зафиксируем любое
%$n_0$, для которого зона неподвижности всех состояния в ходе после $n_0$
%не меньше $i$.
%Рассмотрим состояние $\pair{S(n_0),j(n_0),T_1(n_0),\dots,T_{k(n_0)}(n_0)}$
%автомата $B$ в момент $n_0$. Состояние $T_i(n_0)$ есть состояние некоторого
%автомата $A_q$, запущенного в некоторый момент $n_1\le n_0$. Более того, поскольку
%для всех моментов $n>n_0$ зона неподвижности включает в себя $T_i(n)$,
%мы можем заключить, что  $T_i(n)$ есть состояние этого же автомата
%в момент $n$. Поскольку состояние $T_i$ имеет максимальное накопление
%и  $T_i(n)=T_i$ для бесконечно многих $n$, пучок
%с начальной точкой $\pair{n_0,q}$ имеет бесконечно много сбросов.
%По Лемме~\ref{l1} недетерминированный автомат допускает данное сверхслово.

Итак, мы доказали теорему в предположении,
что заключительное макросостояние единственно.
В общем случае нужно построить, как описывалось выше, детерминированной
автомат $B_F$ для каждого заключительного макросостояния $F$
и запускать эти автоматы
параллельно. То есть состоянием автомата будет
последовательность, состоящая из множества достижимых состояний
$S$ и  кортежей $\pair{j_F,T_1,\dots,T_{n_F}}$ для каждого
заключительного макросостояния $F$ исходного недетерминированного автомата.
Здесь $T_1,\dots,T_{n_F}$ --- срезы пучков с ограничителем $F$,
а $j_F$ --- зона неподвижности срезов пучков с ограничителем $F$.
Зная предельное макросостояние $U$ построенного автомата, можно найти
и предельное макросостояние всех автоматов $B_F$, как множество
$F$-проекций состояний из $U$.

Осталось оценить количество состояний построенного автомата.
Пусть в исходном недетерминированном автомате $N$ состояний.
Каждое состояние автомата $A_q$ есть кортеж вида
$\pair{R,i_1,\dots,i_{|R|}}$, где $R$ множество состояний,
а числа $i_j$ не превосходят $N$.
Поэтому автомат $A_q$ имеет не более $K=2^{N}N^N=(2N)^N$ состояний.
Каждое состояние $B$ есть
кортеж вида $\pair{S,j,T_1,\dots,T_k}$, где $j\le k$,
$r_i$ --- различные состояния $A_q$, а $S$ множество состояний.
Поэтому количество состояний $B$
не превосходит $2^NK^{1+K}=2^{2^{O(N\log N)}}$.
Это число еще нужно возвести в степень $2^N$ (количество возможных
предельных макросостояний), что не повлияет на порядок.
Однако это число больше объявленного в условии теоремы.

Количество состояний $B$
можно уменьшить следующим образом.
Раньше в процедуре сокращения мы удаляли некоторый
срез, если он совпал с некоторым срезом с меньшим номером. Теперь же
будем исключать срез, у которого первая компонента
(тень) совпала с первой компонентой среза с меньшим номером (а накопления
состояний могут быть разными). В описанной выше конструкции
автомата $B$ все остается без изменения, кроме процедуры сокращения.
После такого изменения, количество состояний $B$ будет оцениваться
как
$
(2^N2^NK^{2^N})^{2^N}=
2^{2^{O(N)}}$.

Надо убедиться, что после этого изменения автомат $B$
допускает то же множество сверхслов, что и до изменения.
В результате изменения не могло появиться новых допускаемых слов:
для любого $i\le \lim$ по-прежнему существует
пучок, у которого начиная с некоторого момента срез совпадает
с $i$-ым хранимым срезом.

С другой стороны, ни одно из допускаемых слов не пропало.
Действительно, если некоторый пучок $\Pi$ насыщен
и в некоторый момент тень пучка
$\Pi$ совпала с тенью некоторого другого пучка
$\Pi'$, то и
пучок $\Pi'$ насыщен: между любыми двумя сбросами
$\Pi$ имеется хотя бы один сброс  $\Pi'$.
\end{proof}

%$$
%2^NK^{2^N}2^N=
%2^N(2N)^{N2^N}2^N=
%2^{2N+N\log N2^N}=
%2^{2N+2^{N+\log N+\log\log N}}=
%2^{2^{O(N)}}.
%$$


\section{Доказательство теоремы о детерминизации ординальных
автоматов}\label{s:ordinal}


%\begin{proof}
Построим сначала
детерминированный автомат, который работает правильно на
всех ординалах вида
$\omega n=\omega+\omega+\dots+\omega$ ($n$ раз).

В доказательстве теоремы~\ref{th1} мы для каждого подмножества
$F$  множества $Q$ построили детерминированный автомат $B_F$,
который допускает те сверхслова, на которых исходный автомат
имеет ход с предельным макросостоянием $F$.

Запустим на начале длины $\omega$ данного
нам сверхслова параллельно для всех $F\subset Q$ автоматы
$B_F$. По предельному макросостоянию полученного автомата
мы сможем найти предельные макросостояния ходов всех
автоматов  $B_F$.
Зная предельные макросостояния ходов автоматов
$B_F$, мы можем найти все возможные предельные макросостояния
$\omega$-ходов исходного автомата на этом начале.
Применяя к ним предельные переходы недетерминированного автомата,
мы сможем найти множество
$S_1$ состояний исходного автомата, достижимых в момент $\omega$.
Больше никакой информации в этот момент нам и не требуется.
Действительно, предельное макросостояние любого хода
на начале длины  $\omega+\omega$ равно предельному макросостоянию
его сужения на второе вхождение $\omega$.

Для каждой пары подмножеств $S,F$ множества $Q$
изменим множество начальных состояний исходного недетерминированного
автомата, сделав его равным $S$, а единственным заключительным макросостоянием
сделаем $F$. Обозначим через
$B_{SF}$ результат детерминизации полученного автомата.
(Нетрудно понять, что автомат $B_{SF}$ получается из $B_F$
изменением начального состояния.)
В момент $\omega$
запустим на сверхслове, полученном сужением исходного сверхслова на второе
$\omega$
параллельно для всех $F$ автоматы $B_{S_1F}$ (где $S_1$
обозначает множество состояний исходного автомата, достижимых в момент $\omega$).
Зная предельные макросостояния ходов этих автоматов, можно
найти  множество $S_2$ всех
состояний исходного автомата, достижимых в момент $\omega2$.
И так далее.
По предельному макросостоянию хода построенного автомата на
всем $\omega n$-сверхслове можно найти
все возможные предельные макросостояния ходов исходного автомата.
Однако уже для ординала
$\omega\times\omega$ такой конструкции недостаточно, поскольку этот ординал
не имеет последнего вхождения $\omega$.


Итак, перейдем к
общему случаю. Пусть фиксированы
%счетный предельный
ординал $\rho$ и $\rho$-слово.
%Будем подмножество $M\subset \rho$ называть неограниченным в $\rho$,
%если в $\rho$ нет ординала, большего всех ординалов из $M$.
Пусть $I$ --- отрезок в ординале $\rho$, то есть подмножество $\rho$,
которое вместе с любыми двумя ординалами содержит и все промежуточные.
Будем называть \emph{$I$-путем} любую
функцию $P$, определенную на $I$
со значениями в множестве
состояний, удовлетворяющую пункту (2) на стр.~\pageref{items}
для всех
$n$ из $I$ (кроме наибольшего элемента)
и  пункту (3) для всех предельных ординалов
$\alpha$ из $I$.
Если $I$ имеет наибольший ординал $n$, то точка
$\pair{n,P(n)}$ называется \emph{конечной точкой} пути.
Точка называется \emph{достижимой},
если она является конечной точкой некоторого
пути, начинающегося в нулевой момент.

Пусть даны достижимая точка $\pair{m,q}$ и $F\subset Q$,
для которых $q\in F$.
\emph{Пучком} путей с \emph{начальной точкой} $\pair{m,q}$
и \emph{ограничителем} $F$ (или $F$-пучком
с начальной точкой $\pair{m,q}$) называется
множество, состоящее из всех путей
с начальной точкой   $\pair{m,q}$, проходящих только
через состояния из $F$,
а также сужений таких путей на произвольные отрезки.
Множество состояний $Q_\Pi(n)$ пучка $\Pi$ в момент $n$ определяется как и раньше,
как множество таких $q$, для которых пучок содержит путь
с конечной точкой $(n,q)$. А точки сброса и накопления путей и
состояний теперь определяются немного сложнее из-за того, что
множество точек сброса может быть не упорядочено по типу $\omega$.
Понятие
точки сброса пучка и накопления состояния в пучке определяются
трансфинитной рекурсией по $n<\rho$:\\
1) накопление $[k,n]$-пути $P$ определяется
как наибольшее $c$ такое,
что $P(n_1)=f_1,\dots,P(n_c)=f_c$
для некоторых $k\le n_1<\dots<n_c\le n$, где $f_1,\dots,f_c$ ---
первые $c$ состояний из $F$ и полуинтервал $[n_1,n)$ не содержит
моментов  сброса пучка;
накопление состояния $q$ в момент $n$ равно наибольшему  из
накоплений путей пучка,  конечная точка которых равна $(n,q)$;\\
2) $n$ является \emph{моментом сброса} пучка, или просто \emph{сбросом},
если его тень в момент $n$ непуста и
накопления всех точек из тени максимальны.
Будем говорить в таком случае, что пучок имеет в момент $n$ \emph{максимальное
накопление}.
Если множество точек сброса пучка, принадлежащих предельному
ординалу $\alpha$, не ограничено в  $\alpha$,
то пучок называется \emph{$\alpha$-насыщенным} или \emph{насыщенным в $\alpha$}.

Теперь установим аналог Леммы~\ref{l1}, позволяющий свести задачу
о путях с данным предельным макросостоянием к задаче о насыщенных пучках.
Пусть $\alpha\le\rho$ --- счетный предельный ординал.

\begin{lemma}  \label{l2}
(1) Пусть дан ход $P$ автомата,
предельное макросостояние которого равно $F$.
Тогда для всех достаточно больших $m\in\alpha$
пучок с начальной точкой $\pair{m,P(m)}$
и ограничителем $F$ является $\alpha$-насыщенным.

(2) Если  пучок $\Pi$ с ограничителем $F$
$\alpha$-насыщен, то он содержит некоторый $[*,\alpha)$-путь,
предельное макросостояние которого равно $F$.
\end{lemma}

\begin{proof}
Утверждение (1) доказывается точно так же, как и для сверхслов.
Счетность $\alpha$ при этом не используется.

Докажем утверждение (2).
Пусть дан пучок с неограниченным множеством сбросов.
Напомним, что раньше мы рассматривали
пути из начальной точки
пучка в точки сброса, сужение
которых на интервал между любыми последовательными точками сброса
имеет максимальное накопление.
На этих путях рассматривалась структура дерева и применялась лемма
Кенига. Теперь это рассуждение не пройдет, поскольку моменты
сброса могут быть не упорядочены по типу натуральных чисел.
Однако, пользуясь счетностью $\alpha$, мы можем выбрать
возрастающую последовательность моментов сброса
$n_1,n_2,\dots$, неограниченную в $\alpha$.
После этого будем рассматривать
пути из начальной точки
пучка в точки пучка в моменты $n_j$, сужение
которых на все интервалы вида $(n_{j-1},n_j]$
имеет максимальное накопление.
Как и раньше, на этих путях вводится структура дерева.
Чтобы количество сыновей каждой вершины было конечным,
для каждого $j$ и каждого состояния  $s$ из пучка в момент $n_j$
отбираем только один
путь с начальным моментом $n_{j-1}+1$ и конечной точкой $\pair{n_j,s}$,
который имеет максимальное накопление.
Конкатенации этих путей и образуют дерево.

Как и раньше доказывается, что дерево бесконечно, поэтому
содержит бесконечный путь. Поскольку множество
$\{n_1,n_2,\dots\}$ не ограничено в $\alpha$,
этот путь является $[m,\alpha)$-путем с предельным макросостоянием $F$.
\end{proof}

Скажем, что два пучка с одним ограничителем \emph{$n$-эквивалентны}, если их
тени в момент $n$ равны.
Для предельних ординалов $\alpha$ назовем
два пучка с одним ограничителем \emph{$\alpha^-$-эквивалентными},
если они $n$-эквивалентны для некоторого $n<\alpha$.

Ввиду Леммы~\ref{l2} можно действовать, как и раньше.
То есть, построить такой автомат, который в момент $n$
для каждого $F\subset Q$ хранит срезы всех $n$-минимальных $F$-пучков
(так называются пучки, которые не являются $n$-эквивалентными
меньшим пучкам) и зону неподвижности $F$-пучков.
Зона неподвижности в предельный момент $\alpha$ определяется
следующим образом: она равна наибольшему такому $j$,
что ни один из первых $j$ $\alpha^-$-минимальных
пучков не является  $\alpha$-эквивалентным некоторому
меньшему пучку. Нетрудно понять, что для непредельных ординалов
это определение равносильно использованному ранее.
%Из определения следует, что
%она всегда не превосходит предела зон неподвижности
%в моменты $n<\alpha$ при $n\to\alpha$,
%но может быть и строго меньше.
Нетрудно также проверить, что
сохраняется основное свойство предельных зон неподвижности: предел
зон неподвижности $F$-пучков при $n\to\alpha$ равен количеству
$\alpha^-$-минимальных $F$-пучков.

Однако этой информации недостаточно для того,
чтобы найти тени пучков, а также
накопления их состояний в предельные моменты времени.
Поясним, в чем здесь трудность. Пусть
автомат $B_F$ прочитал первые $\omega$ букв исходного
ординального слова.
Пусть $\Pi$ --- некоторый $\omega^-$-минимальный пучок
с ограничителем $F$.
Состояния пучка $\Pi$ в момент $\omega$ получаются применением
предельных переходов исходного
недетерминированного автомата ко всем макросостояниям
$G\subset F$, для которых в пучке $\Pi$ есть бесконечный путь,
предельное макросостояние
которого равно $G$. Имеющаяся у нас информация (предельное макросостояние
детерминированного автомата)
позволяет только узнать, есть ли пучке $\Pi$
путь, предельное макросостояние которого равно $F$,
но не позволяет узнать то же самое для собственных подмножеств $F$.
Правда, по предельному макросостоянию автомата $B_G$ мы можем узнать,
есть ли путь с предельным макросостоянием $G$, но мы не знаем,
принадлежит ли хотя бы один из таких путей пучку $\Pi$.
Поэтому надо хранить еще дополнительную информацию, связывающую пучки
с разными ограничителями.

Нам понадодится еще одно новое понятие.
Если начальная точка $\pair{m,q}$ пучка $\Pi'$ с ограничителем
$G\subset F$ принадлежит пучку $\Pi$, то
мы говорим, что $\Pi'$ является \emph{подпучком} пучка $\Pi$,
а накопление состояния $q$ в момент $m$ в пучке
$\Pi$ называем  \emph{накоплением подпучка $\Pi'$ в пучке $\Pi$}
(оно не зависит от момента времени).


Пусть $G$ подмножество $F$ и пусть $\Pi_F$
--- некоторый $n$-минимальный $F$-пучок, а $\Pi_G$ ---
некоторый $n$-минимальный  $G$-пучок.
Будем говорить, что \emph{$\Pi_F$ связан с $\Pi_G$ в момент $n$},
если $\Pi_G$ имеет подпучок, $n$-эквивалентный пучку $\Pi_F$.
Определим \emph{накопление связи $\Pi_F\to \Pi_G$ в момент
$n$} следующим образом. Оно равно $-1$,
если $\Pi_F$ не связан с $\Pi_G$ в момент $n$.
А иначе оно равно максимуму из нуля и
наибольшего из накоплений подпучков $\Pi'_G$ в пучке $\Pi_F$,
которые $n$-эквивалентны пучку $\Pi_G$ и таких, что
на отрезке $[\text{начальный момент } \Pi'_G,n]$ нет сбросов
пучка $\Pi_F$.
Таким образом, накопление неотрицательно тогда и только тогда,
когда $\Pi_F$ связан с $\Pi_G$ в момент $n$.
Будем еще в момент $n$ хранить для всех $F,G,\Pi_F,\Pi_G$ таких, как описано выше,
накопление связи $\Pi_F\to \Pi_G$ в этот момент.
Точнее, если $p_F,p_G$ --- количества
$n$-минимальных  пучков с ограничителями $F,G$,
соответственно, и
$G\subset F$, то для каждой пары чисел $i\le p_F$, $j\le p_G$,
мы храним одно число, которое называем
\emph{накопление связи ($i$-ый $F$-срез $\to j$-ый $G$-срез) в момент $n$}.


Итак, мы определили, каким должно быть состояние детерминированного автомата
в каждый момент $n\in\sigma$. Обозначим это состояние через $U_n$.
Осталось определить его переходы таким образом,
чтобы это в самом деле было выполнено. То есть надо объяснить,
как для непредельных $n$ по $U_{n-1}$ и букве $a_{n}$ можно найти $U_{n}$
и как для предельных ординалов $\alpha$ по
предельному макросостоянию хода $\pair{U_n\mid n<\alpha}$ можно
найти $U_\alpha$

Для непредельных переходов проблем нет: состояния и их накопления
вычисляем как и раньше. Накопления связей
вычисляем так:
при Обновлении накопления связей не меняются,
при добавлении нового $G$-среза $\Pi'=\pair{\{q\},l}$
добавляем также новые связи $\Pi_F\to \Pi'$ для тех $F$-пучков $\Pi_F$,
тень среза которых содержит $q$ и $G\subset F$;
при этом накопление этой связи становится равным накоплению $q$ в
пучке $\Pi_F$.
Кроме того, добавляем
связи $\Pi'\to \Pi''$ для всех вновь добавленных пучков $\Pi',\Pi''$
таких, что их тени состоят из одного и того же состояния.
При сокращении  среза некоторого $G$-пучка $\Pi'_G$ из-за того,
что его тень в момент $n$ совпала с
тенью $n$-минимального $G$-пучка  $\Pi_G$
накопление всех связей вида $\Pi_F\to \Pi_G$
становится равным наибольшему из накоплений связей $\Pi_F\to \Pi_G$
и $\Pi_F\to \Pi'_G$,
а  накопление всех связей $\Pi_G\to \Pi_H$ не изменяется.
Если в пучке $\Pi_F$  происходит сброс, то все неотрицательные накопления
связей вида $\Pi_F\to \Pi_G$  обнуляются (а отрицательные остаются
отрицательными).

Теперь рассмотрим предельные переходы.
Пусть $\alpha$ --- предельный ординал.
Рассмотрим предельное макростостояние $L$ хода
$\pair{U_n\mid n<\alpha}$.
Нам нужно по $L$ найти срезы всех $\alpha$-минимальных
пучков в момент $\alpha$,
зоны неподвижности в момент $\alpha$ и накопления
всех связей в момент $\alpha$.
Зафиксируем некоторое $F$ и объясним сначала, как можно
найти срезы всех $\alpha$-минимальных $F$-пучков в момент $\alpha$
и зону их неподвижности в момент $\alpha$.
Сначала найдем количество $\alpha^-$-минимальных пучков с ограничителем $F$:
оно равно предельной зоне неподвижности $\lim_{F}$
срезов пучков с ограничителем $F$.
Теперь для каждого $i\le \lim_{F}$ и каждого $G\subset F$
выясним, есть ли в $i$-ом (для определенного порядка на пучках)
$\alpha^-$-минимальном $F$-пучке $\Pi_{iF}$
путь с пределом $G$.
Мы утверждаем, что такой путь есть тогда и только тогда,
когда для некоторого $j\le\lim_{G}$
и некоторого состояния $S$ автомата $B_G$,
входящего в предельное макросостояние $L$,
накопление связи ($i$-ый $F$-срез $\to j$-ый $G$-срез) в $S$ неотрицательно
и $j$-ый $G$-срез в $S$ имеет максимальное накопление.

Действительно, если в $i$-ом $\alpha^-$-минимальном пучке $\Pi_{iF}$
с ограничителем $F$ есть путь с пределом $G$, то
по Лемме 2 найдется $\alpha$-насыщенный подпучок $\Pi'_G$ пучка $\Pi_{iF}$,
имеющий ограничитель $G$.
Тогда найдется и $\alpha^-$-минимальный
такой пучок $\Pi'_G$.
Пусть предельный номер этого пучка
равен $j$. Тогда накопление связи
($i$-ый $F$-срез $\to j$-ый $G$-срез) неотрицательно
для всех достаточно больших $n<\alpha$,
а значит накопление этой связи
неотрицательно в каждом состоянии предельного макросостояния,
причем $j$-ый $G$-срез имеет максимальное накопление
хотя бы в одном состоянии из предельного макросостояния $L$.

Обратно, пусть  накопление связи ($i$-ый $F$-срез $\to j$-ый $G$-срез)
неотрицательно в некотором состоянии $S$ из предельного макросостояния,
причем $j$-ый срез с ограничителем $G$ имеет в $S$
максимальное накопление. Следовательно, $j$-ый $n$-миниальный $G$-пучок
$\Pi_{jG}$ насыщен в $\alpha$.
Рассмотрим такое $n$, начиная с которого зоны неподвижности
пучков с ограничителями $F,G$
не меньше $\lim_F,\lim_G$, соответственно.
Тогда в этот момент (и во все большие моменты)
$i$-ый $F$-срез равен срезу пучка $\Pi_{iF}$ и
$j$-ый $G$-срез равен срезу пучка $\Pi_{jG}$.
Если $n$ выбрано достаточно большим, то
$i$-ый $F$-срез связан с $j$-ым $G$-срезом в момент $n$,
то есть имеется связь $\Pi_{iF}\to \Pi_{jG}$. Последнее означает
по условию, что пучок $\Pi_{jG}$
$n$-эквивалентен некоторому подпучку
$\Pi'_G$ пучка $\Pi_{iF}$. Поскольку $\Pi_{jG}$ насыщен в $\alpha$,
таков же и $\Pi'_G$. По Лемме 2 пучок $\Pi'_G$
содержит путь с пределом $G$. Этот путь принадлежит
пучку $\Pi_{iF}$, поскольку $\Pi'_G$ является подпучком пучка
$\Pi_{iF}$.

Теперь для каждого $F$,
каждого $i\le \lim_{F}$ и
для каждого собственного
подмножества $G$ множества $F$
найдем наибольшее из накоплений $[*,\alpha)$-путей
из $i$-ого $\alpha^-$-минимального
пучка $\Pi_{iF}$, имеющих предельное макросостояние $G$.
Фиксируем такие $F,i,G$ и будем это число обозначать через
$s$.

По предельному макросостоянию автомата $B_F$ мы можем
узнать, насыщен $\Pi_{iF}$ в $\alpha$ или нет.
Если он насыщен, то $s=0$.
Мы утверждаем, что в противном случае
число $s$ равно максимальному из накоплений связи
($i$-ый $F$-срез $\to j$-ый $G$-срез) в таких состояниях $S\in L$,
что $j$-ый $G$-срез  имеет максимальное накопление в $S$ и $j\le\lim_G$.
Действительно, пусть для некоторых таких $j,S$
предельное накопления связи ($i$-ый $F$-срез $\to j$-ый $G$-срез)
равно $s'$. Рассмотрим любое
такое $n<\alpha$,
что после момента $n$
зоны неподвижности пучков с ограничителями $F,G$ не меньше
$\lim_F,\lim_G$ и
накопление связи ($i$-ый $F$-срез $\to j$-ый $G$-срез)
в момент $n$ равно
$s'$. Из последнего следует, что $j$-ый $n$-минимальный пучок $\Pi_{jG}$
с ограничителем $G$ $n$-эквивалентен некоторому подпучку
$\Pi'_G$ пучка $\Pi_{iF}$, накопление которого в пучке $\Pi_{iF}$ равно $s'$.
Поскольку пучок $\Pi_{jG}$ насыщен в $\alpha$, таков же и пучок
$\Pi'_G$.
По Лемме 2 пучок $\Pi'_G$
содержит путь с пределом $G$. Этот путь принадлежит
пучку $\Pi_{iF}$, поскольку $\Pi'_G$ является подпучком пучка
$\Pi_{iF}$, и имеет накопление в пучке $\Pi_{iF}$ не меньше $s'$.
Значит $s\ge s'$.

Обратно, в пучке $\Pi_{iF}$ имеется путь $P$
с пределом $G$ и накоплением $s$. Зафиксируем $n$, большее всех
моментов сброса пучка $\Pi_{iF}$ в $\alpha$ и такое, что
сужение пути $P$ на отрезок $[\text{начальный момент }P,n]$
имеет накопление $s$ в пучке $\Pi_{iF}$.
Рассмотрим   пучок $\Pi'_G$, ограничитель которого равен $G$
и начальная точка равна  $(n,P(n))$.
По Лемме 2, если $n$ достаточно большое, то этот пучок является
$\alpha$-насыщенным; кроме того он имеет
накопление $s$ в пучке $\Pi_{iF}$. Пучок $\Pi'_G$ $\alpha^-$-эквивалентен
некоторому $\alpha^-$-минимальному пучку $\Pi_{jG}$.
Поэтому начиная с некоторого момента накопление связи
($i$-ый $F$-срез $\to j$-ый $G$-срез)
будет не меньше $s$ (а именно, с момента, когда тени пучков
$\Pi'_G$ и $\Pi_{jG}$ совпадут и зоны неподвижности будут не меньше
предельных зон неподвижности).

Итак, для каждого $F$
мы нашли количество  $\alpha^-$-минимальных $F$-пучков,
для всех $i$ нашли все возможные предельные макросостояния
$[*,\alpha)$-путей в $i$-ом $\alpha^-$-минимальном $F$-пучке $\Pi_{iF}$.
Кроме того, для каждого возможного предельного макросостояния таких путей мы нашли
максимальное из накоплений (в пучке $\Pi_{iF}$) путей, имеющих это предельное
макросостояние. Ясно, что этой информации вместе с предельными
переходами исходного автомата достаточно, чтобы найти
срезы $\alpha^-$-минимальных пучков
и накопления связей между ними в момент $\alpha$. После этого можно узнать,
какие из  $\alpha^-$-минимальных пучков оказались
$\alpha$-эквивалентными и найти зону неподвижности
$F$-пучков в момент $\alpha$. Добавив новые срезы,
и вычислив накопления связей между ними и старыми
срезами и накопления между новыми срезами,
мы найдем то состояние, которое должен иметь наш автомат в момент $\alpha$.

Оценим количество состояний построенного автомата.
Мы уже оценивали числом $2^{2^{O(N)}}$ количество состояний автомата $B$.
Это число еще надо умножить на количество возможных накоплений пар
пучков. Количество минимальных пучков не превосходит $2^{2N}$ (дли каждого из
$2^N$ разных
$F$ имеется не более $2^{|F|}$ пучков). Для каждого из них надо хранить
одно целое число от $-1$ до $N$, что дает
$(N+2)^{2^{2N}}$. Умножение количества состояний $B$ на это число не изменит
порядка.
%\end{proof}

\begin{thebibliography}{9}

\bibitem{buchi60}
J.R. B\"uchi. Weak second order arithmetic and finite automata.
Zeitschrift f\"ur Math. Logik and Grundlagen Math.,
6 (1960) 66--92.

\bibitem{buchi62}
J.R. B\"uchi. On a decision method in restricted second order
arithmetics. Im E. Nagel et al., editor, Proc. International
Congres on Logic, Methodology amd Philosophy of Science., 1960,
pp. 1--12, Standford Uni. Press, 1962.

\bibitem{buchi65}
J.R. B\"uchi. Decision methods in the theory of ordinals.
Bulletin of AMS, September 1965, Vol. 71, No. 5, pp. 767--770.

\bibitem{buchi73}
J.R. B\"uchi. The monadic
theory of $\omega_1$. In Decidable Theories II, Lecture Notes in Mathematics
328, pp. 1--128, Springer 1973.

\bibitem{choueka74}
Y. Choueka. Theories of automata on $\omega$-tapes: A simplified
approach. Journal of Computer and Systems Sciences 8 (1974) 117--141.

\bibitem{eilenberg74}
S. Eilenberg. Automata, languages, machines, volume A. Academic Press,
1974.

%\bibitem{el85}
%A.E. Emerson and C.L. Lei.
%Modalities for modal checking: Branching
%time strikes back. In Proc. 12th ACM Symp. on Principles of Programming
%Languages, pp. 84--96, 1985.

\bibitem{mcn} R. McNaughton. Testing and generating infinite
sequences by a finite automaton. {\em Information and Control}
{\bf 9:5} (1966) 521--530.

\bibitem{muller63}
D.E. Muller. Infinite sequences and finite automata. In Proc. 4th
IEEE Symp. on Switching Circuits and Logical Design, pp. 3--16, 1963.



\bibitem{rabin69}
M.O. Rabin. Decidability of second-order theories and special
automata on infinite tress. Trans. AMS, 141 (1969) 1--35.

\bibitem{rabin72}
M.O. Rabin. Automata on infinite objects and Church's problem.
Regional Conf. Se. Math., Providence, Rhode Island, 1972.

\bibitem{rabin-scott59}
M.O. Rabin, D. Scott. Finite automata and their decision problems.
IBM J. Research and Development 3 (1959), No. 2, 114--125.
Русский перевод см. Кибернетический сборник, вып. 4 (1962), 56--91.

\bibitem{safra88}
S. Safra. On the complexity of $\omega$-automata. In Proc. 29th
IEEE Symp. on Foundations of Computer Scienece, pp. 318--327, 1988.

\bibitem{sch73}
M.P. Sch\"utzenberger. Sur les relations rationelles functionelles.
In M. Nivat, editor, Automata, Languages and Programming, pp.
103--114. North Holland 1973.

%\bibitem{streett82} R.S. Streett. Propositional dynamic logic of
%looping and converse is elementary decidable. Information and Control,
%54 (1982) 121--141.

\bibitem{subb}
Субботовская

\bibitem{tb73}
Б.А. Трахтенброт, Я.М. Барздинь. Конечные автоматы (поведение
и синтез). М.: Наука. 1970.
Англ. перевод: B.A. Trachtenbrot and Y.M. Barzdin. Finite automata
(behaviour and synthesis). North Holland 1973.

\bibitem{thomas81}
W. Thomas. A combinatorial approach to the theory of $\omega$-automata.
Information and Control 48 (1981) 261--283.

\end{thebibliography}

\end{document}
