Well structured transtition systems everywhere and everytime!

The theory of Well Structured Transition Systems provides the good structure for computing a finite basis of the set of predecessors of the upward closure of a finite set of states. We address here the dual problem which is to compute a finite representation of the set of successors of the downward closure of a finite set of states (called the cover). This last problem is, a priori, more difficult because in general, the cover has no finite basis. It is possible to complete any well-ordered set to obtain a cpo in which every downward closed set has a finite representation. We then define the framework of Complete Well Structured Transition Systems and we propose a simple and a conceptual procedure for computing the covering set and the covering graph. This procedure terminates more often than the generalized Karp-Miller tree procedure when applied on extended Petri nets and lossy channel systems.