Maurice Laveaux ; Jan Friso Groote ; Tim A. C. Willemse - Correct and Efficient Antichain Algorithms for Refinement Checking

lmcs:5775 - Logical Methods in Computer Science, February 1, 2021, Volume 17, Issue 1 - https://doi.org/10.23638/LMCS-17(1:8)2021
Correct and Efficient Antichain Algorithms for Refinement CheckingArticle

Authors: Maurice Laveaux ; Jan Friso Groote ORCID; Tim A. C. Willemse

    The notion of refinement plays an important role in software engineering. It is the basis of a stepwise development methodology in which the correctness of a system can be established by proving, or computing, that a system refines its specification. Wang et al. describe algorithms based on antichains for efficiently deciding trace refinement, 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 additional run time improvements can be obtained by applying divergence-preserving branching bisimulation minimisation.


    Volume: Volume 17, Issue 1
    Published on: February 1, 2021
    Accepted on: October 30, 2020
    Submitted on: September 20, 2019
    Keywords: Computer Science - Logic in Computer Science

    4 Documents citing this article

    Consultation statistics

    This page has been seen 1144 times.
    This article's PDF has been downloaded 298 times.