Stubborn set intuition explained

Antti Valmari; Henri Hansen

doi:10.1007/978-3-662-55862-1_7

Stubborn set intuition explained

Antti Valmari, Henri Hansen

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review

15 Citations (Scopus)

Abstract

This study focuses on the differences between stubborn sets and other partial order methods. First a major problem with step graphs is pointed out with an example. Then the deadlock-preserving stubborn set method is compared to the deadlock-preserving ample set and persistent set methods. Next, conditions are discussed whose purpose is to ensure that the reduced state space preserves the ordering of visible transitions, that is, transitions that may change the truth values of the propositions that the formula under verification has been built from. Finally solutions to the ignoring problem are analysed both when the purpose is to preserve only safety properties and when also liveness properties are of interest.

Original language	English
Title of host publication	Transactions on Petri Nets and Other Models of Concurrency XII
Publisher	Springer Verlag
Pages	140-165
Number of pages	26
ISBN (Print)	9783662558614
DOIs	https://doi.org/10.1007/978-3-662-55862-1_7
Publication status	Published - 2017
Publication type	A4 Article in conference proceedings
Event	INTERNATIONAL CONFERENCE ON APPLICATION AND THEORY OF PETRI NETS AND CONCURRENCY - Duration: 1 Jan 1900 → …

Publication series

Name	Lecture Notes in Computer Science
Volume	10470
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	INTERNATIONAL CONFERENCE ON APPLICATION AND THEORY OF PETRI NETS AND CONCURRENCY
Period	1/01/00 → …

Publication forum classification

Publication forum level 1

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-662-55862-1_7

Cite this

@inproceedings{2e4bae01c15e46499a33704582afca89,

title = "Stubborn set intuition explained",

abstract = "This study focuses on the differences between stubborn sets and other partial order methods. First a major problem with step graphs is pointed out with an example. Then the deadlock-preserving stubborn set method is compared to the deadlock-preserving ample set and persistent set methods. Next, conditions are discussed whose purpose is to ensure that the reduced state space preserves the ordering of visible transitions, that is, transitions that may change the truth values of the propositions that the formula under verification has been built from. Finally solutions to the ignoring problem are analysed both when the purpose is to preserve only safety properties and when also liveness properties are of interest.",

author = "Antti Valmari and Henri Hansen",

note = "jufoid=62555; INTERNATIONAL CONFERENCE ON APPLICATION AND THEORY OF PETRI NETS AND CONCURRENCY ; Conference date: 01-01-1900",

year = "2017",

doi = "10.1007/978-3-662-55862-1_7",

language = "English",

isbn = "9783662558614",

series = "Lecture Notes in Computer Science",

publisher = "Springer Verlag",

pages = "140--165",

booktitle = "Transactions on Petri Nets and Other Models of Concurrency XII",

address = "Germany",

}

TY - GEN

T1 - Stubborn set intuition explained

AU - Valmari, Antti

AU - Hansen, Henri

N1 - jufoid=62555

PY - 2017

Y1 - 2017

N2 - This study focuses on the differences between stubborn sets and other partial order methods. First a major problem with step graphs is pointed out with an example. Then the deadlock-preserving stubborn set method is compared to the deadlock-preserving ample set and persistent set methods. Next, conditions are discussed whose purpose is to ensure that the reduced state space preserves the ordering of visible transitions, that is, transitions that may change the truth values of the propositions that the formula under verification has been built from. Finally solutions to the ignoring problem are analysed both when the purpose is to preserve only safety properties and when also liveness properties are of interest.

AB - This study focuses on the differences between stubborn sets and other partial order methods. First a major problem with step graphs is pointed out with an example. Then the deadlock-preserving stubborn set method is compared to the deadlock-preserving ample set and persistent set methods. Next, conditions are discussed whose purpose is to ensure that the reduced state space preserves the ordering of visible transitions, that is, transitions that may change the truth values of the propositions that the formula under verification has been built from. Finally solutions to the ignoring problem are analysed both when the purpose is to preserve only safety properties and when also liveness properties are of interest.

U2 - 10.1007/978-3-662-55862-1_7

DO - 10.1007/978-3-662-55862-1_7

M3 - Conference contribution

AN - SCOPUS:85030723564

SN - 9783662558614

T3 - Lecture Notes in Computer Science

SP - 140

EP - 165

BT - Transactions on Petri Nets and Other Models of Concurrency XII

PB - Springer Verlag

T2 - INTERNATIONAL CONFERENCE ON APPLICATION AND THEORY OF PETRI NETS AND CONCURRENCY

Y2 - 1 January 1900

ER -

Stubborn set intuition explained

Abstract

Publication series

Conference

Publication forum classification

ASJC Scopus subject areas

Access to Document

Fingerprint

Cite this