支持Stutter-不变性的命题区间时序逻辑

• 作者: 杨琛 段振华
• 来源期刊: 西安电子科技大学学报（自然科学版）
• 学科: 工学
• 关键词: 模型检测 时序逻辑 状态爆炸
• 年，卷（期）: 2011,（2）
• 页码范围: 151-156
• 分类号: TP301
• 字数: 5139字
• 语种: 中文
• DOI: 10.3969/j.issn.1001-2400.2011.02.027

摘要

为了将命题区间时序逻辑(PITL)应用于组合验证,并降低组合产生的状态爆炸风险,提出了支持Stutter-不变性的命题区间时序逻辑PITLst.PITLst继承了PITL的结构相关性,可表达所有PITL能够表达的Stutter-不变性质,支持模块抽象约简系统规模,降低了状态爆炸风险.自动加油站模型的组合验证实例表明,PITLst可有效应用于组合验证技术.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	段振华	西安电子科技大学计算理论与技术研究所	47	363	10.0	16.0
5	杨琛	西安电子科技大学计算理论与技术研究所	4	29	3.0	4.0