Correct and efficient antichain algorithms for refinement checking

Onderzoeksoutput: Bijdrage aan tijdschriftTijdschriftartikelAcademicpeer review

Samenvatting

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.

Originele taal-2Engels
Artikelnummer8
Pagina's (van-tot)8:1-8:40
Aantal pagina's40
TijdschriftLogical Methods in Computer Science
Volume17
Nummer van het tijdschrift1
DOI's
StatusGepubliceerd - 2021

Vingerafdruk Duik in de onderzoeksthema's van 'Correct and efficient antichain algorithms for refinement checking'. Samen vormen ze een unieke vingerafdruk.

Citeer dit