Handling infinitely branching well-structured transition systems

摘要

AbstractMost decidability results concerning well-structured transition systems apply to thefinitely branchingvariant. 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 arefiniteunions 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.