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.