Refinement And Symmetry Reduction Of Multi-valued Models Based On Bilattice

Model checking is an automatic verification technology for the system behavior. The traditionalmodel checking is for the system model based on Boolean logic. All the behaviors of the system needto be described determinately. However, the users’ requirements may be uncertain or their views areinconsistent in many stages of software development, such as on the demand analysis stage. Themodel may contain uncertain or inconsistent information. The traditional Boolean model cannotsatisfy this requirement, but multiple valued model is suitable for modeling and analysis in such cases.General multi-valued model is defined on De Morgan algebra, as an extension of the traditionalBoolean model. Similar to traditional model checking, State explosion problem also exists inmulti-value model checking. The methods to solve problem of state explosion are based on refinement,such as abstract and symmetry reduction. The refinement preserves property of original model andreduced model. The definitions of the existing refinements of multi-valued model are too strong, sothe application of the existing refinement is limited. To this end, we first put forward a new and moregeneralized refinement of multi-valued models, and on this basis, we study the symmetry reduction ofthe multi-value models.Our stdudy is based on world-based bilattice. The bilattice has two orders: truth order andinformation order. Any De Morgan algebra is isomorphic to the sublattice of world-based bilattice.The model checking of the behaviors can be defined on truth order, and the accuracy of the modelchecking results as well as the preservation of property between the original model and reduced modelcan be defined according to the information order. To this end, we first define multi-valued modelbased on the world-based bilattice, and the corresponding semantics of μ calculus. Then, we describerefinement of the new multi-valued model from two perspectives:(i) through decomposing themulti-value model into three-valued model,(ii) directly describing it by the structure of multi-valuedmodel. It is proved that these two descriptions are equivalent. They are the necessary and sufficientcondition to preserve the information order of the model checking result of the μ-calculus formula onthe original model and reduced model. We provide the algorithm to recognize the refinement of themulti-valued model states. Furthermore, on basis of the refinement, we define the symmetry reducedquotient structure of multi-value model, and show that the quotient structure and the original modelrefines each other, extending the symmetry reduction to more general multi-valued model.