基于吴方法的多值模型检验

APPLICATION OF WU'S METHOD TO MULTI-VALUED MODEL CHECKING

大型复杂系统的开发过程中不可避免的涉及到非确定或不一致信息的处理,而多值模型检验作为经典模型检验的一种扩展,是处理和分析包含此类信息模型的一种有效手段.提出了一种系统化的多值逻辑(涵盖经典逻辑)的代数表示方法,使用吴方法的基本思想和框架实现复杂系统形式验证中基于多值逻辑的模型检验的代数化,建立了通过吴方法实现多值模型检验技术的整体框架.这种代数化的多值模型检验方法可以作为现有方法的有力补充.

The development of most large and complex systems is necessarily involved with the treatment of uncertainty andinconsistency. Multi-valued model checking is very useful for analyzing models that contain such information. Based on the algebraic representation of multi-valued logics, we present a framework to apply Wu＇s method to multi-valued model checking. This algebraic approach to multi-valued model checking can be used as a powerful supplement to the existing methods.