WQO dichotomy for homogeneous structures (experimental evaluation)

The project lies on the borderline of automata theory, formal verification, and model theory. It concerns data-enriched models, like Petri nets with data or register automata, where executability of a transition is conditioned by a relation between data values involved. Decidability status of various decision problems in such models may depend on the structure of data domain. According to the WQO Dichotomy Conjecture [1], if a data domain is homogeneous then it either exhibits a well quasi-order (in which case decidability follows by standard arguments), or essentially all the decision problems are undecidable for Petri nets over that data domain. 

The conjecture has been confirmed for data domains being homogeneous graphs, directed graphs, and 3-graphs (graphs with 2-colored edges) [2]. On the technical level, the latter results is a significant step beyond known classification results for homogeneous structures. 

The Master's thesis [3] experimentally confirmed the conjecture for k-graphs excluding 3-element structures, for small k (by encoding the problem in SAT and using efficient SAT-solvers). The topic of this project is to investigate possibilities of pushing the experimental confirmation further, or to possibly attempt proving the conjecture in some restricted cases.

[1] Decidability border for Petri nets with data: WQO dichotomy conjecture
    https://www.mimuw.edu.pl/~sl/PAPERS/pn16.pdf

[2] WQO dichotomy for 3-graphs
    https://arxiv.org/abs/1802.07612

[3] Eksperymentalna weryfikacja hipotezy o dychotomii WQO
    Master's thesis (in Polish)