For which series of finite simple groups is it algorithmically decidable whether they contain a homomorphic image of a given finitely presented group?
There are algorithms that can find all quotients of a finitely presented group isomorphic to ${\rm PSL}(2,q)$ for some $q$: see W. Plesken and A. Fabianska. An L2-quotient algorithm for finitely presented groups. J. Algebra, 322(3):914--935, 2009, and arXiv:1402.6788.
I believe that some progress has been made also with general $L_3(q)$ and $U_3(q)$ quotient algorithms. Roughly speaking, they just introduce variables for entries in the $2 \times 2$ or $3 \times 3$ matrices, and solve for them, using Gröbner basis type methods, although of course a lot of clever tricks are needed to enable them to work in practice.
I would guess that for any fixed $n$, it is possible in theory to test for the existence of finite simple quotients that have Lie rank $n$. That might be possible to prove.
I would also speculate that it might be undecidable whether there exists a quotient of the form $A_n$ for some $n$. Or, if you fix the field and vary the rank then it might also be undecidable: do there exist quotients of form $L_n(2)$ for example.
UPDATE 22/10/17: The question is answered for many classes of simple quotients in this preprint of Bridson--Evans--Liebeck--Segal.
Here's what I know.
Martin Bridson and I proved the theorem mentioned in the question, namely that it is undecidable whether or not a fp group has a non-trivial finite quotient. As you say, it follow trivially that, for at least one infinite family $S$ of finite simple groups, it's undecidable whether or not a fp group has quotient from $S$, and so the question is raised of which families $S$ this is true for.
I have seen a very early preprint which resolves this in several cases. Since it isn't publicly available, I don't want to reveal the authors, but, iirc, it proves that this is undecidable for the alternating groups, and also for any family of classical Lie groups (eg PSL(n,q) for any q as n varies).
I believe that techniques of proof are expected to extend to the other families of groups of Lie type, and this may be work in progress.
Remarkably, although I don't recall the reference, it is known that the problem is decidable when $n=2$ and $q$ varies (that is, when $S=\{PSL(2,q)\}$), and I believe this also for the other classical groups. Based on this, Bridson has conjectured (in conversation) that the same holds for any fixed $n$ when $q$ varies (and similarly for the other classical groups).
Here's the proof for the decidability when the family $\mathcal{F}$ consists of all abelian simple groups $C_p$ along with all $PSL(2,q)$ for $q$ prime power.
The first remark is that a group has a quotient in $\mathcal{F}$ iff it has a nontrivial representation in $SL(2,q)$ for some $q$. (Including abelian simple groups in $\mathcal{F}$ allows me not to care about the image.)
The second remark is that a finitely generated group has a nontrivial representation in $SL(2,q)$ for some $q$ iff it has a nontrivial representation in $SL(2,K)$ for some field $K$. This does not use any kind of strong approximation, but simple facts that are basically the same as those showing that a f.g. linear group is residually finite. Namely if there's a nontrivial rep. in $SL_2(K)$, there's a nontrivial rep. in $SL_2(A)$ for some f.g. domain $A$, and since $A$ is residually a finite field we get a nontrivial rep. in $SL_2(F)$ for some finite field $F$.
Now the set of representations of a finitely presented group $\Gamma$ into $SL_2(A)$ can be described as $V(A)$, where $V$ is a $\mathbf{Z}$-defined affine variety, whose equations are explicitly defined according to a presentation of $\Gamma$. Here $V(A)=Hom(B,A)$, where $B$ is a finitely generated commutative ring, defined by a finite presentation explicitely output from the presentation of $\Gamma$.
Thus we are reduced to: given a finitely generated commutative ring $B$, determine whether there exists a field $K$ such that $Hom(B,K)$ is not reduced to a singleton $\{f_0\}$. Here $B$ comes with an explicit ring homomorphism $f_0$ onto $\mathbf{Z}$, coming from the trivial representation. Again by the standard argument, the above field $K$ can be chosen finite. Hence if we check all finite fields, we can detect when $Hom(B,K)\neq\{f_0\}$ for some field $K$. Conversely, a simple lemma (*) shows that if $Hom(B,K)=\{f_0\}$ for every field $K$, then the kernel of $f_0$ consists of nilpotent elements. Since the kernel of $f_0$ has explicit generators (the $x_i-f_0(x_i)$ where $x_i$ range over generators of $B$), in case these generators are nilpotent this can be detected in finite time. So we have an algorithm.
[Edit: proof of lemma (*): if $f_0(x)=0$ and $x$ is not nilpotent, since $B$ is a Jacobson ring there exists a quotient field $K$ in which $x$ has a nonzero image; then $K$ is finite, say of characteristic $p$ and using $f_0$, $B$ admits $K\times\mathbf{Z}/p\mathbf{Z}$ as a quotient, and thus admits two distinct homomorphisms to $K$, a contradiction.]
The argument, for each given $n$, extends to the family of all simple subquotients of $SL(n,q)$ for all prime powers $q$. Also it probably adapts, for given $(n,p)$ to the family of all simple subquotients of $SL(n,p^k)$. Now if one wishes to hold the family of say all $PSL(n,q)$ ($n$ fixed) and not its subquotients, one needs additional arguments.