On Effective Representations of Well Quasi-Orderings

With motivations coming from Verification, we define a notion of effective WQO for which it is possible to represent closed subsets and to compute basic set-operations on these representations.

In a first part, we show that many of the natural constructions that preserve WQOs also preserve our notion of effectiveness, proving that a large class of commonly used WQOs are effective. This part is based on an unpublished article with Jean Goubault-Larrecq, Narayan Kumar, Prateek Karandikar and Philippe Schnoebelen.

In a second part, we investigate the consequences of our notion on first-order logics over WQOs. Although the positive existential fragment is decidable for any effective WQO, the perspective of extension to larger fragments is hopeless since the existential fragment is already undecidable for the first-order logic over words with the subword ordering.

This last result has been published in LICS 2017 with Philippe Schnoebelen and Georg Zetzsche.