Fair testing and stubborn sets

Tutkimustuotos › › vertaisarvioitu

Standard

Fair testing and stubborn sets. / Valmari, Antti; Vogler, Walter.

Model Checking Software: 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings. Springer Verlag, 2016. s. 225-243 (Lecture Notes in Computer Science; Vuosikerta 9641).

Tutkimustuotos › › vertaisarvioitu

Harvard

Valmari, A & Vogler, W 2016, Fair testing and stubborn sets. julkaisussa Model Checking Software: 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings. Lecture Notes in Computer Science, Vuosikerta. 9641, Springer Verlag, Sivut 225-243, INTERNATIONAL WORKSHOP ON MODEL CHECKING OF SOFTWARE, 1/01/00. https://doi.org/10.1007/978-3-319-32582-8_16

APA

Valmari, A., & Vogler, W. (2016). Fair testing and stubborn sets. teoksessa Model Checking Software: 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings (Sivut 225-243). (Lecture Notes in Computer Science; Vuosikerta 9641). Springer Verlag. https://doi.org/10.1007/978-3-319-32582-8_16

Vancouver

Valmari A, Vogler W. Fair testing and stubborn sets. julkaisussa Model Checking Software: 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings. Springer Verlag. 2016. s. 225-243. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-319-32582-8_16

Author

Valmari, Antti ; Vogler, Walter. / Fair testing and stubborn sets. Model Checking Software: 23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings. Springer Verlag, 2016. Sivut 225-243 (Lecture Notes in Computer Science).

Bibtex - Lataa

@inproceedings{c4434af35f4a49839613c0b79de5dfa0,

title = "Fair testing and stubborn sets",

abstract = "Partial-order methods alleviate state explosion by considering only a subset of transitions in each constructed state. The choice of the subset depends on the properties that the method promises to preserve. Many methods have been developed ranging from deadlockpreserving to CTL ∗-and divergence-sensitive branching bisimilarity preserving. The less the method preserves, the smaller state spaces it constructs. Fair testing equivalence unifies deadlocks with livelocks that cannot be exited, and ignores the other livelocks. It is the weakest congruence that preserves whether the ability to make progress can be lost. We prove that a method that was designed for trace equivalence also preserves fair testing equivalence. We describe a fast algorithm for computing high-quality subsets of transitions for the method, and demonstrate its effectiveness on a protocol with a connection and data transfer phase. This is the first practical partial-order method that deals with a practical fairness assumption.",

keywords = "Fair testing equivalence, Fairness, Partial-order methods, Progress",

author = "Antti Valmari and Walter Vogler",

year = "2016",

doi = "10.1007/978-3-319-32582-8_16",

language = "English",

isbn = "9783319325811",

series = "Lecture Notes in Computer Science",

publisher = "Springer Verlag",

pages = "225--243",

booktitle = "Model Checking Software",

address = "Germany",

}

RIS (suitable for import to EndNote) - Lataa

TY - GEN

T1 - Fair testing and stubborn sets

AU - Valmari, Antti

AU - Vogler, Walter

PY - 2016

Y1 - 2016

N2 - Partial-order methods alleviate state explosion by considering only a subset of transitions in each constructed state. The choice of the subset depends on the properties that the method promises to preserve. Many methods have been developed ranging from deadlockpreserving to CTL ∗-and divergence-sensitive branching bisimilarity preserving. The less the method preserves, the smaller state spaces it constructs. Fair testing equivalence unifies deadlocks with livelocks that cannot be exited, and ignores the other livelocks. It is the weakest congruence that preserves whether the ability to make progress can be lost. We prove that a method that was designed for trace equivalence also preserves fair testing equivalence. We describe a fast algorithm for computing high-quality subsets of transitions for the method, and demonstrate its effectiveness on a protocol with a connection and data transfer phase. This is the first practical partial-order method that deals with a practical fairness assumption.

AB - Partial-order methods alleviate state explosion by considering only a subset of transitions in each constructed state. The choice of the subset depends on the properties that the method promises to preserve. Many methods have been developed ranging from deadlockpreserving to CTL ∗-and divergence-sensitive branching bisimilarity preserving. The less the method preserves, the smaller state spaces it constructs. Fair testing equivalence unifies deadlocks with livelocks that cannot be exited, and ignores the other livelocks. It is the weakest congruence that preserves whether the ability to make progress can be lost. We prove that a method that was designed for trace equivalence also preserves fair testing equivalence. We describe a fast algorithm for computing high-quality subsets of transitions for the method, and demonstrate its effectiveness on a protocol with a connection and data transfer phase. This is the first practical partial-order method that deals with a practical fairness assumption.

KW - Fair testing equivalence

KW - Fairness

KW - Partial-order methods

KW - Progress

U2 - 10.1007/978-3-319-32582-8_16

DO - 10.1007/978-3-319-32582-8_16

M3 - Conference contribution

SN - 9783319325811

T3 - Lecture Notes in Computer Science

SP - 225

EP - 243

BT - Model Checking Software

PB - Springer Verlag

ER -

TUTCRIS