differential refinement logic (dRℒ), a logic with first-class support for refinement relation'/> Differential Refinement Logic<sup>*</sup>
  • 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Annual ACM/IEEE Symposium on Logic in Computer Science >Differential Refinement Logic*
【24h】

Differential Refinement Logic*

机译：差分优化逻辑 *

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We introduce differential refinement logic (dRℒ), a logic with first-class support for refinement relations on hybrid systems, and a proof calculus for verifying such relations. dRℒ simultaneously solves several seemingly different challenges common in theorem proving for hybrid systems: 1. When hybrid systems are complicated, it is useful to prove properties about simpler and related sub-systems before tackling the system as a whole. 2. Some models of hybrid systems can be implementation-specific. Verification can be aided by abstracting the system down to the core components necessary for safety, but only if the relations between the abstraction and the original system can be guaranteed. 3. One approach to taming the complexities of hybrid systems is to start with a simplified version of the system and iteratively expand it. However, this approach can be costly, since every iteration has to be proved safe from scratch, unless refinement relations can be leveraged in the proof. 4. When proofs become large, it is di cult to maintain a modular or comprehensible proof structure. By using a refinement relation to arrange proofs hierarchically according to the structure of natural subsystems, we can increase the readability and modularity of the resulting proof. dRℒ extends an existing specification and verification language for hybrid systems (differential dynamic logic, dℒ) by adding a refinement relation to directly compare hybrid systems. This paper gives a syntax, semantics, and proof calculus for dRℒ. We demonstrate its usefulness with examples where using refinement results in easier and better-structured proofs.
机译：我们介绍 差分优化逻辑 （dRℒ），具有对混合系统上的精炼关系的一流支持的逻辑，以及用于验证这种关系的证明演算。 dRℒ同时解决了混合系统定理证明中常见的几个看似不同的挑战：1.当混合系统复杂时，在解决整个系统之前证明简单和相关子系统的性质很有用。 2.混合系统的某些模型可能是特定于实现的。可以通过将系统抽象到安全所必需的核心组件来辅助验证，但前提是可以保证抽象和原始系统之间的关系。 3.驯服混合系统复杂性的一种方法是从系统的简化版本开始，然后迭代扩展它。但是，这种方法可能会很昂贵，因为必须证明每次迭代都从头开始是安全的，除非可以在证明中利用细化关系。 4.当证明变大时，很难保持模块化或易于理解的证明结构。通过使用细化关系根据自然子系统的结构分层排列证明，我们可以提高结果证明的可读性和模块化。 dRℒ通过添加细化关系来直接比较混合系统，扩展了混合系统的现有规范和验证语言（差分动态逻辑，dℒ）。本文给出了dRℒ的语法，语义和证明演算。我们通过使用精炼结果生成更简单，结构更好的证明的示例来证明其有用性。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号