An algorithmic account of winning strategies in Ehrenfeucht games on labelled successor structures

Ehrenfeucht-Fraïssé games are commonly used as a method to measure the expressive power of a logic, but they are also a flexible tool to compare structures. To exploit such a comparison power, explicit conditions characterizing the winning strategies for both players must be provided. We give a necessary and sufficient condition for Duplicator to win games played on finite structures with a successor relation and a finite number of unary predicates. This structural characterization suggests an algorithmic approach to the analysis of games, which can be used to compute the “remoteness” of a game and to determine the optimal moves for both players, that is, to derive algorithms for Spoiler and Duplicator that play optimally. We argue that such an algorithmic solution may be used in contexts where the “degree of similarity” between two structures must be measured, such as the comparison of biological sequences.