Compositional abstraction and safety synthesis using overlapping symbolic models
KTH Royal Institute of Technology（皇家理工学院）；Laboratoire des signaux et systèmes (L2S), CNRS, CentraleSupélec, Université Paris-Sud, Université Paris-Saclay（信号与系统实验室，法国国家科学研究中心，中央苏佩莱克高等学院，巴黎第十一大学，巴黎萨克雷大学）；Univ. Grenoble Alpes/CNRS, GIPSA-Lab（格勒诺布尔阿尔卑斯大学/法国国家科学研究中心，GIPSA实验室）
本文提出了一种组合方法，用于离散时间非线性系统的抽象和安全合成。通过组合一组重叠的符号子系统来定义符号抽象，这些子系统可以共享一些共同的状态变量。利用这种重叠的符号子系统开发了组合安全合成技术，并比较了不同系统分解方式下抽象和控制器的保守性和计算复杂性。数值实验表明，所提出的符号控制合成方法在减少计算复杂性方面优于集中方法，并在减少保守性方面优于使用非重叠子系统的组合方法。
2017-07-19 cs.SY eess.SY
Event-Driven Safe and Resilient Control of Automated and Human-Driven Vehicles under EU-FDI Attacks
University of Connecticut（康涅狄格大学）；Worcester Polytechnic Institute（伍斯特理工学院）
本文提出了一种事件驱动的安全与鲁棒控制框架，用于在EU-FDI攻击下实现CAVs与HDVs的混合交通环境中的安全变道控制。
2026-03-09 cs.SY eess.SY
Compositional Design of Safety Controllers for Large-Scale Stochastic Hybrid Systems
School of Computing, Newcastle University（纽卡斯尔大学计算机学院）
本文提出基于小增益推理的组成方案，用于合成互联随机混合系统的安全控制器。通过引入增强控制子屏障证书，构建互联网络的安全控制器，并在小增益组成条件下推导安全概率的下界。
2026-04-13 cs.SY eess.SY
Data-Driven Compositional Safety Verification of Interconnected Monotone Systems
University of Colorado Boulder（科罗拉多大学博尔德分校）
本文提出一种数据驱动的组合式安全验证方法，利用单调性构建局部区间障碍证书并组合验证互联单调系统，无需显式模型，实验证明其有效且可扩展。
2026-09-18 cs.SY eess.SY
A Compositional Resilience Index for Computationally Efficient Safety Analysis of Interconnected Systems
本文提出一种组合弹性指数，通过构建优化程序计算子系统安全约束的充分条件，并利用线性不等式组高效验证互联系统在故障与攻击下的安全性。
2023-04-04 cs.SY eess.SY
Compositional Controller Synthesis for Interconnected Stochastic Systems with Markovian Switching
在这项工作中，我们提出了一个组合方案的安全控制器的合成互联离散时间随机系统的马尔可夫开关信号。我们提出的方法是基于一个概念，所谓的控制存储证书计算的各个子系统，通过利用它，可以合成状态反馈控制器的互联系统，以执行安全规范在有限的时间范围内。为此，我们采用平方和（SOS）优化方法来搜索多个存储证书的每个开关子系统，同时合成其相应的安全控制器。然后，我们利用耗散性理论的组合构造屏障证书的互联系统的基础上存储证书的各个子系统。所提出的耗散型组合条件可以利用互连拓扑的结构，并独立于子系统的数量或增益来实现。我们最终采用构造的屏障证书和量化的概率上界，互联系统在有限的时间范围内达到某些不安全的区域。我们将我们的研究结果应用于200个房间的室温网络，同时接受多个存储证书。我们合成的安全控制器，以保持每个房间的温度在一个舒适区的有界的时间范围。
2022-08-06 cs.SY eess.SY
Defense Strategies for Autonomous Multi-agent Systems: Ensuring Safety and Resilience Under Exponentially Unbounded FDI Attacks
针对自主多智能体系统在指数无界虚假数据注入攻击下面临的安全与协同挑战，提出了一种结合观测器层防御、控制输入补偿及基于控制障碍函数二次规划的安全感知与攻击弹性控制器，有效保障了系统的安全性与弹性。
2025-05-05 cs.SY eess.SY
A Unified Framework for Attack-Resilient CLF-CBF Quadratic Programs for Nonlinear Control-Affine Systems
University of Connecticut（康涅狄格大学）
本文提出了一种针对非线性控制仿真的攻击鲁棒CLF-CBF二次规划统一框架，通过嵌入统一的自适应补偿项，实现了在控制输入虚假数据注入攻击下有限时间内恢复到名义安全集，无需事先确定攻击幅度上限，仅依赖于增长率分析和在线增益调节律。
2026-05-19 cs.SY eess.SY
Resilient Estimator-based Control Barrier Functions for Dynamical Systems with Disturbances and Noise
University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）
本文提出RE-CBF方法，结合弹性估计器与随机CBF优化，解决动态系统在扰动和噪声下的路径规划安全问题，并通过仿真与真实无人机实验验证其有效性。
2024-06-28 cs.RO cs.SY eess.SY
From Data to Control: A Formal Compositional Framework for Large-Scale Interconnected Networks
针对大规模模型未知互联网络的安全控制问题，提出基于含噪声数据的组合式方法，利用控制存储证书组合推导控制障碍证书，将计算复杂度从多项式降为线性，实现全去中心化安全控制并提供正确性保证。
2025-06-17 cs.SY eess.SY
Transient-Safe and Attack-Resilient Secondary Control in AC Microgrids Under Polynomially Unbounded FDI Attacks
针对交流微电网控制通道的多项式无界FDI攻击，提出一种全分布式暂态安全弹性二次控制策略，通过李雅普诺夫分析证明其可实现频率电压调节的UUB收敛与有功均分，仿真验证了其在不利条件下的可靠性与抗攻击能力。
2024-10-07 cs.SY eess.SY
An Analytical Framework for Control Synthesis of Cyber-Physical Systems with Safety Guarantee
网络物理系统（CPS）需要在故障和恶意攻击下安全运行。单工架构和最近提出的网络弹性架构，例如，拜占庭容错++（BFT++）分别为CPS在故障和恶意网络攻击下提供安全性。然而，这些现有的架构利用不同的定时参数和实现来提供安全性，并且看起来是不相关的。在本文中，我们提出了一个分析框架来表示单纯形，BFT++和其他实用的网络弹性架构（CRA）。我们构建了一个混杂系统，该系统对采用任何这些架构的CPS进行建模。我们得到充分的条件，通过我们提出的框架下，控制策略是保证安全的。我们提出了一个算法来综合控制策略。我们验证了所提出的框架使用的案例研究的横向控制的波音747，并表明，我们提出的方法，确保系统的安全性。
2022-04-01 cs.SY eess.SY
Scenario-Based Compositional Statistical Model Checking for Safety Specifications
University of California, Berkeley（加州大学伯克利分校）
针对安全关键系统中组合场景验证成本高的问题，提出基于场景的组合式统计模型检验框架，通过分解场景与规范、独立验证及重要性采样和核密度估计组合结果，实现高效准确验证并降低模拟成本。
2026-10-06 cs.AI cs.LO cs.RO
Data-Driven Safety Certificates of Infinite Networks with Unknown Models and Interconnection Topologies
School of Computing, Newcastle University（纽卡斯尔大学计算机学院）
本文提出了一种基于组成框架的数据驱动方法，用于验证具有未知数学模型和未知互联拓扑的无限网络的安全性，通过利用子系统的联合耗散性特性，构建安全证书并提供正确性保证。
2026-05-18 cs.SY eess.SY
A Safety Constrained Control Framework for UAVs in GPS Denied Environment
无人机（UAV）在GPS拒绝的环境中遭受传感器漂移，这可能导致潜在的危险情况。为了避免无法容忍的传感器漂移存在的GPS欺骗攻击，我们提出了一个安全约束的控制框架，适应无人机在路径重新规划水平，以支持弹性状态估计对GPS欺骗攻击。攻击检测器用于基于弹性状态估计检测GPS欺骗攻击，并提供鲁棒控制模式和紧急控制模式之间的切换准则。为了量化安全裕度，我们引入逃逸时间，逃逸时间被定义为一个安全时间，在该时间下，状态估计误差保持在指定置信度的容许误差之内。设计了一种攻击者位置跟踪器（ALT），利用滑动窗口输出的无迹卡尔曼滤波器（UKF）跟踪攻击者的位置并估计欺骗设备的输出功率。使用ALT的估计，基于约束模型预测控制器（MPC）设计逃逸控制器（ESC），使得UAV在逃逸时间内从欺骗设备的有效范围逃逸。
2020-04-12 cs.SY eess.SY
Resilient Supervisory Control of Autonomous Intersections in the Presence of Sensor Attacks
本文研究了在传感器攻击存在下自主交叉口的监督控制问题，提出了一种安全、非死锁且最大宽容的抗攻击控制系统，以应对干扰、无控车辆和传感器攻击。
2016-06-21 cs.CR cs.SY eess.SY
Compositional Construction of Control Barrier Certificates for Large-Scale Stochastic Switched Systems
在本文中，我们提出了一个组成框架的建设控制屏障证书的大规模随机切换系统接受多个控制屏障证书与一些停留时间的条件。所提出的计划是基于一个概念，所谓的增广伪屏障证书计算每个切换子系统，使用它可以合成状态反馈控制器的互联系统执行安全规范在有限的时间范围内。特别是，我们首先利用足够的最大型小增益条件，构造增强控制屏障证书的互联系统的基础上，相应的增强伪屏障证书的子系统。然后，我们量化退出概率的上限-互联系统到达某些不安全区域的概率-在有限的时间范围内使用构造的增强屏障证书。我们采用了一种技术的基础上的反例引导归纳合成（CEGIS）的方法来搜索控制屏障证书的每一种模式，同时合成安全控制器提供开关信号。我们证明了我们提出的结果，首先将它们应用到一个包含1000个房间的室温网络。最后，我们将我们的技术应用到一个网络的500个交换子系统（共1000个维度）接受多个障碍证书的停留时间的条件，并提供上界的概率，互联系统在有限的时间范围内达到一些不安全的区域。
2020-05-04 cs.SY eess.SY
Compositional Inductive Invariant Based Verification of Neural Network Controlled Systems
Northeastern University（东北大学）
本文提出一种基于组合归纳不变式的NNCS安全验证方法，通过将归纳性证明义务分解为子问题并自动推断分解谓词，大幅缩短验证时间至数秒。
2024-03-26 cs.LG cs.LO cs.SY
From Formal Methods to Data-Driven Safety Certificates of Unknown Large-Scale Networks
本文提出一种基于含噪声数据的组合式数据驱动框架，通过为未知大规模互联网络的子系统设计控制子屏障证书（CSBC）并组合为全局控制屏障证书（CBC），以去中心化方式实现了鲁棒安全控制，并将计算复杂度从多项式降至线性。
2025-08-13 cs.SY eess.SY
Safety Constrained Multi-UAV Time Coordination: A Bi-level Control Framework in GPS Denied Environment
无人机（UAV）在GPS拒绝环境中遭受传感器漂移，这可能导致安全问题。为避免多无人机系统在完成时间要求严格的协调任务时出现不可容忍的传感器漂移，提出了一种安全约束的双层控制框架。第一级是时间关键协调级，其实现协调状态的一致性并提供作为协调状态的函数的虚拟目标。第二层是安全关键控制层，其设计为跟踪虚拟目标，同时在路径重新规划层调整被攻击的UAV以支持弹性状态估计。特别地，基于多无人机协同任务，通过提出的一致性协议算法，时间关键协调级框架生成虚拟目标的期望速度和位置剖面。安全关键控制级别能够使每个UAV遵循其分配的路径，同时检测攻击，弹性地估计状态，并在逃逸时间内将UAV驱动到欺骗设备的有效范围之外。通过对三无人机系统的数值仿真，验证了所提出的安全约束双层控制框架的有效性。
2020-05-19 cs.MA cs.SY eess.SY
Resilient Interval Observer-Based Control for Cooperative Adaptive Cruise Control under FDI Attack
University of Tulsa（塔尔萨大学）
本文提出了一种结合非线性控制器和区间观测器的控制框架，用于在面对FDI攻击时实现鲁棒的状态估计和安全的协同自适应巡航控制。
2026-01-18 cs.SY eess.SY
Resilient Control of Platooning Networked Robotic Systems via Dynamic Watermarking
联网的机器人系统，如联网的车辆排，可以通过允许高速协调来提高运输网络的安全性和效率。为了实现这种协调，这些系统依赖于网络通信。这可能使他们容易受到网络攻击。虽然加密或专门设计的网络拓扑等安全方法可能会增加成功执行此类攻击的难度，但这些技术无法保证针对攻击者的安全通信。更麻烦的是，这些安全方法无法确保单个代理能够检测到更改特定消息内容的攻击。为了确保在这种攻击下的弹性行为，本文制定了一个网络化的线性时变版本的动态水印，其中每个代理生成并添加一个私人激励到其相应的机器人子系统的输入。本文证明，这种方法可以使网络机器人系统中的每个代理都能够检测网络攻击。通过改变车辆之间发送的测量值，本文说明了攻击者可以在一个队列中创建不稳定的行为。通过利用本文提出的动态水印方法，检测到的攻击，允许车队中的车辆优雅地降级到一个非通信控制策略，保持安全跨越各种场景。
2021-06-14 cs.SY eess.SY math.OC
Symbolic Models for Infinite Networks of Control Systems: A Compositional Approach
本文提出了一个组成框架的符号模型的网络构成的可数无限数量的有限维离散时间控制子系统的建设。我们把这样的网络称为无限网络。所提出的方法是基于交替模拟功能的概念。这个概念将一个具体的网络与它的符号模型联系起来，并保证它们的输出行为之间的不匹配界限。我们提出了一种组合的方法来构建一个符号模型的无限网络，连同交替模拟功能，通过组成符号模型和交替模拟功能构建子系统。假设每个子系统是增量输入到状态稳定的，在一些小增益类型的条件下，我们提出了一个算法，有序地构建本地符号模型与适当设计的量化参数。通过这种方式，所提出的组合方法可以为我们提供一个指导方针，用于构建具有任何期望的近似精度的整体符号模型。还提供了一种组合控制器合成方案，以分散的方式在无限网络上执行安全属性。我们的结果的有效性说明通过道路交通网络由无限多个道路单元。
2021-10-28 cs.SY eess.SY
A Modular Safety Filter for Safety-Certified Cyber-Physical Systems
针对网络化控制系统面临的网络攻击，本文提出一种可与现有控制器和检测器结合的模块化安全滤波器，无需命令可靠性信息，并通过20台移动机器人编队仿真验证其在不可检测智能攻击下的安全保障效果。
2025-05-15 cs.SY eess.SY
Proprioceptive feedback paradigm for safe and resilient motion control
Southwest Research Institute（西南研究所）
本文提出一种类本体反馈机制用于运动控制系统，通过快速反馈环路补偿意外响应，分析了可管理的损伤程度，并提供了全MPF和分MPF两种方案。
2026-03-31 cs.SY eess.SY
Distributed Resilience-Aware Control in Multi-Robot Networks
University of Michigan（密歇根大学）
针对多机器人系统中异常智能体导致的弹性共识难题，提出一种基于控制屏障函数的分布式控制律，仅用局部信息在时变网络中同时保证弹性共识与碰撞避免，并通过仿真验证。
2025-09-10 cs.RO cs.SY eess.SY
Detection and Inference of Randomness-based Behavior for Resilient Multi-vehicle Coordinated Operations
弹性多车辆系统通过交换信息、检测和消除旨在劫持或降低整个系统性能的网络攻击来协作执行任务。在本文中，我们提出了一个框架：i）检测和隔离网络中行为不端的车辆，ii）安全地加密网络中的信息，以提醒和吸引附近的车辆在环境中的兴趣点，而无需明确广播安全关键信息。为了实现这些目标，我们利用分散的虚拟弹簧阻尼器网格物理模型对每个车辆进行编队控制。为了发现网络中任何车辆的不一致行为，我们考虑了一种方法，该方法监视与期望不匹配的车辆间残差的符号行为的变化。同样，为了掩盖重要信息并触发车辆切换到不同的行为，我们利用车辆状态的侧信道信息，并描述了一个隐藏的弹簧阻尼器签名模型，该模型可被邻居车辆检测到。我们的框架证明了在模拟和实验中的编队无人地面车辆（UGV）的存在下，恶意的人在中间的通信攻击。
2021-10-05 cs.SY eess.SY
Compositional Planning for Logically Constrained Multi-Agent Markov Decision Processes
针对多智能体系统时序逻辑约束控制策略设计难、传统分解方法保守的问题，提出基于CMDPs框架的假设-保证分解方法，可生成高概率满足约束且奖励接近最优的去中心化策略，同时大幅降低问题规模与计算耗时。
2024-10-05 cs.SY eess.SY
Critical Load Restoration using Distributed Energy Resources for Resilient Power Distribution System
极端天气事件对老化和过时的配电基础设施产生重大影响。这些高影响低概率（HILP）事件通常会导致长期停机和关键服务的损失，从而严重影响客户的安全。这就需要在灾难期间迅速恢复关键服务，以确保配电网络的复原力。本文提出了一种先进的馈线恢复方法，恢复关键负荷使用分布式能源（DER）。提出了一种弹性恢复方法，联合最大限度地提高恢复的关键负载的量，并通过优化分配网格的可用DER资源，优化恢复时间。恢复问题被建模为一个混合整数线性规划的目标是最大限度地提高恢复后故障的恢复能力，同时满足电网的关键连接和操作约束，并确保一个给定的开环馈线配置的径向操作。仿真结果表明，所提出的方法使用IEEE 123节点馈线与5 DER供应11个关键负荷和IEEE 906总线馈线与3 DER供应17个关键负荷的有效性。DER的可用性和燃料储备恢复网络的影响进行了评估，它表明，所提出的方法是成功地能够恢复最大数量的临界负载使用可用的DER。
2019-12-10 cs.SY eess.SY
Cyber-Resilient Data-Driven Event-Triggered Secure Control for Autonomous Vehicles Under False Data Injection Attacks
本文提出了一种具备网络韧性的数据驱动事件触发安全控制框架，用于提升自动驾驶车辆在虚假数据注入攻击下的安全性和通信效率。
2025-12-13 cs.SY eess.SY
Resilient Model Predictive Control of Distributed Systems Under Attack Using Local Attack Identification
针对分布式系统在恶意攻击下的不确定性问题，提出基于局部信息的模型攻击识别方法，结合分布式模型预测控制构建弹性框架，并在微电网模型上验证了其有效性。
2023-01-13 cs.SY eess.SY
Resilient Cooperative Adaptive Cruise Control for Autonomous Vehicles Using Machine Learning
University of Florida（佛罗里达大学）
协同自适应巡航控制（CACC）是一种基本的互联车辆应用，它通过利用车对车（V2V）通信来扩展自适应巡航控制。CACC是众多自动驾驶汽车功能的关键组成部分，包括队列行驶、分布式路线管理等。不幸的是，恶意V2V通信可能会破坏CACC，导致字符串不稳定和道路事故。在本文中，我们开发了一种新的弹性基础设施，RACCON，用于检测和减轻对CACC的V2V攻击。RACCON使用机器学习来开发车载预测模型，该模型可以捕获异常的车辆响应并实时的执行缓解。支持RACCON的车辆可以利用CACC的高效率，而不会影响安全性，即使在潜在的敌对场景下也是如此。我们提出了广泛的实验评估，以证明RACCON的疗效。
2021-03-18 cs.CR cs.RO cs.SY
Resilient AFE Drive Control using Neural Networks with Tracking Guarantees
本文提出利用神经网络的参考跟踪性能提升方法，提高主动前端驱动器在电网故障时的鲁棒性和安全性。
2025-12-03 cs.SY eess.SY
Trust-Aware Resilient Control and Coordination of Connected and Automated Vehicles
Boston University（波士顿大学）；Massachusetts Institute of Technology（麻省理工学院）
针对CAV通过冲突区域时遭受Sybil攻击及不合作车辆影响的问题，提出基于信任框架的去中心化弹性控制与协调方案，保证无碰撞安全并缓解拥堵。
2023-06-03 cs.AI cs.MA cs.SY
Composing Control Barrier Functions for Complex Safety Specifications
California Institute of Technology（加州理工学院）
本文针对复杂安全规范问题，提出将状态约束布尔组合转化为单一连续可微控制障碍函数的算法框架，并验证其安全控制效果。
2023-12-03 cs.RO cs.SY eess.SY
Certified Closed-Loop Control for Packet Networks: A Compositional Certification Framework
Lancaster University（兰卡斯特大学）；University of Cambridge（剑桥大学）；Nanjing University of Information Science and Technology（南京信息工程大学）；Tianjin University（天津大学）
本文提出一种组合认证框架，通过在提议者与数据平面之间插入认证算子，将候选动作投影到满足证书的可执行动作或报告不可行并执行有量化松弛的默认动作，从而保证数据包网络在延迟、部分状态信息等条件下的安全性、稳定性与组合性。
2026-06-01 cs.NI cs.SY eess.SY
Strategy Templates for Almost-Sure and Positive Winning of Stochastic Parity Games towards Permissive and Resilient Control
本工作将策略模板概念从确定性博弈推广至随机博弈，覆盖两种获胜准则与五种目标，提出构建模板及提取获胜策略的算法，以实现宽容且弹性的控制器设计。
2025-10-16 cs.LO cs.SY eess.SY
Resilient Scheduling of Control Software Updates in Radial Power Distribution Systems
针对配电系统智能电子设备的控制软件更新推出问题，提出基于非线性DistFlow方程的线性决策模型，将其表述为向量装箱问题，实现了实时生成安全且高效的更新调度方案。
2023-07-23 cs.SY eess.SY math.OC
Trajectory Synthesis for a UAV Swarm to Perform Resilient Requirement-Aware Surveillance: A Smart Grid-based Study
智能电网是一个广泛分布的架空输电线路工程系统。自然灾害或技术故障对这些电力线造成的物理损坏将破坏电网的功能完整性。为了确保在这些现象发生时电网的运行流程能够继续，电网运营商必须立即采取措施消除影响并修复问题，即使这些问题发生在难以到达的偏远地区。新兴的无人机（UAV）显示出巨大的潜力，可以取代传统的人工巡逻，定期监测涉及电网安全的关键情况。关键线路可以由一队无人机监控，以确保有弹性的监控系统。建议的方法考虑了\textit{n}应急分析，以确定传输线的临界性。我们提出了一个正式的框架，验证是否一组给定的无人机（即，无人机群）可以执行满足各种要求的电网的连续监视，特别是监视和弹性规范。验证过程最终为无人机提供了一个轨迹计划，包括加油计划。检查线路上的点的弹性要求用$k-$属性表示，该属性指定如果$k$ UAV发生故障或受损，则仍有UAV在准时内收集该点处的数据。我们评估所提出的框架，基于各种IEEE测试总线系统的合成数据。
2019-11-03 cs.LO cs.SY eess.SP
