Stop It, and Be Stubborn!
Antti Valmari · ACM Transactions on Embedded Computing Systems · 2017
This publication discusses how automatic verification of concurrent systems can be made more efficient by focusing on always may-terminating systems . First, making a system always may-terminating is a method for meeting a modelling need that exists independently of this publication. It is illustrated that without doing so, non-progress errors may be lost. Second, state explosion is often alleviated with stubborn, ample, and persistent set methods. They use expensive cycle or terminal strong component conditions in many cases. It is proven that for many important classes of properties, if the systems are always may-terminating, then these conditions can be left out.