\documentclass{rtaloop}


\begin{document}
\begin{problem}{Hitoshi Ohsaki}{\cite{ohsaki02rta}}{July 2002}

\begin{abstract}
Are universality and inclusion of AC-recognizable languages decidable?
\end{abstract}

An \emph{AC-tree automaton} as defined by \cite{ohsaki01csl} is given by a
signature $\Sigma$, a set of AC-axioms (that is, associativity and
commutativity) for some function symbols of $\Sigma$, and a set of rewrite
rules $R$ of the form

\begin{eqnarray}
f(q_1,\ldots,q_n) & \rightarrow & q\\
f(q_1,\ldots,q_n) & \rightarrow & f(p_1,\ldots,p_n)\\
q & \rightarrow & p
\end{eqnarray}

where the $q$'s and $p$'s are state symbols. Such an automaton accepts a term
$t$ iff it rewrites $t$ modulo the given AC-axioms to some final state. $L(A)$
denotes the language recognized by an AC-tree automaton $A$; a language $L$ is
called \emph{AC-recognizable} iff $L=L(A)$ for some AC-tree automaton $A$.

Are the following questions decidable?
\begin{itemize}
\item \emph{Universality}: Given an AC-tree automaton $A$, is $L(A)$ equal to
  the set of all ground terms over the given signature $\Sigma$?
\item \emph{Inclusion}: Given AC-tree automata $A$ and $B$, is $L(A)$ a subset
  of $L(B)$?
\end{itemize}

It has been shown \cite{ohsaki02rta} that emptiness of AC-recognizable
languages is decidable. Furthermore, as a consequence of the results of
\cite{dalzilio-lugiez03rta}, universality and inclusion are decidable if
transition rules of the form $f(q_1,\ldots,q_n) \rightarrow f(p_1,\ldots,p_n)$
are not allowed (this is the sub-class of so-called \emph{regular} AC
tree-automata). However, both questions are still open in the general case.

\begin{remark}
The inclusion problem of AC-tree automata is undecidable~\cite{ohsaki05lpar}.
Decidability of universality is still an open question.
\end{remark}
\end{problem}
\end{document}