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

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