• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Science of Computer Programming >Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces
【24h】

Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces

机译：具有大离散状态空间的线性混合自动机的精确和完全符号验证

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

摘要

We propose an improved symbolic algorithm for the verification of linear hybrid automata with large discrete state spaces (where an explicit representation of discrete states is difficult). Here both the discrete part and the continuous part of the hybrid state space are represented by one symbolic representation called LinAIGs. LinAIGs represent (possibly non-convex) polyhedra extended by Boolean variables. Key components of our method for state space traversal are redundancy elimination and constraint minimization: redundancy elimination eliminates so-called redundant linear constraints from LinAIG representations by a suitable exploitation of the capabilities of SMT (Satisfiability Modulo Theories) solvers. Constraint minimization optimizes polyhedra by exploiting the fact that states already reached in previous steps can be interpreted as "don't cares" in the current step. Experimental results (including comparisons to the state-of-the-art model checkers PHAVer and RED) demonstrate the advantages of our approach.
机译：我们提出了一种改进的符号算法，用于验证具有大离散状态空间（其中离散状态的显式表示很困难）的线性混合自动机。这里，混合状态空间的离散部分和连续部分都由一种称为LinAIG的符号表示形式表示。 LinAIG表示由布尔变量扩展的（可能是非凸的）多面体。我们用于状态空间遍历的方法的关键组成部分是冗余消除和约束最小化：冗余消除通过适当地利用SMT（可满足性模理论）求解器的能力，从LinAIG表示中消除了所谓的冗余线性约束。约束最小化通过利用以下事实来优化多面体：在先前步骤中已经达到的状态可以在当前步骤中解释为“无关紧要”。实验结果（包括与最先进的模型检查器PHAVer和RED的比较）证明了我们方法的优势。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号