  The problem of finding pure strategy Nash equilibria in multiagent concurrent
games with finite-horizon temporal goals has received some recent attention.
Earlier work solved this problem through the use of Rabin automata. In this
work, we take advantage of the finite-horizon nature of the agents' goals and
show that checking for and finding pure strategy Nash equilibria can be done
using a combination of safety games and lasso testing in B\"uchi automata. To
separate strategic reasoning from temporal reasoning, we model agents' goals by
deterministic finite-word automata (DFAs), since finite-horizon logics such as
LTL\textsubscript{f} and LDL\textsubscript{f} are reasoned about through
conversion to equivalent DFAs. This allow us characterize the complexity of the
problem as PSPACE complete.
