Heuristic Search for Equivalence Checking

Organisation:	University of Pisa and University of Sannio (ITALY)
Method:	CCS LOTOS
Tools used:	CWB-NC CADP (Construction and Analysis of Distributed Processes)
Domain:	Concurrency Theory.
Period:	2014-2016
Size:	n/a.
Description:	Equivalence checking plays a crucial role in formal verification since it is a natural relation for expressing the matching of a system implementation against its specification. This work proposes an equivalence checking method based on heuristic search techniques on AND/OR graphs. A key assumption of heuristic search is that a utility or cost can be assigned to each state to guide the search by suggesting the next state to expand; in this way, the most promising paths are considered first. The heuristic functions are syntactically defined on the CCS process algebra. The heuristic search equivalence checking method has been implemented (for strong and weak equivalence) in a prototype tool and compared with the equivalence checking implementations provided by CWB-NC and CADP on a number of case studies. Regarding strong equivalence, the heuristic search method outperforms the other tools, although CADP exhibits better time performance in some cases (e.g., for the MUTUAL case study). Regarding weak equivalence, while its memory occupation is higher, CADP shows a better performance in general.
Conclusions:	Heuristic search proves to be a viable alternative in improving the performance of equivalence checking. Experimental evidence was provided of the reduction in both state space and running time that may result when applying the heuristic search method with respect to CWB-NC and CADP, when checking strong equivalence. For weak equivalence, the performance of the heuristic search method is lower than CADP in terms of analysis scalability, and comparable with CADP in terms of memory space reduction. Quoting [DeFrancesco-Lettieri-Santone-Vaglini-16]: CADP uses very efficient algorithms, and great attention is devoted to implementation efficiency issues.
Publications:	[DeFrancesco-Lettieri-Santone-Vaglini-16] N. De Francesco, G. Lettieri, A. Santone, and G. Vaglini. "Heuristic Search for Equivalence Checking". Software and Systems Modeling 15(2):513-530, May 2016. Available on-line from https://www.researchgate.net/profile/Gigliola_Vaglini/publication/285414779_Heuristic_search_for_equivalence_checking/links/567293e208ae54b5e462b908/Heuristic-search-for-equivalence-checking.pdf and from the CADP Web site in PDF or PostScript
Contact:	Prof. Nicoletta De Francesco Dipartimento di Ingegneria dell'Informazione University of Pisa Via Diotisalvi, 2 I-56126 Pisa ITALY Tel: +39 (50) 2217527 Email: n.defrancesco@ing.unipi.it
Further remarks:	This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies

Back to the CADP case studies page