Switched Systems as Hybrid Programs
现实世界中的系统往往具有离散和连续动态之间的相互作用。已经使用各种混合系统形式来建模和分析这种动态组合，范围从数学描述，例如，使用脉冲微分方程和开关，自动机理论和基于语言的方法。本文桥接两个这样的形式主义，显示如何切换系统的各种类别可以建模使用的语言的混合程序从微分动态逻辑（dL）。由此产生的模型，使正式规格说明和验证切换系统使用dL和现有的演绎验证工具，如KeYmaera X。切换系统也提供了一个自然的途径推广的dL的演绎证明理论的微分方程。本文证明的切换系统不变量的完备性结果，使这些系统的安全性验证有效的dL。
2021-04-29 cs.LO cs.SY eess.SY
Hybrid Metaheuristic Optimization of Distributed Control System Hardware Architecture with Model-Based Verification
NEXT engineering, LLC（NEXT工程有限公司）
本文提出一种混合蚁群算法框架，用于在部分工艺参数不确定的情况下设计低成本、高可靠性的分布式控制系统硬件架构，并通过硫磺酸厂案例验证了方法的有效性。
2026-05-14 cs.SY eess.SY
Abstraction of Elementary Hybrid Systems by Variable Transformation
Chongqing Key Lab. of Automated Reasoning and Cognition, CIGIT, CAS（中国科学院重庆智能技术研究院）；State Key Lab. of Comput. Sci., Institute of Software, CAS（中国科学院软件研究所）
本文提出通过变量变换将基本混合系统转换为多项式混合系统，以解决其验证难题，利用现有工具提升安全性验证效率。
2015-01-14 cs.SY eess.SY
SOS-based Stability Verification for Saturated INDI Control of Hybrid-VTOL Aircraft Pitch Rate Dynamics
Université Côte d‘Azur I3S CNRS（蔚蓝海岸大学）；Swiss Federal Institute of Technology (ETH) Zurich（苏黎世联邦理工学院）
针对混合VTOL飞行器的饱和增量非线性动态逆（INDI）俯仰角速率控制器，通过等效循环平衡网络（REN）表示，利用平方和（SOS）规划合成局部Lyapunov函数，获得考虑执行器饱和的吸引域内估计，实现非线性稳定性验证。
2026-06-15 cs.SY eess.SY
Approximate Safety Verification and Control of Partially Observable Stochastic Hybrid Systems
University of Oxford（牛津大学）；University of New Mexico（新墨西哥大学）
本文针对离散时间随机混合系统在观测噪声或不完整时的安全性保证问题，提出两种近似求解动态规划的方法，通过马尔可夫决策过程和径向基函数分别近似信息状态，并通过点基值迭代生成子最优控制策略。
2015-07-06 cs.SY eess.SY math.OC
Multicriteria design and experimental verification of hybrid renewable energy systems. Application to electric vehicle charging stations
安装电动汽车充电站（EVCS）对于促进电动汽车（EV）用户的接受至关重要。然而，如果EVCS完全由电网供电，则可能会对其稳定性产生负面影响，并可能增加CO2排放。为EVCS引入混合可再生能源系统（HRES）可以通过减少电网负荷和产生清洁电力来应对这两个缺点。本文提出了一种基于加权多准则过程的方法来设计最合适的HRES在EVCS的配置。该方法确定当地可再生资源和EVCS电力需求。然后，综合考虑环境、经济和技术等因素，推导出最适合电动汽车控制系统的HRES设计方案。此外，实验阶段，以验证从多准则过程推导出的设计。因此，在EVCS的HRES的最终设计支持不仅是一个完整的数值评估，但也通过实验验证的需求被完全覆盖。瓦伦西亚（西班牙）的方法应用证明，离网HRES与太阳能光伏，风能资源和电池的支持将是最合适的配置系统。该方案也得到了实验验证。
2021-03-31 cs.SY eess.SY
Characterization, Verification and Computation of Robust Controlled Invariants for Monotone Dynamical Systems
本文针对离散时间单调动力系统，基于偏序关系分类，提出鲁棒受控不变量的集合与轨迹表征，并给出验证与计算算法，示例证明其有效性。
2023-06-24 cs.SY eess.SY
Towards Deductive Verification of Control Algorithms for Autonomous Marine Vehicles
针对自主海洋航行器混合系统特性导致控制算法形式化安全验证困难的问题，提出结合GNU/Octave数值计算与Isabelle证明助手的验证方法，可验证多模式切换控制器的微分不变量。
2020-06-16 cs.SE cs.SY eess.SY
Approximate probabilistic verification of hybrid systems
Harvard Medical School（哈佛医学院）；University of Pittsburgh（匹兹堡大学）；Institute de Recherche en Informatique de Toulouse（图卢兹信息技术研究所）；National University of Singapore（新加坡国立大学）
本文提出了一种基于马尔可夫链的混合系统概率验证方法，通过将模式转换视为随机事件，利用BLTL规范验证系统在高概率下的符合性。
2015-06-20 cs.SY eess.SY
A unified framework for modeling and implementation of hybrid systems with synchronous controllers
University of Auckland（奥克兰大学）
本文提出了一种新的方法，用于在线性混合自动机方法中包含非即时的离散控制转换。通过扩展同步子集的SystemJ编程语言，研究了如何用同步编程语言控制持续变化的模拟植物，并提供了一种合理的重写语义来近似连续变量在离散域中的演化。
2015-01-23 cs.PL cs.SY eess.SY
Structural Analysis of Hybrid-Trace Nets: An Optimization Approach
针对混合迹网的安全验证，提出可达性松弛方法，高效识别不变量以缩减状态空间，实验证明在更多实例中证明不可达且生成更多不变量、速度更快。
2026-10-08 cs.LO cs.SY eess.SY
Verifying Switched System Stability With Logic
切换系统表现出微妙的（不）稳定行为，要求系统设计者仔细分析闭环系统的稳定性，从他们提出的切换控制律。本文提出了一种形式化的方法来验证切换系统的稳定性，融合了经典的思想，从控制和验证文献使用微分动态逻辑（dL），逻辑演绎验证的混杂系统。从控制，我们使用标准的稳定性概念，各类开关机制和相应的李雅普诺夫函数为基础的分析技术。从验证，我们使用dL的能力，以验证量化属性的混杂系统和切换系统的dL模型作为循环的混合程序，其稳定性可以正式指定和证明，通过找到适当的循环不变量，即，在每次循环迭代中保留的属性。这种思想的融合使基于dL的KeYmaera X证明器能够可靠地实现切换系统稳定性验证。对于标准类的开关机制，实现提供了全自动的稳定性证明，包括搜索合适的李雅普诺夫函数。此外，演绎方法的一般性还使得能够通过适当地表达这些控制律背后的特定直觉的回路不变量的设计来验证需要非标准稳定性参数的切换控制律。这种灵活性证明了三个案例研究：一个模型的纵向飞行控制的Branicky，自动巡航控制器，和Brockett的非完整积分。
2022-04-08 cs.LO cs.SY eess.SY
Weak Singular Hybrid Automata
Indian Institute of Technology - Bombay（印度孟买理工学院）
本文研究弱奇异混合自动机，证明其可达性问题为NP完全，LTL模型检验为PSPACE完全，并探讨扩展后的问题不确定性。
2014-06-19 cs.CC cs.FL cs.SY
Counterexample-guided computation of polyhedral Lyapunov functions for hybrid systems
针对不确定连续时间线性混杂系统，提出了一种计算凸分段线性（多面体）李雅普诺夫函数的反例引导迭代算法。多面体李雅普诺夫函数提供了一种替代常用的多项式李雅普诺夫函数。我们的方法首先表征多面体李雅普诺夫函数的内在属性，包括其“偏心率”和“鲁棒性”的扰动。然后，我们推导出一个算法，要么计算一个多面体李雅普诺夫函数证明系统是稳定的，或得出结论，没有多面体李雅普诺夫函数存在的偏心率和鲁棒性参数满足一些用户提供的限制。值得注意的是，我们的方法没有先验界限的线性件，使所需的多面体李雅普诺夫函数的数量。该算法在学习步骤和验证步骤之间交替，始终保持证人状态的有限集。学习步骤求解线性规划以计算与见证状态的有限集兼容的候选李雅普诺夫函数。在验证步骤中，我们的方法验证候选的李雅普诺夫函数是否是一个有效的李雅普诺夫函数的系统。如果验证失败，我们会获得一个新的证人。我们证明了我们的算法所需的最大迭代次数的理论界。我们证明了该算法的数值例子的适用性。
2022-06-22 cs.SY eess.SY math.OC
CODEV: Automated Model Predictive Control Design and Formal Verification (Tool Paper)
Coordinated Science Laboratory, University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校协同科学实验室）
CODEV工具通过自动化分析MPC系统，提供对安全性的严格保证，结合离线计算的MPC解决方案与物理系统形成混合自动机，验证控制律是否能鲁棒维持约束。
2018-04-07 cs.SY eess.SY
