PSPACE-completeness of DFA intersection problem Let some deterministic finite automata be given. There is a problem of determining whether the intersection of these DFA is empty, and I want to show its PSPACE-completeness. 

It seems to me that I understand, why this problem lies in PSPACE: if $ n_1,\dots, n_k $ are the numbers of states, then one can take the product of these DFA and get that if there is a recognisable string, then there is a recognisable string of length $ \le n_1\dots n_k$. Then we can non-deterministically guess this string and use Savitch theorem.

So, the question is, how to prove PSPACE-hardness? Should I reduce any given TM to this problem, or maybe some known problem like QBF?
Your proof that the problem is in PSPACE is not quite correct. The problem is that the product $n_1 \cdots n_k$ is not bounded by a polynomial in the input length $n_1 + \dots + n_k$. The correct way to do it is to directly apply Savitch's theorem to the NPSPACE machine that nondeterministically guesses a path through the product graph. The difference is that, while an accepting path can indeed be as long as $n_1 \dots n_k$, the machine only guesses one symbol at a time and never stores the entire input string in memory, so we stay within the polynomial space limit.



It is a well-known fact that this problem is PSPACE-hard, but the only proof that I am aware of is not particularly trivial. I believe the first proof was given in:


  Dexter Kozen. Lower Bounds for Natural Proof Systems. FOCS 1977: 254-266.


The proof involves constructing a mess of DFAs which collectively enforce all the necessary constraints to require that any string in the intersection language is a trace of the execution of a polynomial space Turing machine that leads to an accepting configuration.