A1 Journal article (refereed)
Stubborn Sets, Frozen Actions, and Fair Testing (2021)

Valmari, A., & Vogler, W. (2021). Stubborn Sets, Frozen Actions, and Fair Testing. Fundamenta Informaticae, 178(1-2), 139-172. https://doi.org/10.3233/FI-2021-2001

JYU authors or editors

Publication details

All authors or editors: Valmari, Antti; Vogler, Walter

Journal or series: Fundamenta Informaticae

ISSN: 0169-2968

eISSN: 1875-8681

Publication year: 2021

Volume: 178

Issue number: 1-2

Pages range: 139-172

Publisher: IOS Press

Publication country: Netherlands

Publication language: English

DOI: https://doi.org/10.3233/FI-2021-2001

Publication open access: Not open

Publication channel open access:

Publication is parallel published (JYX): https://jyx.jyu.fi/handle/123456789/74019

Additional information: Special Issue on the 11th International Workshop on Reachability Problems (RP 2017).

Abstract

Many partial order methods use some special condition for ensuring that the analysis is not terminated prematurely. In the case of stubborn set methods for safety properties, implementation of the condition is usually based on recognizing the terminal strong components of the reduced state space and, if necessary, expanding the stubborn sets used in their roots. In an earlier study it was pointed out that if the system may execute a cycle consisting of only invisible actions and that cycle is concurrent with the rest of the system in a non-obvious way, then the method may be fooled to construct all states of the full parallel composition. This problem is solved in this study by a method that “freezes” the actions in the cycle. The new method also preserves fair testing equivalence, making it usable for the verification of many progress properties.

Keywords: data processing; parallel processing; algorithmics

Free keywords: partial order methods; stubborn sets; safety properties; ignoring problem; fair testing

Contributing organizations

Ministry reporting: Yes

Reporting Year: 2021

JUFO rating: 1