Decidability of the Reachability Problem

This famous problem was originally solved, almost simultaneously, by a number of researchers. Prominent amongst them are R. Kosaraju, (a little later) J.-L. Lambert, and H.W. Mayr. Their approaches make extensive use of generalised coverability graphs and employ decomposition techniques. They are now collectively known as the KLM approach. More recently, a different approach was successfully pursued by J. Leroux. This approach employs two semidecision algorithms, of which the second is based heavily on what are called “almost semilinear” sets. In this chapter, the KLM approach is described in its “Lambert flavour”. This is not outdated by Leroux’ proof because various complexity results are based on KLM decompositions.