  The logics $\mathsf{CS4}$ and $\mathsf{IS4}$ are the two leading
intuitionistic variants of the modal logic $\mathsf{S4}$. Whether the finite
model property holds for each of these logics have been long-standing open
problems. It was recently shown that $\mathsf{IS4}$ has the finite frame
property and thus the finite model property. In this paper, we prove that
$\mathsf{CS4}$ also enjoys the finite frame property.
  Additionally, we investigate the following three logics closely related to
$\mathsf{IS4}$. The logic $\mathsf{GS4}$ is obtained by adding the
G\"odel--Dummett axiom to $\mathsf{IS4}$; it is both a superintuitionistic and
a fuzzy logic and has previously been given a real-valued semantics. We provide
an alternative birelational semantics and prove strong completeness with
respect to this semantics. The extension $\mathsf{GS4^c}$ of $\mathsf{GS4}$
corresponds to requiring a crisp accessibility relation on the real-valued
semantics. We give a birelational semantics corresponding to an extra
confluence condition on the $\mathsf{GS4}$ birelational semantics and prove
strong completeness. Neither of these two logics have the finite model property
with respect to their real-valued semantics, but we prove that they have the
finite frame property for their birelational semantics. Establishing the finite
birelational frame property immediately establishes decidability, which was
previously open for these two logics. Our proofs yield NEXPTIME upper bounds.
The logic $\mathsf{S4I}$ is obtained from $\mathsf{IS4}$ by reversing the roles
of the modal and intuitionistic relations in the birelational semantics. We
also prove the finite frame property, and thereby decidability, for
$\mathsf{S4I}$
