I have a need for an algorithm which I can express as a reachability problem in a graph.
Note that I'd appreciate any advices with respect to better wording this question. Also please tell me if this question does not fit this site (I considered posting it to "Computer Science" instead).
Consider an directed, connected, possibly cyclic graph $G=(V,E)$.
Consider also a finite set of "indicators" $I$, of a finite size. They are numbered $I_0 .. I_n$.
Each indicator $I_i$ can take an integer value in the range $[0..v(i)]$.
Each vertex can be labelled with one or more "assignations" of the form $I_i := v$, with $v \in [0..v(i)]$.
Exactly one vertex $V_0 \in V$ is distinguished as the "graph entry".
It is also considered that $V_0$ is labelled by $I_j := 0, \forall j \in [0..n]$ (i.e. the "value" of all indicators is $0$ at the graph entry).
Some vertices are such that all outbound edges from them are labelled by a "guard" of the form $I_k = v_p$, for a fixed value $k$ and all possible $p \in [0..m(k)]$ (i.e. there are "switches" at some vertexes where an edge is "chosen" based on the "current" value of an indicator).
We define (somewhat informally) a "valid" path in the graph as:
- being finite,
- respecting the topology constraints in the graph,
- and being such that, if is is crossed from its beginning to its end, while collecting the "current" (i.e., latest encountered) value of indicators in the process, then the equality associated to each guard is verified.
Informally, the graph represents all possible execution flows in a piece of code, with indicator variables being set and branching decisions being taken with respect to those indicators.
Now my problem is the following: given a vertex $V_q \in V$, does a valid path (in the sense defined above) exists from $V_0$ to $V_q$?
Note that I only need an algorithm efficiently answering if such path exists; I do not need it to construct one.
What I Did so Far
Empirically, I had quite good results so far with a brute-force execution simulation strategy enumerating all possible paths (with some memoization to limit memory consumption and ensure termination in the presence of cycles). But some larger graphs are proving a challenge, since most probably my current enumeration approach is of an exponential complexity.
Mostly I'd like to express my problem in a domain where I could benefit from existing complexity proofs and (hopefully!) solvers. I tried my hands at classical graph theory problems, considered SAT and Petri Nets too, but did not see a match so far. I also tried some classic and more recent data flow algorithms at first, but they fail short since I need an exact result.