Handling infinitely branching well-structured transition systems

Most decidability results concerning well-structured transition systems apply to the finitely branching variant. Yet some models (inserting automata, ω-Petri nets, …) are naturally infinitely branching. Here we develop tools to handle infinitely branching WSTS by exploiting the crucial property that in the (ideal) completion of a well-quasi-ordered set, downward-closed sets are finite unions of ideals. Then, using these tools, we derive decidability results and we delineate the undecidability frontier in the case of the termination, the maintainability and the coverability problems. Coverability and boundedness under new effectiveness conditions are shown decidable.