• 不 限
  • 期刊论文
  • 硕博论文
  • 会议论文
  • 报 纸
  • 英文论文
  2. 您的位置
  3. 首页
  4. 期刊论文
  5. 一种基于时态逻辑的有限状态系统验证方法

一种基于时态逻辑的有限状态系统验证方法

来源 :西北工业大学学报 | 被引量 : 0次 | 上传用户：qilinsanshao
【摘 要】
：
LPTL(Linear Proposition Temporal Logic)与自动机之间有着紧密的联系,结合LPTL语义和语法,提出一种从LPTL公式导出Bchi自动机的方法.导出的Bchi自动机所接受的语言准确地表
【作 者】
：
杜慧敏 杨红丽 高德远 韩俊刚 
【机 构】
：
西北工业大学,西安邮电学院
【出 处】
：
西北工业大学学报
【发表日期】
：
2004年期
【关键词】
：
命题时态逻辑 Bchi自动机 形式化验证 
【基金项目】
：
国家自然科学基金
下载到本地 , 更方便阅读
下载此文 赞助VIP
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
LPTL(Linear Proposition Temporal Logic)与自动机之间有着紧密的联系,结合LPTL语义和语法,提出一种从LPTL公式导出Bchi自动机的方法.导出的Bchi自动机所接受的语言准确地表达了LPTL公式所描述的特性.从而把由LPTL公式描述的系统设计规范的验证问题转换成检验Bchi自动机的包含问题.
其他文献
1例孤独症伴自残行为患者行核磁辅助下脑深部核团射频毁损术的护理
患者男性,30岁,自幼高级神经功能发育迟缓,性格孤僻,不与他人交流.3岁时至精神病专科医院诊断为"孤独症".7岁时开始出现双手拳击头部,睡眠时能停止.1987年至精神病专科医院诊
期刊
孤独症自残行为术中核磁射频毁损术护理
遗传算法在永磁电机气隙磁场设计中的应用
讨论了表面磁钢结构的永磁电机磁极形状的设计问题.表面磁钢结构的永磁电机磁场波形由磁钢的形状确定.如果磁场波形已知,通过求解电磁场反问题就可以获得理想的磁钢形状.其求
期刊
永磁电机电磁场反问题遗传算法
微栓子阳性动脉硬化性脑梗死患者的临床特点以及微栓子的转归
目的 比较经颅多普勒微栓子监测有、无微栓子信号的颅内大动脉狭窄所致急性脑梗死患者的临床特点,观察微栓子信号的转归.方法 收集存在颅内大动脉狭窄的发病7 d内的急性脑梗
期刊
脑梗死微栓子监测磁共振成像弥散Cerebral infarctionMicroembolic signal monitoringDiffusion
体外受精-胚胎移植夫妇心理干预的研究进展
20世纪90年代世界卫生组织(WHO)统计资料显示,全球约有15%育龄夫妇存在不育问题.不孕症是一种身心疾病,患者的社会心理压力显著高于正常生育者,为其治疗带来了负面影响.辅助
期刊
不孕症体外受精-胚胎移植心理问题综述文献
基于神经网络的电液飞行模拟器抗负载干扰控制策略
针对电液飞行模拟器存在的强负载干扰 ,提出一种基于神经网络补偿的新方法 ,它充分吸收了结构不变性原理补偿方法的优点 ,有效地消除了负载扰动的影响 .理论分析、仿真及实验
期刊
飞行模拟器负载干扰神经网络结构不变性原理
培养基介导的旁观者细胞凋亡的研究进展
国内外很多肿瘤研究都观察到旁观者效应诱导的细胞凋亡的存在,且细胞凋亡是旁观者效应重要的检测终点,对肿瘤治疗的疗效有着重要影响.旁观者效应能引起细胞死亡(包括凋亡)、
期刊
旁观者效应细胞凋亡培养基介导
干预方法采血在新生儿疾病筛查足跟血采集中的应用效果
目的 比较干预方法与传统方法采集新生儿足跟血标本的效果.方法 对接受新生儿疾病筛查的180例新生儿,随机分为干预组和对照组,每组各90例.干预组新生儿采用干预方法采血,对照
期刊
新生儿疾病筛查足跟血样采集
早产儿脑室周围白质软化研究现状
脑室周围白质软化(PVL)是早产儿脑损伤主要神经病理学形式,与长期神经行为缺陷密切相关.PVL病因复杂,涉及到解剖学、生理学、细胞学及生物学等方面.其发病机制不甚清楚,自由
期刊
脑室周围白质软化发病机制兴奋毒性少突胶质细胞早产儿
血管内皮生长因子与慢性阻塞性肺疾病继发肺动脉高压的关系
血管内皮生长因子(vascular endothelial growth factor,VEGF)是一种重要的血管内皮细胞丝裂原和通透因子.肺血管的重塑与慢性阻塞性肺疾病(chronic obstructive pulmonary d
期刊
血管内皮生长因子慢性阻塞性肺疾病肺动脉高压肺血管重塑Vascular endothelial growth factorChronic obstruc
125I粒永久植入及89SrCl2治疗雄激素非依赖型伴骨转移前列腺癌
目的　探讨12 5I粒永久植入及氯化锶 [89SrCl2 ]静脉注射治疗雄激素非依赖型伴骨转移前列腺癌的疗效 .方法　在直肠B超引导下 ,经会阴穿刺将12 5I粒子植入到前列腺组织中进行
期刊
前列腺癌骨转移癌125I粒子89SrCl2