Forward analysis and model checking for trace bounded WSTS

Abstract

We investigate a subclass of well-structured transition systems (WSTS), the bounded - in the sense of Ginsburg and Spanier (Trans. AMS 1964) - complete deterministic ones, which we claim provide an adequate basis for the study of forward analyses as developed by Finkel and Goubault-Larrecq (ICALP 2009). Indeed, we prove that, unlike other conditions considered previously for the termination of forward analysis, boundedness is decidable. Boundedness turns out to be a valuable restriction for WSTS verification, as we show that it further allows to decide all ω-regular properties on the set of infinite traces of the system. © 2011 Springer-Verlag.