@book{d8261e6eca98415da165f90ce31cd563,
title = "Correct and efficient antichain algorithms for refinement checking",
abstract = "Refinement checking plays an important role in system verification. This means that the correctness of the system is established by showing a refinement relation between two models; one for the implementation and one for the specification. In [22], Wang et al. describe an algorithm based on antichains for efficiently deciding stable failures refinement and failures-divergences refinement. We identify several issues pertaining to the soundness and performance in these algorithms and propose new, correct, antichain-based algorithms. Using a number of experiments we show that our algorithms outperform the original ones in terms of running time and memory usage. Furthermore, we show that applying divergence-preserving branching bisimulation reduction results in additional run time improvements. ",
author = "Maurice Laveaux and Groote, \{Jan Friso\} and Tim Willemse",
year = "2019",
language = "English",
series = "Computer science reports",
publisher = "Technische Universiteit Eindhoven",
}