TUTCRIS - Tampereen teknillinen yliopisto

TUTCRIS

Stop it, and be stubborn!

Tutkimustuotosvertaisarvioitu

Standard

Stop it, and be stubborn! / Valmari, Antti.

julkaisussa: ACM Transactions on Embedded Computing Systems, Vuosikerta 16, Nro 2, 46, 01.01.2017.

Tutkimustuotosvertaisarvioitu

Harvard

Valmari, A 2017, 'Stop it, and be stubborn!', ACM Transactions on Embedded Computing Systems, Vuosikerta. 16, Nro 2, 46. https://doi.org/10.1145/3012279

APA

Valmari, A. (2017). Stop it, and be stubborn! ACM Transactions on Embedded Computing Systems, 16(2), [46]. https://doi.org/10.1145/3012279

Vancouver

Valmari A. Stop it, and be stubborn! ACM Transactions on Embedded Computing Systems. 2017 tammi 1;16(2). 46. https://doi.org/10.1145/3012279

Author

Valmari, Antti. / Stop it, and be stubborn!. Julkaisussa: ACM Transactions on Embedded Computing Systems. 2017 ; Vuosikerta 16, Nro 2.

Bibtex - Lataa

@article{9e5fb7a238a6467cb0cf0e82588b01b8,
title = "Stop it, and be stubborn!",
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.",
keywords = "Ignoring problem, Safety/progress/liveness properties, Stubborn set/ample set/persistent set/partial order methods",
author = "Antti Valmari",
year = "2017",
month = "1",
day = "1",
doi = "10.1145/3012279",
language = "English",
volume = "16",
journal = "ACM Transactions on Embedded Computing Systems",
issn = "1539-9087",
publisher = "Association for Computing Machinery",
number = "2",

}

RIS (suitable for import to EndNote) - Lataa

TY - JOUR

T1 - Stop it, and be stubborn!

AU - Valmari, Antti

PY - 2017/1/1

Y1 - 2017/1/1

N2 - 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.

AB - 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.

KW - Ignoring problem

KW - Safety/progress/liveness properties

KW - Stubborn set/ample set/persistent set/partial order methods

U2 - 10.1145/3012279

DO - 10.1145/3012279

M3 - Article

VL - 16

JO - ACM Transactions on Embedded Computing Systems

JF - ACM Transactions on Embedded Computing Systems

SN - 1539-9087

IS - 2

M1 - 46

ER -