Membership to double cosets in free groups 
*

*Is there an elementary and efficient algorithm for testing the membership to a double coset of f.g. subgroups in a free group?

*Has this membership problem been implemented in GAP/Magma?
More precisely, I have a finitely generated free group $F$, two finitely generated subgroups $A,B$, given by their free generating sets, and an element $f\in F$. I would like to determine whether $f \in AB$.
I was hoping for something in the spirit of Stallings core graphs, but the standard reference (the paper of Kapovich and Myasnikov [Kapovich, Ilya; Myasnikov, Alexei, Stallings foldings and subgroups of free groups, J. Algebra 248, No. 2, 608-668 (2002). ZBL1001.20015.]) does not seem to treat membership to double cosets.
Theoretically the required algorithm certainly exists. In fact, a much stronger property was proved by Grunschlag ( see Theorem 4.10 in [Grunschlag, Zeph, Computing angles in hyperbolic groups, Gilman, Robert H. (ed.), Groups, languages and geometry. 1998 AMS-IMS-SIAM joint summer research conference on geometric group theory and computer science, South Hadley, MA, USA, July 5-9, 1998. Providence, RI: American Mathematical Society. Contemp. Math. 250, 59-88 (1999). ZBL0953.20034.]
 A: 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.
A: Concerning implementations in GAP and Magma, there is a GAP package for handling subgroups of free groups, but I don't know whether that has the built-in functionality to do what you want.
I know more about the facilities in Magma (I coded some of them myself). It can do membership testing in finitely generated subgroups of free groups, and it does this by building a finite state automaton to recognize membership of reduced words in the subgroup. (This is constructed using coset enumeration, which is algorithmically the same as Stallings Folding.) It can also construct an automaton recognizing the intersection of two subgroups.
The problem here reduces to computing the intersection of cosets of finitely generated subgroups. There is currently no function that computes the automaton recognizing membership of a coset, but I could easily write one. One could then immediately compute the required intersections (as an automaton), which would allow membership testing.
A: Here is a second answer that is just rephrasing @DerekHolt’s answer based on the comments. So upvote his answer first!  Let $X$ be a finite alphabet.  An inverse automaton is a finite directed graph labeled over the alphabet $X$ which is folded in the sense of Stallings, meaning you cannot find two edges entering or leaving a vertex with the same label.  Equivalently these are immersions over a bouquet of circles.  An inverse automaton has a unique initial state and a set of final states.  It recognizes a subset of the free group by looking at all reduced words labelling a path from the initial state to a final state, where inverse letters read edges backward.  The language accepted by an inverse automaton is a finite union of cosets of finitely generated subgroups.
The languages accepted by inverse automata are closed under intersection.  You simply build the product automaton whose vertices are pairs of vertices and there is an edge labeled by $x$ from $(p,q)$ to $(p’,q’)$ if and only if there are edges from $p$ to $p’$ and $q$ to $q’$ labeled by $x$.  This construction is the fiber product of the two inverse automata viewed as immersions over a bouquet of circles.   The initial state is the pair of initial states and the final states are those pairs $(p,q)$ where both $p$ and $q$ are final in their respective automata.  This is an inverse automata that will accept precisely those reduced words which both automata accept.  In particular, the intersection is empty iff the initial vertex of the product construction cannot reach any terminal vertex.
Now to recognize $Hw$ write a linear automaton reading the word $w$ (with inverse letters read backward) and attach at the initial point a generating set for $H$ as loops and apply Stallings foldings.  The initial vertex is the intial vertex of $w$ and the final vertex is the end point of $w$.  These may collapse after folding. This is essentially the Stallings core of $H$ with a thorn labeled $w$ sticking out of the base point and Stallings uses this automaton in his proof of Marshall Hall's Theorem.
We can do a similar thing for $gK$, but we put the generators of $K$ as loops at the end of the path labelled $g$, and then to test if $w\in HgK$ we just form the product automaton for $Hw$ and $gK$ and check if the final state is reachable from the initial state.
Note $w=hgk$ iff $h^{-1}w=gk$.  So $Hw$ and $gK$ intersect iff $w\in HgK$.
