GreASE: A Tool for Efficient "Nonequivalence" Checking

Equivalence checking plays a crucial role in formal verification to ensure the correctness of concurrent systems. However, this method cannot be scaled as easily with the increasing complexity of systems due to the state explosion problem. This article presents an efficient procedure, based on heuristic search, for checking Milner's strong and weak equivalence; to achieve higher efficiency, we actually search for a difference between two processes to be discovered as soon as possible, thus the heuristics aims to find a counterexample, even if not the minimum one, to prove nonequivalence. The presented algorithm builds the system state graph on-the-fly, during the checking, and the heuristics promotes the construction of the more promising subgraph. The heuristic function is syntax based, but the approach can be applied to different specification languages such as CCS, LOTOS, and CSP, provided that the language semantics is based on the concept of transition. The algorithm to explore the search space of the problem is based on a greedy technique; GreASE (Greedy Algorithm for System Equivalence), the tool supporting the approach, is used to evaluate the achieved reduction of both state-space size and time with respect to other verification environments.