Correct and Efficient Antichain Algorithms for Refinement Checking

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.

• Publication year

  2019

• Venue

  Formal Techniques for (Networked and) Distributed Systems

• Publication date

  2019-02-26

• Fields of study

  Computer Science

• Identifiers
  DOI 10.23638/LMCS-17(1:8)2021arXiv 1902.09880
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• The mCRL2 Toolset for Analysing Concurrent Systems - Improvements in Expressivity and Usability

  2019cited by this paper
• An O(m log n) algorithm for branching bisimilarity on labelled transition systems

  2019cited by this paper
• Modeling and Verifying Concurrent Data Structures

  2018cited by this paper
• FDR: From Theory to Industrial Application

  2017cited by this paper
• A Branching Time Model of CSP

  2017cited by this paper
• Formalising the Dezyne Modelling Language in mCRL2

  2017cited by this paper
• An O(mlogn) Algorithm for Computing Stuttering Equivalence and Branching Bisimulation

  2017cited by this paper
• Computing maximal weak and other bisimulations

  2016cited by this paper
• Modelling the Haemodialysis Machine with Circus

  2016cited by this paper
• FDR3: a parallel refinement checker for CSP

  2016cited by this paper
• FDR3 - A Modern Refinement Checker for CSP

  2014cited by this paper
• An Overview of the mCRL2 Toolset and Its Recent Advances

  2013cited by this paper
• More Anti-chain Based Refinement Checking

  2012cited by this paper
• The art of multiprocessor programming by Maurice Herlihy and Nir Shavit

  2011cited by this paper
• Understanding Concurrent Systems

  2010cited by this paper
• Antichain Algorithms for Finite Automata

  2010cited by this paper
• When Simulation Meets Antichains

  2010cited by this paper
• Branching Bisimilarity with Explicit Divergence

  2008cited by this paper
• Generalizing the Paige-Tarjan algorithm by abstract interpretation

  2006cited by this paper
• A practical nonblocking queue algorithm using compare-and-swap

  2000cited by this paper
• Theories of Programming Languages: Communicating Sequential Processes

  1998cited by this paper
• Branching time and abstraction in bisimulation semantics

  1996cited by this paper
• Model-checking CSP

  1994influential reference
• The Linear Time - Branching Time Spectrum II

  1993cited by this paper
• Three Partition Refinement Algorithms

  1987cited by this paper
• Failures without chaos: a new process semantics for fair abstraction

  1987influential reference
• An Improved Failures Model for Communicating Processes

  1984cited by this paper
• CCS expressions, finite state processes, and three problems of equivalence

  1983cited by this paper
• Correct and Efficient Antichain Algorithms for Refinement Checking

  year unknowncited by this paper

• Dezyne: Paving the Way to Practical Formal Software Engineering

  2021influential citation
• Modelling and Analysing Software in mCRL2

  2019cites this paper
• Interface protocol inference to aid understanding legacy software components

  2018cites this paper