location: Current position: Home >> Scientific Research >> Paper Publications

Unified Mathematical Framework for Slicing and Symmetry Reduction over Event Structures

Hits:

Indexed by:期刊论文

Date of Publication:2014-01-01

Journal:JOURNAL OF APPLIED MATHEMATICS

Included Journals:SCIE

ISSN No.:1110-757X

Abstract:Nonclassical slicing and symmetry reduction can act as efficient structural abstract methods for pruning state space when dealing with verification problems. In this paper, we mainly address theoretical and algorithmic aspects for nonclassical slicing and symmetry reduction over prime event structures. We propose sliced and symmetric quotient reduction models of event structures and present their corresponding algorithms. To construct the underlying foundation of the proposed methodologies, we introduce strong and weak conflict concepts and a pair of mutually inverse operators and extend permutation group based symmetry notion of event structures. We have established a unified mathematical framework for slicing and symmetry reduction, and further investigated the translation, isomorphism, and equivalence relationship and other related basic facts from a theoretical point of view. The framework may provide useful guidance and theoretical exploration for overcoming verification challenges. This paper also demonstrates their practical applications by two cases.

Pre One:Groebner Bases Based Verification Solution for SystemVerilog Concurrent Assertions

Next One:Wu's method based temporal assertions checking for SEREs properties