• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文期刊>Journal of logic and computation >Differential-algebraic Dynamic Logic for Differential-algebraic Programs
【24h】

Differential-algebraic Dynamic Logic for Differential-algebraic Programs

机译：微分代数程序的微分代数动态逻辑

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

摘要

We generalize dynamic logic to a logic for differential-algebraic (DA) programs, I.e. discrete programs augmented with first-order differential-algebraic formulas as continuous evolution constraints in addition to first-order discrete jump formulas. These programs characterize interacting discrete and continuous dynamics of hybrid systems elegantly and uniformly. For our logic, we introduce a calculus over real arithmetic with discrete induction and a new differential induction with which DA programs can be verified by exploiting their differential constraints algebraically without having to solve them. We develop the theory of differential induction and differential refinement and analyse their deductive power. As a case study, we present parametric tangential roundabout maneuvers in air traffic control and prove collision avoidance in our calculus.
机译：我们将动态逻辑概括为微分代数（DA）程序的逻辑，即除一阶离散跳跃公式外，离散程序还增加了作为连续演化约束的一阶微分代数公式。这些程序以优雅和一致的方式描述了混合系统的相互作用的离散和连续动力学。对于我们的逻辑，我们引入了具有离散归纳法的实数算术演算和一种新的差分归纳法，通过该演算，DA程序可以通过代数利用它们的差分约束来进行验证，而不必求解它们。我们发展了微分感应和微分细化的理论，并分析了它们的演绎能力。作为案例研究，我们提出了空中交通管制中的参数切向回旋操作，并在我们的演算中证明了避免碰撞的能力。

著录项

相似文献

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

客服邮箱：kefu@zhangqiaokeyan.com

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

  • 客服微信

  • 服务号