Tampere University of Technology

TUTCRIS Research Portal

Stop it, and be stubborn!

Research output: Contribution to journalArticleScientificpeer-review

Details

Original languageEnglish
Article number46
JournalACM Transactions on Embedded Computing Systems
Volume16
Issue number2
DOIs
Publication statusPublished - 1 Jan 2017
Publication typeA1 Journal article-refereed

Abstract

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

Keywords

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

Publication forum classification

Field of science, Statistics Finland