Tampere University of Technology

TUTCRIS Research Portal

Stop it, and be stubborn!

Research output: Contribution to journalArticleScientificpeer-review


Original languageEnglish
Article number46
JournalACM Transactions on Embedded Computing Systems
Issue number2
Publication statusPublished - 1 Jan 2017
Publication typeA1 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.

ASJC Scopus subject areas


  • Ignoring problem, Safety/progress/liveness properties, Stubborn set/ample set/persistent set/partial order methods

Publication forum classification

Field of science, Statistics Finland