Title: A Decidable Intuitionistic Temporal Logic,
Abstract: We introduce the logic $\sf ITL^e$, an intuitionistic temporal logic based on
structures $(W,\preccurlyeq,S)$, where $\preccurlyeq$ is used to interpret
intuitionistic implication and $S$ is a $\preccurlyeq$-monotone function used
to interpret temporal modalities. Our main result is that the satisfiability
and validity problems for $\sf ITL^e$ are decidable. We prove this by showing
that the logic enjoys the strong finite model property. In contrast, we also
consider a `persistent' version of the logic, $\sf ITL^p$, whose models are
similar to Cartesian products. We prove that, unlike $\sf ITL^e$, $\sf ITL^p$
does not have the finite model property.