On the problem of logic-automatic formulas performability

Background. In the theory of finite automata, there are a number of ways to define finite automata (finitely automatic functions). There are systems of canonical equations among them, Moore diagrams, information trees, schemes of automatic elements, and finite-automaton operations. Each of these methods has certain advantages and finds application in suitable research areas. Quite often finite automata are studied by algebraic and logical means. For example, the results of J. Büchi on the connection of finite automata with second-order logic are well known, as well as the results of S. V. Aleshin on the use of groups of finitely automatic permutations in solving the weakened Burnside problem. One of the promising directions in the theory of finite automata is the study of automaton equations of various types. In addition to the well-known canonical equations, there may be functional equations in which variables are finite automata, and connections between them are made using algebraic and logical means. The most natural option is the option when automatic terms are determined based on the given automata and functional variables for (multi-input) automata, then equality of terms (elementary formulas) and finally from elementary formulas using logical connectives-arbitrary logic automaton formulas. For such formulas, the “classic” feasibility problem is posed. Its peculiarity is that we consider the existence of finite automata that perform this formula, i.e. giving the true value of the formula for any values of subject variables (their values are arbitrary superwords in the alphabet {0,1}). The goal of this work is to prove the algorithmic solvability of this problem, while the resolving algorithm is defined in automata terms and ultimately based on a directed iteration of partial nondeterministic automata.
Materials and methods. Logic automaton methods are used in constractions and proofs.
Results and conclusions. We consider logic automaton formulas constructed using logical connectives from the equalities of automaton terms. For formulas of this type, the problem of satisfiability for functional (automatic) variables is formulated. It is assumed that all subject variables (for binary superwords) are under the generality quantifiers. We construct an algorithm based on the iteration of partial nondeterministic automata, which solves this problem. The proposed approach to analyzing and solving the satisfiability problem for finite-automaton logical formulas can be used to solve similar algorithmic problems for more complex types of logic automaton formulas.