Forward Analysis and Model Checking for Trace Bounded WSTS

TL;DR

This paper studies a specific subclass of well-structured transition systems called bounded WSTS, proving that their boundedness is decidable and enabling the verification of all omega-regular properties on infinite traces.

Contribution

It introduces bounded WSTS as a new subclass, proves the decidability of their boundedness, and shows their usefulness for verifying omega-regular properties.

Findings

Boundedness of WSTS is decidable.

Bounded WSTS can verify all omega-regular properties.

Boundedness restriction improves analysis capabilities.

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 (Logic. Meth. Comput. Sci. 2012). 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 $\omega$-regular properties on the set of infinite traces of the system.