用于网络物理系统的量化状态混合自动机
Quantized State Hybrid Automata for Cyber-Physical Systems
AI总结：
本文提出量化状态混合自动机(QSHA)用于模拟复杂系统，通过动态量子方法提高离散事件检测的准确性，并在仿真步骤上显著优于传统方法。
摘要：
网络物理系统涉及由离散控制器控制的物理过程，例如自动驾驶汽车和植入式医疗设备，这些系统对安全至关重要。混合自动机(HA)基于的正式方法正被用于CPS的规范和验证。HA结合了被控系统的模型及其离散控制器，形成一个分段连续系统，具有不连续性。准确检测这些不连续性，使用适当的穿越检测器，是基于HA的CPS模拟的关键挑战。现有技术使用时间离散数值积分和括号法进行穿越检测。这些技术涉及回溯，且高度非确定性，因此容易出错。由于穿越发生在连续变量的值上，量化状态系统(QSS)积分可能更合适。现有基于固定量子的QSS积分器也不适合模拟HA。这是因为所选量子不依赖于HA守卫条件，这些是不连续性的主要原因。因此，我们提出了一种新的基于动态量子的正式模型，称为量化状态混合自动机(QSHA)。开发的正式模型和相关的仿真框架保证了(1)所有穿越都被准确检测，(2)穿越时间在浮点误差范围内也准确。有趣的是，基准测试结果表明，所提出的仿真技术相比标准的QSS-1、Runge-Kutta(RK)-45和微分代数系统求解器(DASSL)积分方法分别减少了720、1.33和4.41倍的仿真步骤。
英文摘要：
Cyber-physical systems involve a network of discrete controllers that control physical processes. Examples range from autonomous cars to implantable medical devices, which are highly safety critical. Hybrid Automata (HA) based formal approach is gaining momentum for the specification and validation of CPS. HA combines the model of the plant along with its discrete controller resulting in a piece-wise continuous system with discontinuities. Accurate detection of these discontinuities, using appropriate level crossing detectors, is a key challenge to simulation of CPS based on HA. Existing techniques employ time discrete numerical integration with bracketing for level crossing detection. These techniques involve back-tracking and are highly non-deterministic and hence error prone. As level crossings happen based on the values of continuous variables, Quantized State System (QSS)- integration may be more suitable. Existing QSS integrators, based on fixed quanta, are also unsuitable for simulating HAs. This is since the quantum selected is not dependent on the HA guard conditions, which are the main cause of discontinuities. Considering this, we propose a new dynamic quanta based formal model called Quantized State Hybrid Automata (QSHA). The developed formal model and the associated simulation framework guarantees that (1) all level crossings are accurately detected and (2) the time of the level crossing is also accurate within floating point error bounds. Interestingly, benchmarking results reveal that the proposed simulation technique takes 720, 1.33 and 4.41 times fewer simulation steps compared to standard Quantized State System (QSS)-1, Runge-Kutta (RK)-45, and Differential Algebraic System Solver (DASSL) integration based techniques respectively.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
