Heuristic search for equivalence checking

被引：0
作者：
Nicoletta De Francesco
Giuseppe Lettieri
Antonella Santone
Gigliola Vaglini
机构：
[1] University of Pisa,Dipartimento di Ingegneria dell’Informazione
[2] University of Sannio,Dipartimento di Ingegneria
来源：
Software & Systems Modeling | 2016年 / 15卷
关键词：
Heuristic search algorithms; Bisimulation; Concurrent systems; Model checking;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
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. In this paper, we present an efficient procedure, based on heuristic search, for checking well-known bisimulation equivalences for concurrent systems specified through process algebras. The method tries to improve, with respect to other solutions, both the memory occupation and the time required for proving the equivalence of systems. A prototype has been developed to evaluate the approach on several examples of concurrent system specifications.
引用
收藏
页码：513 / 530
页数：17
相关论文
共 42 条
[1]  
Graf S(1996)Compositional minimisation of finite state systems using interface specifications Form. Asp. Comput. 8 607-616
[2]  
Steffen B(2006)An efficient deadlock detection tool for ccs processes J. Comput. Syst. Sci. 72 1397-1412
[3]  
Lüttgen G(1991)Local model checking in the modal mu-calculus Theor. Comput. Sci. 89 161-177
[4]  
Gradara S(1992)A stubborn attack on state explosion Form. Methods Syst. Des. 1 297-322
[5]  
Santone A(2013)Incremental construction of systems: an efficient characterization of the lacking sub-system Sci. Comput. Program. 78 1346-1367
[6]  
Villani ML(1994)Model checking and abstraction ACM Trans. Program. Lang. Syst. 16 1512-1542
[7]  
Stirling C(2012)Abstract reduction in directed model checking ccs processes Acta Inf. 49 313-341
[8]  
Walker D(1998)State space reduction by nonstandard semantics for deadlock analysis Sci. Comput. Program. 30 309-338
[9]  
Valmari A(1985)And/or graph heuristic search methods J. ACM 32 28-51
[10]  
Santone A(1994)Algorithms for searching explicit and/or graphs and their applications to problem reduction search Artif. Intell. 65 329-345
12345