Reduction and covering of infinite reachability trees (Q1173681)

The aim of this paper is to generalize the main decidability results concerning Petri nets to the framework of structured transition systems. The author defines the class of structured transition systems and its subclass of strictly structured transition systems, and then proves that the Finite Reachability Tree Problem (FRTP) is decidable for structured transition systems and that the Finite Reachability Set Problem (FRSP) is decidable for strictly structured transition systems. It is conjectured that the FRSP is undecidable for structured transition systems. The author then considers the decidability of the Coverability Problem (CP). The following notions are defined: coverability set of a structured transition system, strictly structured labelled transition systems, generalized Karp and Miller tree, well structured labelled transition systems. The main result of this section is that the CP is decidable for well structured labelled transition systems. Finally, the structured transition systems having a structured set of terminal states are considered. The two main results are: the FRTP for structured transition systems having a structured set of terminal states is decidable and so is the FRSP for strictly structured transition systems having a structured set of terminal states. Known results and open problems (most with a conjecture) are well summarized in a table.