| Summary: | 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.
|
|---|
