Provably Correct Controller Synthesis of Switched Stochastic Systems with Metric Temporal Logic Specifications: A Case Study on Power Systems
School for Engineering of Matter, Transport, and Energy, Arizona State University(亚利桑那州立大学物质、运输与能源工程学院);Argonne National Laboratory(阿贡国家实验室)
针对具有度量时序逻辑(MTL)规范的切换随机控制系统,提出了一种可证明正确的控制器综合方法。首先给出了切换随机控制系统的随机控制互模拟函数,该函数以概率的方式限制了切换随机控制系统与其标称确定性控制系统之间的轨迹发散.然后,我们开发了一种方法来计算最优控制输入的确定性控制系统的标称轨迹与初始状态变化和随机不确定性的鲁棒性解决一个优化问题。我们实现了我们的鲁棒随机控制器的综合方法上的四总线电力系统和九总线电力系统下的发电损耗干扰,MTL规格表示的要求,电网频偏,风力涡轮发电机转子速度的变化和功率流的限制,在不同的电力线。
2021-03-26 cs.AI cs.SY eess.SY
Efficient Strategy Synthesis for Switched Stochastic Systems with Distributional Uncertainty
针对噪声分布存在 Wasserstein 模糊不确定性的离散时间切换随机系统,提出基于鲁棒 MDP 抽象与线性规划的高效策略综合方法,以最大化有界或无界时间 reach-avoid 概率。
2024-05-17 cs.SY eess.SY
Analysis and Synthesis of Switched Optimization Algorithms
University of Stuttgart(斯图加特大学)
本文提出了一种具有认证指数收敛速率的离散时间优化算法,能够有效应对通信网络中的时间延迟和切换动态问题。
2026-03-10 cs.SY eess.SY math.OC
A finite-sample bound for identifying partially observed linear switched systems from a single trajectory
HUN-REN SZTAKI and ELTE(HUN-REN SZTAKI和ELTE);Univ. Lille, CNRS, Centrale Lille, UMR 9189 CRIStAL;HUN-REN SZTAKI
该研究针对单轨迹下的线性切换系统辨识问题,推导了基于马尔可夫参数估计与Ho-Kalman算法变体的辨识算法的有限样本概率误差界,证明其在二次稳定假设下的统计一致性,为该场景下首个此类结果。
2025-05-16 cs.LG cs.SY eess.SY
Counter-Example Guided Synthesis of Control Lyapunov Functions for Switched Systems
University of Colorado, Boulder(科罗拉多大学博尔德分校)
本文提出利用反例引导归纳综合(CEGIS)方法自动综合切换系统的控制Lyapunov函数(CLF),通过LMI松弛方法解决非线性约束问题,并在基准测试中验证了该方法的计算可行性。
2015-09-17 cs.SY eess.SY
Compositional Abstraction-based Synthesis for Networks of Stochastic Switched Systems
在本文中,我们提供了一个组合的方法来构建有限的抽象(a.k.a.有限马尔可夫决策过程(MDP))的互联离散时间随机切换系统。所提出的框架是基于一个概念的随机模拟功能,使用它可以采用一个抽象的系统作为替代原来的控制器设计过程中的输出轨迹上的保证误差界。为此,我们首先提供随机切换子系统的互连和它们的有限抽象通过随机模拟功能之间的概率接近保证。然后,我们利用足够的小增益类型的条件来显示这项工作的组合性结果。之后,我们证明了在标准假设下,确保切换系统的增量输入到状态稳定性(即,存在共同的增量李雅普诺夫函数,或多个增量李雅普诺夫函数与驻留时间),人们可以构造有限的MDP的一般设置的非线性随机切换系统。我们还提出了一种方法来构造有限的MDP的一类特殊的非线性随机切换系统。为了证明我们所提出的结果的有效性,我们首先将我们的方法应用到一个由200个单元组成的圆形级联环中的道路交通网络,并构造一个有限的MDP的网络组成。我们采用构造的有限抽象作为替代品,合成的政策,保持交通密度低于20辆车每细胞。然后,我们将我们提出的技术完全互连的网络的500个非线性子系统(共1000维),并构建其有限的MDP保证误差界。我们将我们提出的结果与文献中的结果进行了比较。
2019-12-24 cs.SY eess.SY
Invariance Control Synthesis for Switched Systems: An Interval Analysis Approach
University of Waterloo(滑铁卢大学)
本文研究离散时间切换非线性系统不变性控制问题,提出基于区间分析的方法,通过有限次迭代计算受控不变集并直接生成基于分区的不变控制器,无需子系统有共同平衡点。
2016-08-30 cs.SY eess.SY math.OC
Model Reduction of Linear Switched Systems by Restricting Discrete Dynamics
Aalborg University(奥尔堡大学);École des Mines de Douai(杜埃国立高等矿业学院)
本文提出一种方法,通过减少离散时间线性切换系统的连续状态数,在部分切换序列下保持系统行为一致,为混合系统抽象控制合成方法提供支持。
2014-09-11 cs.SY eess.SY
Control Synthesis of Nonlinear Sampled Switched Systems using Euler's Method
CMLA, CNRS & ENS Paris-Saclay(CMLA, 法国国家科学研究中心与巴黎萨克雷高等师范学院);LMT, CNRS & ENS Paris-Saclay(LMT, 法国国家科学研究中心与巴黎萨克雷高等师范学院);LSV, CNRS, INRIA & ENS Paris-Saclay(LSV, 法国国家科学研究中心、法国国家信息与自动化研究所与巴黎萨克雷高等师范学院)
本文提出了一种针对非线性采样切换系统控制综合的方法,该系统向量场满足单侧利普希茨条件。通过欧拉方法构建近似模型以生成保证控制,通过选择合适的时空离散化来限制符号建模引入的误差。
2017-04-11 cs.NA cs.SY eess.SY
Control of nonlinear switched systems based on validated simulation
ENSTA(国立高等先进技术学院)
本文提出了一种基于状态空间二分法的非线性切换系统控制合成算法,利用验证模拟考虑有界扰动和变化参数,适用于安全关键应用。
2016-11-21 cs.SY eess.SY
Arbitrarily Fast Switched Distributed Stabilization of Partially Unknown Interconnected Multiagent Systems: A Proactive Cyber Defense Perspective
最近已经开发了一个设计框架,以分布式方式稳定互连的多智能体系统,并系统地捕捉网络物理系统的架构方面。然而,这种控制理论框架导致稳定化协议,该稳定化协议相对于网络攻击是被动的,并且关于保证的弹性水平是保守的。我们将控制层拓扑结构和稳定增益视为自由度,并开发了一个混合控制和网络安全设计框架来解决上述问题。从控制的角度来看,尽管代理层建模的不确定性和扰动,我们提出了一个新的一步一步的过程来设计一组控制子层的控制层拓扑结构的任意快速切换。从积极的网络防御的角度来看,我们提出了一个可满足性模理论公式,以获得一组控制子层结构的安全考虑,并提供这些子层的频繁和快速的突变,使控制层拓扑结构将保持不可预测的对手。我们证明了两层互联多智能体系统的鲁棒输入到状态稳定性,并通过仿真验证了所提出的思想。
2021-11-19 cs.CR cs.SY eess.SY
Synthesis of Partially Observed Jump-Diffusion Systems via Control Barrier Functions
在本文中,我们研究部分可观测跳跃扩散系统的控制策略的形式化综合复杂的逻辑规格。给定一个状态估计器,我们利用一个离散化的方法,通过使用一个符号的控制障碍函数,而不需要任何知识的估计精度的控制策略的正式合成。我们的目标是合成一个离线控制策略,提供(可能最大化)部分观察到的跳跃扩散系统的轨迹满足确定性有限自动机表达的一些复杂规范的概率下界。最后,我们说明了所提出的结果的有效性,通过合成一个政策的喷气发动机的例子。
2021-09-23 cs.SY eess.SY
Hybrid Control Technique for Switched LPV Systems and Its Application to Active Magnetic Bearing System
North Carolina State University(北卡罗来纳州立大学)
本文提出了一种混合控制方法,用于解决切换LPV系统中的参数变化问题,并应用于主动磁 bearings 系统,通过迟滞切换减少振荡并提高稳定性。
2026-02-21 cs.SY eess.SY
Deterministic and probabilistic algorithms for stabilizing discrete-time switched linear systems
Indian Institute of Technology Bombay(印度理工学院孟买分校)
本文研究了用于稳定离散时间切换线性系统的切换信号算法合成,提出了一种基于加权有向图的切换信号设计方法,并讨论了确定性和概率性算法在设计满足稳定切换条件的切换信号中的应用。
2014-09-17 cs.SY eess.SY math.OC
Compositional Construction of Control Barrier Certificates for Large-Scale Stochastic Switched Systems
在本文中,我们提出了一个组成框架的建设控制屏障证书的大规模随机切换系统接受多个控制屏障证书与一些停留时间的条件。所提出的计划是基于一个概念,所谓的增广伪屏障证书计算每个切换子系统,使用它可以合成状态反馈控制器的互联系统执行安全规范在有限的时间范围内。特别是,我们首先利用足够的最大型小增益条件,构造增强控制屏障证书的互联系统的基础上,相应的增强伪屏障证书的子系统。然后,我们量化退出概率的上限-互联系统到达某些不安全区域的概率-在有限的时间范围内使用构造的增强屏障证书。我们采用了一种技术的基础上的反例引导归纳合成(CEGIS)的方法来搜索控制屏障证书的每一种模式,同时合成安全控制器提供开关信号。我们证明了我们提出的结果,首先将它们应用到一个包含1000个房间的室温网络。最后,我们将我们的技术应用到一个网络的500个交换子系统(共1000个维度)接受多个障碍证书的停留时间的条件,并提供上界的概率,互联系统在有限的时间范围内达到一些不安全的区域。
2020-05-04 cs.SY eess.SY
Finite-Time Stability of Switched and Hybrid Systems with Unstable Modes
本文研究了存在不稳定模态的切换与混合系统的有限时间稳定性,提出了基于多个 Lyapunov 函数的充分条件,允许函数在连续流和离散跳变期间增加,从而降低了保守性,并设计了有限时间稳定的输出反馈控制器。
2019-12-17 cs.SY eess.SY
Verification of Switched Stochastic Systems via Barrier Certificates
提出了一种连续时间切换随机系统的时序逻辑验证方法。我们的目标是找到一个复杂的时间属性满足在有限的时间范围内的概率的下限。所需的时间属性的系统表示使用一个片段的线性时序逻辑,称为安全的LTL相对于有限的痕迹。我们的方法结合了基于自动机的验证和屏障证书的使用。它依赖于分解的自动机与规范的否定成一系列更简单的可达性任务和计算这些可达性概率的上限,通过共同的或多个障碍证书。通过应用反例引导归纳合成框架来寻找障碍证书,说明了理论结果。
2021-09-25 cs.LO cs.SY eess.SY
Controller Synthesis of Wind Turbine Generator and Energy Storage System with Stochastic Wind Variations under Temporal Logic Specifications
在本文中,我们提出了一种控制器综合方法的风力涡轮发电机(WTG)和能量存储系统的度量时序逻辑(MTL)规范,可证明的概率保证在随机环境中的风力发电。MTL规范是对电网频偏、WTG转子速度变化和不同线路的功率流约束的要求。提出了随机控制互模拟函数,该函数以概率的方式限制了切换随机控制系统和切换标称控制系统的轨迹的发散,通过求解确定性控制系统标称轨迹的优化问题,设计了一个前馈控制器,该前馈控制器对初始状态变化和随机不确定性具有鲁棒性.然后,我们从模拟轨迹的数据生成反馈控制律。我们实现了我们的控制方法的四节点系统和九节点系统,并测试了该方法的有效性与发电损失的干扰。我们还测试了反馈控制器的优势时,意外的干扰发生的前馈控制器。
2019-11-26 cs.LO cs.SY eess.SY
Hybrid Control of ADT Switched Linear Systems subject to Actuator Saturation
North Carolina State University(北卡罗来纳州立大学);University of Rhode Island(罗德岛大学)
本文提出了一种针对具有执行器饱和的ADT切换线性系统的混合输出反馈控制方法,通过死区表示处理饱和非线性,并结合模式依赖的动态输出反馈控制器与监督重置机制,确保系统在ADT切换下的指数稳定性与扰动衰减性能。
2026-02-20 cs.SY eess.SY math.OC
idSTLPy: A Python Toolbox for Active Perception and Control
本文描述了一个Python工具箱,用于具有加性高斯干扰和测量噪声的切换线性系统的概率信号时序逻辑(PrSTL)公式的主动感知和控制综合。我们实现了一个反例指导的合成策略,结合有界模型检查,线性规划,和采样为基础的运动规划技术。我们说明了我们的方法和工具箱在整个文件中的运动规划的例子与噪声定位的车辆。代码可在\url{https://codeocean.com/capsule/0013534/tree}上获得。
2021-11-04 cs.SY eess.SY
Synthesis of Switching Rules for Ensuring Reachability Properties of Sampled Linear Systems
LSV, ENS Cachan \& CNRS, 94230 Cachan, France;SATIE, ENS Cachan \& CNRS, 94230 Cachan, France
针对周期采样分段线性动力学系统,提出间接抽象为有限离散事件系统和直接在连续状态空间上工作的两种方法,综合切换规则以确保系统始终停留在给定区域,并通过DC-DC升压转换器案例验证。
2011-11-14 cs.LO cs.SY eess.SY
Recurrent Neural Network Controllers Synthesis with Stability Guarantees for Partially Observed Systems
University of California, Berkeley(加州大学伯克利分校);University of Michigan(密歇根大学);Virginia Tech(弗吉尼亚理工大学)
神经网络控制器由于其灵活性和表现力而在控制任务中变得流行。稳定性是安全关键动力系统的一个重要特性,而部分观测系统的稳定性,在许多情况下,需要控制器保持和处理过去的长期记忆。将一类重要的递归神经网络(RNN)作为非线性不确定部分可观测系统的动态控制器,基于积分二次约束、S引理和序列凸化方法,推导出凸稳定性条件.为了确保在学习和控制过程中的稳定性,我们提出了一个投影的政策梯度方法,迭代地执行的稳定性条件,在重新参数化的空间,利用温和的额外信息系统动态。数值实验表明,我们的方法学习稳定控制器,而使用更少的样本,并取得更高的最终性能相比,政策梯度。
2021-12-07 cs.AI cs.RO cs.SY
Symbolic Models for Stochastic Switched Systems: A Discretization and a Discretization-Free Approach
Technische Universität München(慕尼黑工业大学);University of Oxford(牛津大学);Université de Grenoble(格勒诺布尔大学)
本文提出两种符号抽象技术,用于随机切换系统的稳定性分析与控制器合成,通过构造近似等价的符号模型来满足逻辑规范要求。
2014-07-10 cs.LO cs.SY eess.SY
Computationally Efficient State and Model Estimation via Interval Observers for Partially Unknown Systems
针对含界噪声的部分未知非线性系统,提出一种基于雅可比符号稳定分解、紧分解函数及数据驱动过近似框架的区间观测器,可同时估计状态与学习未知动力学,通过SDP优化增益,仿真验证其计算效率优于已有方法。
2025-04-14 cs.SY eess.SY
On-Line Synthesis of Permissive Supervisors for Partially Observed Discrete Event Systems under scLTL Constraints
研究了部分观测下离散事件系统的监督控制问题,其中控制规范由线性时序逻辑给出。我们设计了一个在线监督器,它利用DES的乘积自动机的完整信息和规范的接受者动态计算其控制动作。可控性和可观测性的概念是通过一个排名功能定义的产品自动机,它降低了它的值,如果接受状态的产品自动机正在接近。建议的在线控制方案利用排名功能和许可功能,它代表了随时间变化的许可水平。其结果是,在线监督实现的规范,意识到其许可和接受的规范之间的权衡,如果产品自动机是可控的和可观察的。
2020-03-27 cs.FL cs.SY eess.SY
Data-Driven Strategy Synthesis for Stochastic Systems with Unknown Nonlinear Disturbances
针对受未知非线性扰动影响的随机切换系统,提出基于观测数据构建歧义集与RMDP抽象、结合LTLf自动机和鲁棒值迭代的策略综合方法,并实证验证其高规范满足概率。
2024-06-14 cs.SY eess.SY
Compositional shield synthesis for safe reinforcement learning in partial observability
针对部分可观测环境下整体式屏蔽合成计算成本高的问题,提出分部分建模安全要求的组合式屏蔽合成方法,使RL智能体在更大规模环境中保持安全并提升奖励收敛与训练效率。
2025-09-15 cs.SY eess.SY
Control Synthesis in Partially Observable Environments for Complex Perception-Related Objectives
Department of Mechanical & Aerospace Engineering, University of Florida(机械与航空航天工程系,佛罗里达大学)
本文针对部分可观测马尔可夫决策过程中的复杂感知目标,提出sc-iLTL逻辑进行形式化描述,并通过信念MDP与自动机乘积结合蒙特卡洛树搜索实现概率收敛的最优策略综合,以无人机探测案例验证方法有效性。
2025-06-27 cs.AI cs.RO cs.SY
Optimal Controller and Quantizer Selection for Partially Observable Linear-Quadratic-Gaussian Systems
在网络化的控制系统中,传感信号通常在被传输到控制器之前被量化。因此,性能受到该量化过程的粗糙度的影响。现代通信技术允许用户根据所支付的价格获得分辨率变化的量化测量。在本文中,我们考虑联合最优控制器的合成和量化器调度的部分观测的量化反馈线性二次高斯(QF-LQG)系统,其中的测量被量化之前被发送到控制器。该系统提出了几种选择的量化器,以及使用每个量化器的成本。我们的目标是联合选择的量化器和综合的控制器,以达到控制性能和量化成本之间的最佳平衡。当量化的创新信号,而不是测量,该问题被解耦成两个优化问题:一个最优控制器的合成,和其他的最优量化器的选择。通过求解Riccati方程找到最优控制器,并且通过求解线性规划(LP)找到最优量化器选择策略,这两者都可以离线求解。
2021-11-08 cs.SY eess.SY math.OC
Constructive Safety-Critical Control: Synthesizing Control Barrier Functions for Partially Feedback Linearizable Systems
California Institute of Technology(加州理工学院)
本文建立部分反馈线性化与 CBF 综合的联系,证明输入-输出线性化系统可将输出安全约束扩展为全阶 CBF,并在四旋翼仿真与硬件中验证。
2024-06-04 cs.RO 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
Safe Control of Partially-Observed Linear Time-Varying Systems with Minimal Worst-Case Dynamic Regret
针对存在未知噪声的部分可观测线性时变系统,提出一种基于 System Level Synthesis 的最小最坏情况动态遗憾安全控制算法,在四旋翼轨迹跟踪仿真中展现出优于 $\mathcal{H}_2$ 和 $\mathcal{H}_\infty$ 控制器的性能。
2023-03-31 cs.SY eess.SY
Permissive Finite-State Controllers of POMDPs using Parameter Synthesis
RWTH Aachen University(亚琛工业大学);Radboud University(拉德堡德大学);Albert-Ludwigs-Universität Freiburg(弗赖堡大学)
研究了部分可观测马尔可夫决策过程中的宽容有限状态控制器,通过参数综合法实现正确性保证,实验表明性能与知名POMDP求解器相当。
2018-07-17 cs.LO cs.SY eess.SY
Correct-by-construction reach-avoid control of partially observable linear stochastic systems
University of Kentucky(肯塔基大学)
针对部分可观测线性随机系统,提出基于高斯信念MDP抽象的构造正确性控制器综合方法,可细化为分段线性反馈控制器,确保以所需概率满足到达-避免目标,并能处理高维状态空间及复杂输入约束。
2023-09-12 cs.AI cs.RO cs.SE
Secure Control in Partially Observable Environments to Satisfy LTL Specifications
本文研究了在部分可观察环境中,在对手存在的情况下,必须满足时序逻辑规范的智能体的控制策略的合成。代理(防御者)与对手的相互作用被建模为部分可观察的随机博弈。我们的目标是生成一个防御者的政策,以最大限度地满足给定的时间逻辑规范下的任何对手的政策。搜索策略仅限于有限状态控制器的空间,这导致了一个易于处理的方法来确定策略。我们的规范达到(子集)经常性状态的马尔可夫链的满意度。我们提出了一个算法来确定一组防守者和对手的有限状态控制器的固定大小,将满足时序逻辑规范,并证明它是健全的。然后,我们提出了一个值迭代算法,以最大限度地满足时间逻辑规范下的有限状态控制器的固定大小的概率。最后,我们将此设置扩展到防御者的有限状态控制器的大小可以增加以提高满意度概率的情况。我们用一个例子来说明我们的方法。
2020-11-05 cs.CR cs.GT cs.LO