分布式混合系统量化微分动态逻辑的完备公理化
计算机科学中的逻辑
2016-12-02 v3 编程语言
动力系统
摘要
我们解决了信息物理系统中出现的动力学组合与分析所支持的动力学种类有限之间的根本性不匹配问题。现代应用结合了通信、计算和控制。它们甚至可能形成动态分布式网络，其中结构和维度在系统遵循混合动力学（即离散和连续动力学的混合）时均不保持不变。我们为弥合这一分析差距提供了逻辑基础。我们开发了分布式混合系统的形式模型，它将量化微分方程与量化赋值及动态维度变化相结合。我们引入了一种用于验证分布式混合系统的动态逻辑，并提出了该逻辑的证明演算。这是首个针对分布式混合系统的形式化验证方法。我们证明了相对于量化微分方程，我们的演算是对分布式混合系统行为的可靠且完备的公理化。在我们的演算中，即使道路上可能动态出现无限数量的新车辆，我们也证明了分布式汽车控制中的无碰撞性。
引用
@article{arxiv.1206.3357,
title = {A Complete Axiomatization of Quantified Differential Dynamic Logic for Distributed Hybrid Systems},
author = {Andre Platzer},
journal= {arXiv preprint arXiv:1206.3357},
year = {2016}
}