Tampere University of Technology

TUTCRIS Research Portal

Fair testing and stubborn sets

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


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 a conference publication
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 → …


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.


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

Publication forum classification

Field of science, Statistics Finland

Downloads statistics

No data available