Stubborn Set Intuition Explained
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Scientific › peer-review
Details
Original language | English |
---|---|
Title of host publication | Petri Nets and Software Engineering 2016 |
Subtitle of host publication | Proceedings of the International Workshop on Petri Nets and Software Engineering 2016, including the International Workshop on Biological Processes & Petri Nets 2016 |
Editors | Lawrence Cabac, Lars Michael Kristensen, Heiko Rölke |
Publisher | CEUR-WS |
Pages | 213-232 |
Number of pages | 20 |
Publication status | Published - 2016 |
Publication type | A4 Article in a conference publication |
Event | International Workshop on Petri Nets and Software Engineering, PNSE 2016, including the International Workshop on Biological Processes and Petri Nets, BioPPN 2016 - Torun, Poland Duration: 20 Jun 2016 → 21 Jun 2016 |
Publication series
Name | CEUR Workshop Proceedings |
---|---|
Publisher | CEUR-WS |
Volume | 1591 |
ISSN (Electronic) | 1613-0073 |
Conference
Conference | International Workshop on Petri Nets and Software Engineering, PNSE 2016, including the International Workshop on Biological Processes and Petri Nets, BioPPN 2016 |
---|---|
Country | Poland |
City | Torun |
Period | 20/06/16 → 21/06/16 |
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.