• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Computer aided verification >Lazy Abstractions for Timed Automata
【24h】

Lazy Abstractions for Timed Automata

机译：定时自动机的惰性抽象

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

摘要

We consider the reachability problem for timed automata. A standard solution to this problem involves computing a search tree whose nodes are abstractions of zones. For efficiency reasons, they are parametrized by the maximal lower and upper bounds (LU-bounds) occurring in the guards of the automaton. We propose an algorithm that dynamically updates LU-bounds during exploration of the search tree. In order to keep them as small as possible, the bounds are refined only when they enable a transition that is impossible in the unabstracted system. So our algorithm can be seen as a kind of lazy CEGAR algorithm for timed automata. We show that on several standard benchmarks, the algorithm is capable of keeping very small LU-bounds, and in consequence is able to reduce the search space substantially.
机译：我们考虑定时自动机的可达性问题。该问题的标准解决方案涉及计算搜索树，其节点是区域的抽象。出于效率原因，它们由自动机保护装置中出现的最大上下限（LU界限）参数化。我们提出了一种算法，可在探索搜索树期间动态更新LU边界。为了使它们尽可能小，仅当边界启用了在抽象系统中不可能发生的过渡时，才对边界进行细化。因此，我们的算法可以看作是定时自动机的一种懒惰CEGAR算法。我们表明，在几个标准基准上，该算法能够保持非常小的LU边界，从而能够显着减少搜索空间。

著录项

  • 来源
    《Computer aided verification》|2013年|990-1005|共16页
  • 会议地点 Saint Petersburg(RU)
  • 作者

    Frederic Herbreteau; B. Srivathsan; Igor Walukiewicz;

  • 作者单位

    Univ. Bordeaux, CNRS, LaBRI, UMR 5800, F-33400 Talence, France;

    Software Modeling and Verification Group, RWTH Aachen University, Germany;

    Univ. Bordeaux, CNRS, LaBRI, UMR 5800, F-33400 Talence, France;

  • 会议组织
  • 原文格式 PDF
  • 正文语种 eng
  • 中图分类
  • 关键词

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号