There are several decision problems for certain computation models with atoms that are decidable when atoms admit certain well quasi order (WQO),  and undecidable otherwise. We recall the problems and formulate few questions related to WQOs.

This post is inspired by the decision problems of the following kind, in sets with atoms:

— emptiness of one-dimensional (finitely branching) alternating automata

— coverability of one-dimensional Petri nets.

The problems are parametric in the choice of atoms. For certain choices of atoms the problems are decidable, and in every case the known algorithms use a WQO on finite sets of atoms, or finite multisets of atoms. Examples are: equality atoms, total order atoms, universal tree, universal equivalence relation, etc.  For certain other choices of atoms the problems are undedicable, eg. for universal graph, universal partial order, universal tournament, etc. An  intriguing observation is that every undecidable case is witnessed by an infinite antichain of a very simple form. For instace in case of graphs, the antichain could consist of all cycles . This motivates a strange conjecture to be stated below.

The ordering that naturally arises in the problems mentioned above is the embedding order on  a Fraisse class of finite relational structures:

For an arbitrary fixed quasi order , the embedding ordering naturally extends to , the structures  from labelled with elements of : the embedding must additionally satisfy

The algorithms for the problems mentioned above use the embedding ordering of , for

— the powerset of a finite set , ordered by inclusion, or

— finite multisets over , ordered by multiset inclusions (not to  be confused with another natural choice, namely Dershowitz-Manna ordering:).

Here a natural question appears: are the following  conditions eqiuvalent for every Faisse class ?

— is a WQO

— is a WQO, for every finite

— is a WQO, for every finite quasi order

— is a WQO, for every WQO

Probably not, but any counterexample would probably require defining a WQO on some Fraisse classe that is essentially different from Dickson, Higman or Kruskal, as they “correspond” to equality atoms, total order atoms, or tree atoms, respectively.

Now a strange conjecture claiming that WQO-based methods are essentially the only methods for decidability:

Conjecture (WQO dichotomy). For an effective Fraisse class , exactly on of the following conditions is true:

— is a WQO

— emptiness of one-dimensional (finitely branching) alternating automata is undecidable.

(An analogous conjecture may be stated for the other decision problem, and possibly for many other problems.) It is however not completely clear what effectivity assumption is needed.

In other words, if not a WQO then the Fraisse class contains a “regular” antichain, that may be used for an undecidability proof.

Somehow related may be a result of Ding (see also its generalization in the following paper by Cherlin) stating that a downward closed subclass of graphs (with subgraph or induced subgraph ordering) is a WQO if and only of it contains only finitely many graphs and (H-shaped graphs). In other words, lack of WQO is always witnessed by an infinite antichain consisting of graphs of one of these two simple forms.