Fair testing and stubborn sets

Antti Valmari, Walter Vogler

    Research output: Chapter in Book/Report/Conference proceedingConference contributionScientificpeer-review

    12 Citations (Scopus)
    27 Downloads (Pure)


    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.

    Original languageEnglish
    Title of host publicationModel Checking Software
    Subtitle of host publication23rd International Symposium, SPIN 2016, Co-located with ETAPS 2016, Eindhoven, The Netherlands, April 7-8, 2016, Proceedings
    PublisherSpringer Verlag
    Number of pages19
    ISBN (Print)9783319325811
    Publication statusPublished - 2016
    Publication typeA4 Article in conference proceedings
    EventInternational Workshop on Model Checking Software -
    Duration: 1 Jan 1900 → …

    Publication series

    NameLecture Notes in Computer Science
    ISSN (Print)0302-9743
    ISSN (Electronic)1611-3349


    ConferenceInternational Workshop on Model Checking Software
    Period1/01/00 → …


    • Fair testing equivalence
    • Fairness
    • Partial-order methods
    • Progress

    Publication forum classification

    • Publication forum level 1

    ASJC Scopus subject areas

    • General Computer Science
    • Theoretical Computer Science


    Dive into the research topics of 'Fair testing and stubborn sets'. Together they form a unique fingerprint.

    Cite this