Stubborn Sets, Frozen Actions, and Fair Testing
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
Published inFundamenta Informaticae
© 2021 IOS Press
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.
ISSN Search the Publication Forum0169-2968
Publication in research information system
MetadataShow full item record
Showing items with similar title or keywords.
A Detailed Account of The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction Neele, Thomas; Valmari, Antti; Willemse, Tim A. C. (Logical Methods in Computer Science e.V., 2021)One of the most popular state-space reduction techniques for model checking is partial-order reduction (POR). Of the many different POR implementations, stubborn sets are a very versatile variant and have thus seen many ...
The Inconsistent Labelling Problem of Stutter-Preserving Partial-Order Reduction Neele, Thomas; Valmari, Antti; Willemse, Tim A. C (Springer, 2020)In model checking, partial-order reduction (POR) is an effective technique to reduce the size of the state space. Stubborn sets are an established variant of POR and have seen many applications over the past 31 years. One ...
Partial-order reduction for parity games and parameterised Boolean equation systems Neele, Thomas; Willemse, Tim A. C.; Wesselink, Wieger; Valmari, Antti (Springer, 2022)In model checking, reduction techniques can be helpful tools to fight the state-space explosion problem. Partial-order reduction (POR) is a well-known example, and many POR variants have been developed over the years. ...
All congruences below stability-preserving fair testing or CFFD Valmari, Antti (Springer, 2020)In process algebras, a congruence is an equivalence that remains valid when any subsystem is replaced by an equivalent one. Whether or not an equivalence is a congruence depends on the set of operators used in building ...
Analysis of errors caused by incomplete knowledge of material data in mathematical models of elastic media Mali, Olli (University of Jyväskylä, 2011)