Resumen
In this paper, we continue the topic related to the special binary relation on the set of formal languages (considered primarily on the set of iterations of nonempty finite languages); this is so called equivalence relation at infinity. We have formulated a simpler binary relation in a variety of languages (i.e. the covering relation), the double use of which is equivalent to the use of the equivalence relation at infinity. After that, we considered the algorithm for verifying the implementation of the coverage relation, and identified the auxiliary objects used to prove the correctness of this algorithm. One such object is an infinite iterative tree. In the infinite iterative trees considered, we combine the equivalent states, obtaining in fact a deterministic finite automaton. We have defined a specific such automaton for two given finite languages; this is so called primary automaton, PRI. It is deterministic, defined on sets of words, and each of these sets is a subset of the set of prefixes of the second of the given languages. After that, we define some variants of special nondeterministic automata corresponding to it, describing in fact the construction of this iterative morphism tree. We introduce a completely different object (i.e., a simplified primary automaton, NSPRI), which also describes the construction of an iterative morphism tree, but is defined not on sets of words, but on words. The main idea of the proof of the fact, that the algorithm for constructing a finite automaton for checking the equality of infinite iterations of two finite languages is polynomial is as follows. It is natural to construct a deterministic automaton for this problem, and each state of such deterministic automaton describes the whole set of possible prefixes remaining from various decompositions of the word (this is decompositions of the morphism of the iteration of the first given finite language according to the words of the second given finite language). However, in doing so, we are working with many sets of possible prefixes, which makes it impossible for the algorithm to be polynomial. Therefore, we construct a nondeterministic automaton defined simply on the set of possible prefixes; at the same time, there is some question related to when exactly this automaton gives a positive result. We solve this problem by requiring that the resulting nondeterministic automaton be an analog of the total deterministic automaton.