• 论文 • 上一篇    下一篇

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

赵林(1), 吴尽昭(2)   

  1. (1)北京交通大学轨道交通控制与安全国家重点实验室, 北京 100044; 中国科学院成都计算机应用研究所, 成都 610041; (2)中国科学院成都计算机应用研究所, 成都 610041.
  • 收稿日期:2007-12-30 修回日期:1900-01-01 出版日期:2008-08-25 发布日期:2008-08-25

赵林;吴尽昭. 基于吴方法的多值模型检验[J]. 系统科学与数学, 2008, 28(8): 1020-1029.

ZHAO Lin;WU Jinzhao. Application of Wu's Method to Multi-Valued Model Checking[J]. Journal of Systems Science and Mathematical Sciences, 2008, 28(8): 1020-1029.

Application of Wu's Method to Multi-Valued Model Checking

ZHAO Lin(1), WU Jinzhao(2)   

  1. (1)Chengdu Institute of Computer Applications, CAS, Chengdu 610041; BeijingJiaotong University State Key Laboratory of Rail Traffic Control and Safety, Beijing 100044; (2)Chengdu Institute of Computer Applications, CAS, Chengdu 610041.
  • Received:2007-12-30 Revised:1900-01-01 Online:2008-08-25 Published:2008-08-25
大型复杂系统的开发过程中不可避免的涉及到非确定或不一致信息的处理,而多值模型检验作为经典模型检验的一种扩展,是处理和分析包含此类信息模型的一种有效手段.提出了一种系统化的多值逻辑(涵盖经典逻辑)的代数表示方法,使用吴方法的基本思想和框架实现复杂系统形式验证中基于多值逻辑的模型检验的代数化,建立了通过吴方法实现多值模型检验技术的整体框架.这种代数化的多值模型检验方法可以作为现有方法的有力补充.
The development of most large and complex systems is necessarily involved with the treatment of uncertainty and inconsistency. 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.

MR(2010)主题分类: 

()
[1] 王雯, 王玥, 王文慧, 肖志华. 基于交叉Gram矩阵低秩分解的非对称线性系统的模型降阶[J]. 系统科学与数学, 2021, 41(4): 926-938.
[2] 胡建,曹喜望. 自共轭互反多项式的推广[J]. 系统科学与数学, 2020, 40(8): 1507-1516.
[3] 陈荣军,唐国春. 转包费用有限的两机流水作业排序问题[J]. 系统科学与数学, 2019, 39(9): 1462-1470.
[4] 陈世平,刘忠.  一类超越函数多项式不等式的自动证明[J]. 系统科学与数学, 2019, 39(5): 804-822.
[5] 刘丽,徐溢. 有限域上的广义准多项式码[J]. 系统科学与数学, 2019, 39(3): 470-476.
[6] 李冬梅,粱芮,刘金旺. 二元多项式矩阵Smith型的进一步结果[J]. 系统科学与数学, 2019, 39(12): 1983-1997.
[7] 郭浩,刘湘涛,龚浩博,黄健飞. 基于泛函线性模型的基因水平关联性分析[J]. 系统科学与数学, 2019, 39(11): 1885-1894.
[8] 张晓威,闫会敏,万旭. 基于Legendre多项式的代数信号处理模型[J]. 系统科学与数学, 2018, 38(3): 261-271.
[9] 邓国强,唐敏,张永燊. 一种基于竞争策略的稀疏多元多项式插值算法[J]. 系统科学与数学, 2018, 38(12): 1436-1448.
[10] 胡亦郑,陆征一,罗勇. 低次微分多项式系统的Sibirsky理想生成元的构造[J]. 系统科学与数学, 2018, 38(12): 1497-1505.
[11] 陈世平,刘忠. 指数多项式不等式的自动证明[J]. 系统科学与数学, 2017, 37(7): 1692-1703.
[12] 王砺磊,曾霞,林望,陈鑫,杨争峰. 一个基于多项式约束求解的数值程序测试用例自动生成工具[J]. 系统科学与数学, 2017, 37(7): 1704-1721.
[13] 黄冠利,吕江毅,张华磊. 循环差分-微分模上双变元维数多项式的Gr\"obner基算法[J]. 系统科学与数学, 2017, 37(7): 1722-1728.
[14] 赖义生,段德鑫. 实分片代数超曲面的连通分支数的上界[J]. 系统科学与数学, 2017, 37(10): 2095-2102.
[15] 王燕,李志明.  一类具有优良性质的五点二重逼近细分格式[J]. 系统科学与数学, 2017, 37(10): 2155-2162.
阅读次数
全文


摘要