Complexity/decidability of the "nested maze" problem?

Question

In this Puzzling SE post, there's a maze with infinitely nested inside itself. Inspired by this, consider the following graph problem:

Setup:

1. A graph G with vertices V and undirected edges E
2. And additional set of directed edges F.
3. Starting vertex S
4. Goal vertex Z

We can define the nested maze problem using the above notation by saying you must find a path from state (S, 0) to state (Z, 0), using the edges from E and F as follows:

1. An edge (u, v) in E lets you make the state transitions: (u, n) -> (v, n) or (v, n) -> (u, n) for any n >= 0. This corresponds to ordinary movement in the maze.
2. An edge (u, v) in F lets you make the state transitions: (u, n) -> (v, n + 1) or (v, n + 1) -> (u, n) for any n >= 0. This corresponds to entering/exiting the nested maze, with the second element of the state tracking the "depth".

A path is a sequence of edges (repetitions are allowed!).

Is there an algorithm for solving this problem in general? It seems possible that it's undecidable, but the particular example from the above Puzzling post isn't particularly hard to analyze.

Edit: Thinking about this more, can you discard E by just merging all vertices that are mutually reachable in G. Then, the problem is just one on V and F, where you want to find a path (possibly involving repeated edges) using edges either forwards or backwards, with the number of forward traversals equalling the number of backward traversals. Additionally, the number of forward traversals must be at least the number of backward traversals for all prefixes of the path.

Answer 1

Probably overkill, but given that there hasn't been an answer here's a method of showing that this problem is decidable.

Given an instance of this problem, you can pretty easily define a pushdown automaton which defines a non-empty language iff there's a solution to the instance. Here's how to do so:

• States: The vertices of the graph with one additional state added: V U {v_reject}.
• Input alphabet: The set of ordered triples {(u, v, d): u, v in V, d in {-1, 0, 1}}.
• Stack alphabet: A singleton set {1}
• Transitions:
  • For each (u, v) in E, add a transition from u to v when reading an input of (u, v, 0), and vice versa for an input of (v, u, 0). Both transitions should leave the stack untouched.
  • For each (u, v) in F, add a transition from u to v when reading an input of (u, v, 1). This transition should push a 1 onto the stack.
  • For each (u, v) in F, add a transition from v to u when reading an input of (u, v, -1), which pops a 1 from the stack, but only if the stack is non-empty.
  • For any inputs other than those handled by the three cases above, transition to v_reject.
• Initial/final states: S and Z

Any solution to the original instance defines an input accepted by this PDA, and vice versa. In the original problem, the states consist of a vertex and a natural number. In the PDA formulation, the state is just a vertex, and the second element of the state tuple is tracked by the size of the stack.

Because CFG emptiness is decidable, this problem is decidable as well.