2 - 3 pm, Lecture Hall 5
The Quantifier Alternation Hierarchy of Synchronous Relations
LaBRI, University of Bordeaux, France.
Synchronous relations form a class of word relations definable by finite automata. They play an important role in querying graph databases and pattern matching, enjoying good closure properties. Furthermore, this class possesses a first order logical characterization due to a 1960 theorem by Eilenberg, Elgot and Shepherdson. The logic is over the set of all words, with the signatures containing the prefix, equal length and last letter predicates.
A newer proof of this theorem yields an interesting result: the FO logic collapses to level 3 of its quantifier alternation. We characterize relational classes of levels 1 and 2 of this quantifier alternation hierarchy, and show that they are analogues to their classical FO(<) counterparts. We show that the analogy extends to the Boolean combinations of these classes, a result that yields a decision procedure for the membership problem for all these classes.