⁷A reachability goal of the form $\exists <!--FUNCTION\; APPLICATION-->x_1,\dots ,x_{k}s{\to }^{\ast }t$ is linear if $s$ is linear and $s$ and $t$ do not have variables in common.