An algorithmic account of ehrenfeucht games on labeled 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. © Springer-Verlag Berlin Heidelberg 2005.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)