Decidability Results via Termination of the Verification Machinery

In this chapter, we study how to guarantee termination of the backward reachability procedures defined in the previous chapter. Since both $$\textsf{BReach}_{SAS}$$ and $$\textsf{BReach}_{RAS}$$ have been proved to be semi-decision procedures for detecting safety of SAS s and (plain) RAS s respectively, termination would also ensure, in turn, that they are full decision procedures.