要解决的问题:为了提供LTL(线性时间逻辑)模型检查系统,LTL模型检查方法和LTL模型检查程序,即使没有LTL表情的人也可以轻松地确认LTL表情。解决方案:LTL模型检查系统100包括可变值序列集生成装置3,该可变值序列集生成装置3生成某些可变值序列的组合,该LTL模型中包括的变量具有在预定序列长度中可能的值。检查装置4在将由可变值序列集合产生装置3产生的可变值序列代入LTL模型时,确定是否建立了LTL模型。
版权:(C)2009,日本特许厅&INPIT
公开/公告号JP2009187416A
专利类型
公开/公告日2009-08-20
原文格式PDF
申请/专利权人 NEC CORP;
申请/专利号JP20080028384
发明设计人 HAYAKAWA YUSHI;
申请日2008-02-08
分类号G06F11/36;
国家 JP
入库时间 2022-08-21 19:46:02