In a nutshell, GOE is a tool that assists the user in finding future events in the behaviour without going through the lengthy operation of step-by-step derivation.
The dynamic semantics of LOTOS are defined in terms of axioms and inference rules which generate, from a given behaviour expression, the next possible actions and their resulting behaviour expressions. GOE introduces a new type of inference rules, which are capable of generating traces of actions leading to a pre-selected action in the specification. These inference rules are guided by the static derivation path of the pre-selected action, which locates the action in the abstract syntactic tree of the current behaviour statically. This allows a considerable reduction of the search space. Such a technique often permits the analysis of divergent specifications that are generally beyond the capabilities of verification tools based on traces.