Correct and efficient antichain algorithms for refinement checking

Research output: Contribution to journalArticleAcademic

43 Downloads (Pure)

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 "More Anti-chain Based Refinement Checking", 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.
Original languageEnglish
Article number1902.09880
Number of pages28
JournalarXiv
Publication statusPublished - 26 Feb 2019

Bibliographical note

28 pages, 6 figures, technical report

Keywords

  • cs.LO

Fingerprint

Dive into the research topics of 'Correct and efficient antichain algorithms for refinement checking'. Together they form a unique fingerprint.

Cite this