Safety Property-Driven Stubborn Sets

Henri Hansen; Antti Valmari

doi:10.1007/978-3-319-45994-3_7

Safety Property-Driven Stubborn Sets

Henri Hansen, Antti Valmari

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

3 Citations (Scopus)

Abstract

A new reduced state space construction method is presented where in every constructed state, the set of transitions that are fired is chosen based on the safety property that is being verified. Typical earlier methods only take the property into account in one state of each cycle or in one state of each terminal strong component of the reduced state space. They may fire totally irrelevant transitions in the other states. Where the property is taken into account, typically many or all enabled transitions are fired. This has spoiled attempts to be property-driven in every state. The present study exploits an idea that was published in 2016 with which this can be avoided. Furthermore, most earlier methods classify the transitions to visible and invisible. The new method uses a novel improved concept. An experiment is presented where the new concept provides significant improvement to the reduction results.

Original language	English
Title of host publication	Reachability Problems
Subtitle of host publication	10th International Workshop, RP 2016, Aalborg, Denmark, September 19-21, 2016, Proceedings
Editors	Kim Larsen, Igor Potapov, Jirí Srba
Publisher	Springer International Publishing
Pages	90-103
Number of pages	14
ISBN (Electronic)	978-3-319-45994-3
ISBN (Print)	978-3-319-45993-6
DOIs	https://doi.org/10.1007/978-3-319-45994-3_7
Publication status	Published - Sept 2016
Publication type	A4 Article in conference proceedings
Event	INTERNATIONAL WORKSHOP ON REACHABILITY PROBLEMS - Duration: 1 Jan 1900 → …

Publication series

Name	Lecture notes in computer science
Publisher	Springer
Volume	9899
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	INTERNATIONAL WORKSHOP ON REACHABILITY PROBLEMS
Period	1/01/00 → …

Publication forum classification

Publication forum level 1

Access to Document

10.1007/978-3-319-45994-3_7

Cite this

Hansen, H., & Valmari, A. (2016). Safety Property-Driven Stubborn Sets. In K. Larsen, I. Potapov, & J. Srba (Eds.), Reachability Problems: 10th International Workshop, RP 2016, Aalborg, Denmark, September 19-21, 2016, Proceedings (pp. 90-103). (Lecture notes in computer science; Vol. 9899). Springer International Publishing. https://doi.org/10.1007/978-3-319-45994-3_7

@inproceedings{a516417329334175b97d59bece7b266e,

title = "Safety Property-Driven Stubborn Sets",

abstract = "A new reduced state space construction method is presented where in every constructed state, the set of transitions that are fired is chosen based on the safety property that is being verified. Typical earlier methods only take the property into account in one state of each cycle or in one state of each terminal strong component of the reduced state space. They may fire totally irrelevant transitions in the other states. Where the property is taken into account, typically many or all enabled transitions are fired. This has spoiled attempts to be property-driven in every state. The present study exploits an idea that was published in 2016 with which this can be avoided. Furthermore, most earlier methods classify the transitions to visible and invisible. The new method uses a novel improved concept. An experiment is presented where the new concept provides significant improvement to the reduction results.",

author = "Henri Hansen and Antti Valmari",

note = "JUFOID=62555; INTERNATIONAL WORKSHOP ON REACHABILITY PROBLEMS ; Conference date: 01-01-1900",

year = "2016",

month = sep,

doi = "10.1007/978-3-319-45994-3_7",

language = "English",

isbn = "978-3-319-45993-6",

series = "Lecture notes in computer science",

publisher = "Springer International Publishing",

pages = "90--103",

editor = "Kim Larsen and Igor Potapov and Jir{\'i} Srba",

booktitle = "Reachability Problems",

}

Hansen, H & Valmari, A 2016, Safety Property-Driven Stubborn Sets. in K Larsen, I Potapov & J Srba (eds), Reachability Problems: 10th International Workshop, RP 2016, Aalborg, Denmark, September 19-21, 2016, Proceedings. Lecture notes in computer science, vol. 9899, Springer International Publishing, pp. 90-103, INTERNATIONAL WORKSHOP ON REACHABILITY PROBLEMS, 1/01/00. https://doi.org/10.1007/978-3-319-45994-3_7

Safety Property-Driven Stubborn Sets. / Hansen, Henri; Valmari, Antti.
Reachability Problems: 10th International Workshop, RP 2016, Aalborg, Denmark, September 19-21, 2016, Proceedings. ed. / Kim Larsen; Igor Potapov; Jirí Srba. Springer International Publishing, 2016. p. 90-103 (Lecture notes in computer science; Vol. 9899).

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

TY - GEN

T1 - Safety Property-Driven Stubborn Sets

AU - Hansen, Henri

AU - Valmari, Antti

N1 - JUFOID=62555

PY - 2016/9

Y1 - 2016/9

N2 - A new reduced state space construction method is presented where in every constructed state, the set of transitions that are fired is chosen based on the safety property that is being verified. Typical earlier methods only take the property into account in one state of each cycle or in one state of each terminal strong component of the reduced state space. They may fire totally irrelevant transitions in the other states. Where the property is taken into account, typically many or all enabled transitions are fired. This has spoiled attempts to be property-driven in every state. The present study exploits an idea that was published in 2016 with which this can be avoided. Furthermore, most earlier methods classify the transitions to visible and invisible. The new method uses a novel improved concept. An experiment is presented where the new concept provides significant improvement to the reduction results.

AB - A new reduced state space construction method is presented where in every constructed state, the set of transitions that are fired is chosen based on the safety property that is being verified. Typical earlier methods only take the property into account in one state of each cycle or in one state of each terminal strong component of the reduced state space. They may fire totally irrelevant transitions in the other states. Where the property is taken into account, typically many or all enabled transitions are fired. This has spoiled attempts to be property-driven in every state. The present study exploits an idea that was published in 2016 with which this can be avoided. Furthermore, most earlier methods classify the transitions to visible and invisible. The new method uses a novel improved concept. An experiment is presented where the new concept provides significant improvement to the reduction results.

U2 - 10.1007/978-3-319-45994-3_7

DO - 10.1007/978-3-319-45994-3_7

M3 - Conference contribution

SN - 978-3-319-45993-6

T3 - Lecture notes in computer science

SP - 90

EP - 103

BT - Reachability Problems

A2 - Larsen, Kim

A2 - Potapov, Igor

A2 - Srba, Jirí

PB - Springer International Publishing

T2 - INTERNATIONAL WORKSHOP ON REACHABILITY PROBLEMS

Y2 - 1 January 1900

ER -

Safety Property-Driven Stubborn Sets

Abstract

Publication series

Conference

Publication forum classification

Access to Document

Fingerprint

Cite this