• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Conference on Computer Aided Verification(CAV 2006); 20060817-20; Seattle,WA(US) >Bounded Model Checking for Weak Alternating Buechi Automata
【24h】

Bounded Model Checking for Weak Alternating Buechi Automata

机译：弱交替Buechi自动机的有界模型检查

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We present an incremental bounded model checking encoding into propositional satisfiability where the property specification is expressed as a weak alternating Biichi automaton (WABA). The encoding is linear in the specification, or, more exactly O(╚OI∣ +k·∣T∣ +k·∣δ∣), where ∣I∣ is the size of the initial state predicate, k is the bound, ∣T∣ is the size of the transition relation, and ∣δ∣ is the size of the WABA transition relation. Minimal length counterexamples can also be found by increasing the encoding size to be quadratic in the number of states in the largest component of the WABA. The proposed encoding can be used to implement more efficient bounded model checking algorithms for ω-regular industrial specification languages such as Accellera's Property Specification Language (PSL). Encouraging experimental results on a prototype implementation are reported.
机译：我们提出了一种渐进式有界模型检查，将其编码成命题可满足性，其中属性规范表示为弱交替Biichi自动机（WABA）。在规范中，编码是线性的，或更准确地说是O（╚OI∣ + k·∣T∣ + k·∣δ∣），其中∣I∣是初始状态谓词的大小，k是边界，∣ T∣是过渡关系的大小，∣δ∣是WABA过渡关系的大小。还可以通过将WABA的最大部分中的状态数增加为二次方的编码大小来找到最小长度的反例。所提出的编码可用于为ω-常规工业规范语言（如Accellera的属性规范语言（PSL））实施更有效的边界模型检查算法。报告了关于原型实现的令人鼓舞的实验结果。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号