Benois gave a Stallings type algorithm before Stallings to compute membership in any rational subset of a free group on a set $X$. A rational subset $R$ is given by a finite automoaton over the alphabet $X\cup X^{-1}$. An element $g\in FG(X)$ of the free group belongs to $R$ if some word which freely reduces to $g$ is accepted by the automaton. Note that you are not allowed to read an edge in the backward direction and the automaton can be non-deterministic and have epsilon-transitions.

For a double coset $HgK$ you build an automaton where the generators of $H$ and their inverses read loops at the initial state, then there is a sequence of edges spelling out $g$ landing at the final state which has loops labeled by the generators of $K$ and their inverses. If $g$ is the identity you should use an epsilon transition.

Here is the Benois algorithm. We start off with an automaton and we add epsilon transitions until we guarantee that whenever a word is readable between two states, then so is its free reduction. First of all, we search for paths of length two labelled $xx^{-1}$ or $x^{-1}x$ and we add an epsilon transiiton from the beginning of the path to the end of the path (epsilon means empty word). This is the analogue of Stallings folding Inducitvely, we search for paths of the form $\epsilon\epsilon$ or $x\epsilon x^{-1}$ or $x^{-1}\epsilon x$ ($x$ a generator) and if there is no epsilon edge from the beginning to the end of this path of length 2 or 3, we add one. Since we never changed the number of vertices, in a finite number of steps we will not be able to add any new epsilon edges. The resulting automaton is called saturated.

Notice that none of these new epsilon edges change the image of this rational set in the free group. But once it is saturated, whenever we can read a word between two vertices, we can also read its reduced form. Hence the set of reduced words accepted by the saturated automaton is exactly our rational subset of the free group. There is a well known automaton which accepts precisely the reduced words and there is a well known direct product construction that builds an automaton which recognizes the intersection of two regular languages and so you can build an automaton which recognizes exactly the reduced words in your rational subset.

Details can be found in Theorem 3.3 I believe. My memory is that this can be implemented in no worse than cubic time in the size of the automaton (which will be the natural size in the double coset case), but I haven’t thought about that in years.

**Added.** You can also solve this problem in virtually free groups. Here is another algorithm for free groups that also works for virtually free groups. Recall by Muller-Schupp that a group is virtually free if and only if its word problem is a context-free language. Most reasonable ways of describing a virtually free group will give that context-free grammar. Now if $R$ is a rational subset of a virtually free group (like a double coset of finitely generated subgroup), then $g\in R$ if and only if $1\in g^{-1}R$ and so it suffices to be able to solve the question given a finite automaton over the alphabet of the group, is the intersection of the word problem with the regular subset recognized by the automaton non-empty? But the intersection of a context-free language and a regular language is always context-free and emptiness is decidable for context-free languages.

2more comments