Stop it, and be stubborn!
Research output: Contribution to journal › Article › Scientific › peer-review
|Journal||ACM Transactions on Embedded Computing Systems|
|Publication status||Published - 1 Jan 2017|
|Publication type||A1 Journal article-refereed|
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 formeeting 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.