We consider a slightly extended version of a nondeterministic finite automaton, call it a "propositional nondeterministic finite automaton". It is defined as follows. Consider a fixed propositional language $L\_A$ built over a finite set of propositional variables $A$. $L\_A$ is together with the usual logical connectives $\wedge$, $\vee$, $\neg$, etc.
A propositional nondeterministic finite automaton is a tuple $(Q, \Sigma, \Delta, q\_\*, prop)$, where $Q$ is a finite set of states, $\Sigma$ is a finite set of symbols, $\Delta \subseteq Q \times \Sigma \times Q$ is a transition relation, $q\_\* \in Q$ is called the initial state, and $prop$ is a mapping from $Q$ to $L\_A$.


Given a state $q \in Q$ and a symbol $a \in \Sigma$, we say that $(q, a)$ is an "admissible transition" if there exists a state $q' \in Q$ such that $(q, a, q') \in \Delta$.


Recall that a (propositional) interpretation (on $A$) is a mapping from $A$ to $\{0, 1\}$, and a model of a propositional formula is an interpretation that satisfies the formula in the usual way.


We consider the following decision problem. Given a propositional nondeterministic finite automaton $(Q, \Sigma, \Delta, q\_\*, prop)$, a property $P$ on any finite serie of propositional interpretations $(I\_1, \dots, I\_n), n > 0$ that can be checked in polynomial time (i.e., in $O(n^i)$ steps, where i is some constant), and a non-negative integer $k$ given in binary notation, determine whether there exists a model $I\_0$ of $prop(q\_0)$ where $q\_0 = q\_\*$, and a symbol $a\_1 \in \Sigma$ where $(q\_0, a\_1)$ is an admissible transition, such that for every state $q\_1 \in Q$ where $(q\_0, a\_1, q\_1) \in \Delta$, there exists a model $I\_1$ of $prop(q\_1)$ and a symbol $a\_2 \in \Sigma$ where $(q\_1, a\_2)$ is an admissible transition, such that for every state $q\_2 \in Q$ where $(q\_1, a\_2, q\_2) \in \Delta$, there exists \dots, there exists a model $I\_k$ of $prop(q\_k)$ such that the serie $(I\_0, \dots, I\_k)$ of propositional interpretations satisfies the property $P$.


I would like to characterize the complexity of this problem (belongness and hardness). Actually, I am interested in a specific property $P$ which is parametrized by a non-negative integer $s$, i.e., the property $P\_s$ defined as follows: a serie of propositional interpretations $(I\_1, \dots, I\_n), n > 0$, satisfies $P\_s$ if for each $i \in \{1, \dots, n-1\}$, the Hamming distance between $I\_i$ and $I\_{i+1}$ is below $s$. However, the "hardness" part may be easier to prove if one considers the generic form of the decision problem with any property $P$ checked in polynomial time.


For the "belongness" part: this decision problem looks like the canonical $\mathsf{PSPACE}$-complete problem $True-QBF$: indeed, there is an alternation of existential and universal quantifiers. But the main problem is that since $k$ is given in binary form, the length of this sequence of these alternative existential/universal quantifiers is exponential ($= 2^{|k|}$), as well as the size of the serie $(I\_0, \dots, I\_k)$. Is $\mathsf{EXPTIME}$ the class to which this problem belong to? In any case, I would be happy to get the intuition of the proof for the non-expert I am.



QBF of exponential length?
$\DeclareMathOperator\prop{prop}$Allowing general poly-time properties $P$ unnecessarily blows up the complexity, it makes the problem complete for EXPSPACE = AEXPTIME. On the one hand, the definition of the problem itself is more or less a description of an exponential-time alternating Turing machine that solves it. On the other hand, let $L$ be an AEXPTIME problem. By standard elementary manipulations, $L$ can be solved by an alternating TM which is given the length $n$ of its input on a tape, and its computation proceeds by first making $2^{n^c}$ alternating universal and existential choices of bits that are recorded on an auxiliary tape, followed by a deterministic computation. In other words,
$$\tag{$\*$}w\in L\iff\forall a\_1\,\exists b\_1\,\forall a\_2\,\cdots\,\exists b\_{2^{|w|^c}}\,P(w,a\_1,b\_1,\dots,a\_{2^{|w|^c}},b\_{2^{|w|^c}}),$$
where $a\_i,b\_i\in\{0,1\}$, and $P$ is a polynomial-time predicate (note that this gives it exponential time in terms of $|w|$, because the length of $P$’s input is $O(2^{|w|^c})$). This can be reduced to your problem as follows. Let $A=\{u,v\}$, and $|\Sigma|=1$ (so I will just ignore symbols in the description). Given a word $w$ of length $n$, we construct an automaton with states $\{q\_0,\dots,q\_{n-1},r\_0,r\_1\}$. There are transitions from $q\_i$ to $q\_{i+1}$, and the formula $\prop(q\_i)$ is $\neg u\land\neg v$ or $\neg u\land v$ depending on $w\_i$; note that this forces $I\_0,\dots,I\_{n-1}$ deterministically to essentially equal $w$ (mixed with irrelevant $0$’s). Then we have transitions from each of $q\_{n-1},r\_0,r\_1$ to each of $r\_0,r\_1$, and $\prop(r\_0)=\neg u$, $\prop(r\_1)=u$. The point is that when we are in $r\_i$, the quantifiers “for each state $r\_j$ with $(r\_i,r\_j)\in\Delta$ there exists $I\models\prop(r\_j)$ such that ...” resolve to “for every $u\in\{0,1\}$ there is a $v\in\{0,1\}$”, with $I\_j=(u,v)$. Thus, if we run the whole thing for $k=n+2^{n^c}$ steps, the sequence of the $I$’s will consist of a copy of $w$ plus a sequence $a\_1,b\_1,\dots,a\_{2^{n^2}},b\_{2^{n^2}}$ that were quantified the same way as in $(\*)$.


In contrast, your specific $P\_s$ can be handled much more efficiently, because it only restricts possible transitions from one step to the next one.
You can incorporate $I$ into the state of the automaton, and since you are not discussing acceptance of any words, you can get rid of the alphabet as well. That is, your problem is easily reducible to the alternating reachability problem, and as such it is solvable in P (deterministic polynomial time).


Rather than the reduction, let me give the final algorithm. Let us define that $(q\_0,a\_0,I\_0)\in Q\times\Sigma\times\{0,1\}^A$ is $n$-step admissible if for every $q\_1$ such that $(q\_0,a\_0,q\_1)\in\Delta$, there exists $I\_1\models\prop(q\_1)$ with Hamming distance $\delta(I\_0,I\_1)\le s$ and an admissible transition $(q\_1,a\_2)$ such that etc up to $q\_n$. Note that $A$ is fixed, hence $2^{|A|}$ is constant, hence the set $X$ of all possible triples has polynomial size $O(|Q||\Sigma|)$. We can thus compute the set $X\_n$ of $n$-step admissible triples inductively by putting $X\_0=X$, and then given $X\_n$, check all the polynomially many possibilities to determine $X\_{n+1}$. Since $X\_0\supseteq X\_1\supseteq X\_2\supseteq\dots$, the sequence will stabilize after $m\le|X|$ steps, at which point we know the answer to the original question for $k$ (even if it is given in binary).


It is also not hard to establish that the problem is in fact P-complete.


This answers the question as stated. Your comments below indicate that you somehow do not like the fact that $2^{|A|}$ is constant, but then you need to clarify the question, since I have no idea would else could “*consider a fixed propositional language $L\_A$ built over a finite set of propositional variables* $A$” possibly mean.


If I just ignore this sentence completely and allow formulas over an arbitrary $A$ which is given as a part of the input, then the problem becomes complete for EXP = APSPACE. On the one hand, the alternating exponential time solution from the beginning becomes alternating polynomial space, as we do not have to keep more than two assignments at a time in memory. One can show EXP-hardness by simulating alternating polynomial-space machines. As a rough sketch, the states $Q$ of the automaton will encode the state of the simulated machine, the position of tape head, and the symbol below the head, while propositional assignments $I$ will simulate the content of the tape. One can arrange that a Hamming distance $1$ constraint will ensure the coherence of the tape from one step to another. Additional propositional variable or two can be used to simulate existential choices of the machine, while universal choices can directly correspond to nondeterminism of the automaton.


Concerning your comment (2): as long as the properties can be checked on the fly while keeping only a polynomial-size data, the problem will still be solvable in EXP, but there is no telling whether it can be done more efficiently without knowing the properties.


