混合系统

混合系统（hybrid system）是同时包括连续及离散动态特性的动力系统，这类系统中同时有“流”（flow，以微分方程描述）以及跳跃（以有限状态机或自动机理论描述）的特性。有时也会用混合动态系统（hybrid dynamical system）这个词语，比较不会和结合人工神经网络及模糊逻辑的系统，或是同时应用电子及机械的系统混唏。混合系统的好处是其结构可以包括更多种类的系统，在针对系统特性建模时也有更大的弹性。

一般而言，混合系统的状态可以用连续变数的值以及其他离散的模式来表示。状态可能依照其“流条件”（flow condition）有连续性的变化，或依照控制图（control graph）有离散的变化。只要所谓的不变量维持不变，就会有连续性的变化，不过若满足了特定的跳跃条件，就会有离散转态。离散转态也可能和事件有关。

例子

混合系统可以用来为许多系统进行建模，包括有碰撞的物理系统、逻辑动态控制器，甚至是互联网拥堵问题等。

弹跳球

弹跳球（英语：bouncing ball）属于有碰撞的物理系统，混合系统中的经典范例。在此例中，球（以点状质量表示）由启始高度掉到地面弹跳，每一次的弹跳都会耗散能量。球在每一次弹跳之间都是连续的动态特性，当球碰到地面时，因为非弹性碰撞，球的速度会有离散的变化。弹跳球的数学模型如下：令 $x_{1}$ 是球的高度， $x_{2}$ 是球的速度，其混合系统如下：

当 $x\in C=\{x_{1}>0\}$ ，“流”的统御方程为 ${\dot {x_{1}}}=x_{2},{\dot {x_{2}}}=-g$ , 其中 $g$ 为因为重力而有的加速度，上述方程指出，若球在地面之上，最终会因为重力而掉到地面。

若 $x\in D=\{x_{1}=0\}$ ，“跳跃”的统御方程为 $x_{1}^{+}=x_{1},x_{2}^{+}=-\gamma x_{2}$ , 其中 $0<\gamma <1$ 为耗散系数。方程式是当高度为零（和地面碰撞）时，其速度符号会相反，且会以 $\gamma$ 的比例减少。这也是非弹性碰撞的特性。

弹跳球系统的特点是有Zeno行为。Zeno行为有严格的数学定义，可以大致描述为系统在有限时间内进行了无限次的“跳跃”。在此例中，弹跳球每次碰到地面，就会损失能量，因此之后碰到地面的时间间隔也就会越来越接近。

混合系统的验证

有关混合系统的形式验证，有些方法可以自动证明一些混合系统的特性，验证混合系统安全性的常用工具包括可到达集的计算、抽象模型检查（英语：Abstraction model checking）以及barrier certificate（英语：barrier certificate）。

大部分的验证工作都是不可判定问题^[1]，因此没有办法找出通用的验证算法。不过，这些工具会在指标性问题上展现其分析能力。这些可以验证所有强健案例的混合系统验证法^[2]带来一个可能的理论性结论：混合系统中的许多问题虽然是不可判定的，但至少是准可判定的^[3]。

其他建模方式

基本的混合系统建模方式可以分为两种：隐式以及显式。显式的方式会用混合自动机（英语：hybrid automaton）、混合程式或是混合Petri网表示。隐式的作法会用统御方程式来表示，因此会得到微分代数方程（英语：differential algebraic equation）（DAE）的系统，也有可以透过混合键结图来表示。

若是考虑混合系统分析的统一仿真方法，有一种以DEVS（英语：DEVS）形式化为基础的方法，其中微分方程的积分子会量化为原子性的DEVS模型。该方法以离散事件系统的行为产生系统的轨迹，和离散时间系统不同。在参考资料[Kofman2004]、[CF2006]及[Nutaro2010]中有描述该作法的细节，而软件工具PowerDEVS（英语：PowerDEVS）中也有描述。

参考资料

^ Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya: What's Decidable about Hybrid Automata, Journal of Computer and System Sciences, 1998
^ Martin Fränzle: Analysis of Hybrid Systems: An ounce of realism can save an infinity of states, Springer LNCS 1683
^ Stefan Ratschan: Safety verification of non-linear hybrid systems is quasi-decidable, Formal Methods in System Design, volume 44, pp. 71-90, 2014, doi:10.1007/s10703-013-0196-2

延伸阅读

Henzinger, Thomas A., The Theory of Hybrid Automata, 11th Annual Symposium on Logic in Computer Science (LICS), IEEE Computer Society Press: 278–292, 1996, （原始内容存档于2010-01-27）
Alur, Rajeev; Courcoubetis, Costas; Halbwachs, Nicolas; Henzinger, Thomas A.; Ho, Pei-Hsin; Nicollin, Xavier; Olivero, Alfredo; Sifakis, Joseph; Yovine, Sergio, The algorithmic analysis of hybrid systems, Theoretical Computer Science, 1995, 138 (1): 3–34, doi:10.1016/0304-3975(94)00202-T, （原始内容存档于2010-01-27）
Goebel, Rafal; Sanfelice, Ricardo G.; Teel, Andrew R., Hybrid dynamical systems, IEEE Control Systems Magazine, 2009, 29 (2): 28–93, doi:10.1109/MCS.2008.931718
Acary, Vincent; Brogliato, Bernard, Numerical Methods for Nonsmooth Dynamical Systems, Lecture Notes in Applied and Computational Mechanics, 2008, 35
[Kofman2004] Kofman, E, Discrete Event Simulation of Hybrid Systems, SIAM Journal on Scientific Computing, 2004, 25 (5): 1771–1797, doi:10.1137/S1064827502418379
[CF2006] Francois E. Cellier and Ernesto Kofman, Continuous System Simulation first, Springer, 2006, ISBN 978-0-387-26102-7
[Nutaro2010] James Nutaro, Building Software for Simulation: Theory, Algorithms, and Applications in C++ first, Wiley, 2010

外部链接

IEEE CSS Committee on Hybrid Systems

[1] Thomas A. Henzinger, Peter W. Kopke, Anuj Puri, and Pravin Varaiya: What's Decidable about Hybrid Automata, Journal of Computer and System Sciences, 1998

[2] Martin Fränzle: Analysis of Hybrid Systems: An ounce of realism can save an infinity of states, Springer LNCS 1683

[3] Stefan Ratschan: Safety verification of non-linear hybrid systems is quasi-decidable, Formal Methods in System Design, volume 44, pp. 71-90, 2014, doi:10.1007/s10703-013-0196-2

[1]

[2]

[3]

例子

弹跳球

混合系统的验证

其他建模方式

相关条目

参考资料

延伸阅读

外部链接