• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Verification, model checking, and abstract interpretation >Synthesizing Switching Logic Using Constraint Solving
【24h】

Synthesizing Switching Logic Using Constraint Solving

机译：使用约束求解综合开关逻辑

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

摘要

A new approach based on constraint solving techniques was recently proposed for verification of hybrid systems. This approach works by searching for inductive invariants of a given form. In this paper, we extend that work to automatic synthesis of safe hybrid systems. Starting with a multi-modal dynamical system and a safety property, we present a sound technique for synthesizing a switching logic for changing modes so as to preserve the safety property. By construction, the synthesized hybrid system is well-formed and is guaranteed safe. Our approach is based on synthesizing a controlled invariant that is sufficient to prove safety. The generation of the controlled invariant is cast as a constraint solving problem. When the system, the safety property, and the controlled invariant are all expressed only using polynomials, the generated constraint is an (EA) formula in the theory of reals, which we solve using SMT solvers. The generated controlled invariant is then used to arrive at the maximally liberal switching logic.
机译：最近提出了一种基于约束求解技术的新方法来验证混合系统。该方法通过搜索给定形式的归纳不变量来工作。在本文中，我们将这项工作扩展到安全混合系统的自动综合。从多模式动态系统和安全特性开始，我们提出了一种合理的技术，用于合成用于更改模式的开关逻辑，从而保留安全特性。通过构造，合成的混合系统结构良好，并保证安全。我们的方法基于合成足以证明安全性的受控不变式。受控不变量的生成被转换为约束求解问题。当仅使用多项式来表示系统，安全性和受控不变式时，生成的约束为实数理论中的（EA）公式，我们使用SMT求解器对其进行求解。然后，将所生成的受控不变式用于得出最大自由度的切换逻辑。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号