一种针对安全可达动态系统的形式化学习方法.pdf
《一种针对安全可达动态系统的形式化学习方法.pdf》由会员分享,可在线阅读,更多相关《一种针对安全可达动态系统的形式化学习方法.pdf(6页珍藏版)》请在咨信网上搜索。
1、书书书收稿日期:;修回日期:基金项目:国家自然科学基金资助项目()作者简介:鲁腾飞(),男,浙江湖州人,硕士研究生,主要研究方向为深度学习、形式化方法;娄攀登(),男,浙江杭州人,系统分析师,研究生企业导师,主要研究方向为软件分析与验证;王胜朴(),内蒙古满洲里人,硕士研究生,主要研究方向为系统可靠性研究和形式化方法;丁觅(),湖北咸宁人,硕士研究生,主要研究方向为形式化方法、软件分析与验证;林望(),男(通信作者),浙江温州人,副教授,硕导,博士,主要研究方向为形式化方法、软件分析与验证、信息物理融合系统()一种针对安全可达动态系统的形式化学习方法鲁腾飞,娄攀登,王胜朴,丁觅,林望(浙江理工
2、大学 计算机科学与技术学院,杭州 ;浙江唐彩智能信息科技有限公司,杭州 )摘要:在动态系统建模问题中,深度学习为建模提供了更便捷和灵活的方法,但其难以解释的特点降低了模型的可靠性。针对具有安全性和可达性的动态系统,提出了一种形式化模型学习方法,将安全性和可达性引入到对目标系统的学习过程中,使模型满足这两个性质。为保证所学系统在定义域上严格满足这两个性质,该方法基于现代控制理论中的 方法和 函数设计了可验证的 函数(),通过将其与动态系统联合学习,使得 能够为所学系统提供安全性和可达性保障。最后通过求解混合整数线性规划问题验证了模型确实满足相关性质,与 的对比实验展示了这一方法的有效性。关键词:
3、形式化方法;动态系统学习;安全性;可达性中图分类号:文献标志码:文章编号:():,(,;,):,(),:;引言信息物理系统广泛应用于工业控制、自动驾驶和航空航天等涉及社会运作和人身安全的关键基础设施,这类系统关乎人身、财产和环境安全,因此建立可靠的系统模型至关重要。在这一情形下,基于严格数学基础的形式化方法被应用于系统可靠性研究中 。如今深度学习方法为动态系统建模提供了新的途径,但其难以解释的特点导致模型的可靠性难以保证,比如在动态系统中常见的两种性质 安全性和可达性,在通过深度学习的方法对系统进行建模后这两个性质的证明变得十分困难。其中,安全性是指对于给定动态系统的初始状态,系统在随时间演化
4、的过程中不会进入不安全状态集;系统的可达性是指对于给定系统的初始状态,系统随着时间的推移总能进入目标状态集。由于 函数可以将系统的状态空间分割成两个子集,常被用来证明系统的安全性。理论是刻画动力系统稳定性的方法,求出系统的 函数可以保证系统的稳定性。这类函数能够为系统提供某些性质的保障,因此也被称为证书。为了在建模的同时保证系统的某些性质,诸多领域从不同的角度为此做了大量的研究工作,目前已存在许多针对不同种类系统的建模方法,但如何在学习动态系统的同时为模型提供安全性和可达性的保障仍是悬而未决的问题。比如文献 ,通过将系统投影到一个隐空间来保证系统的稳定性,在该隐空间中 函数严格满足定义,但是这
5、种方法给系统施加了过强的限制,牺牲了神经网络的灵活性,而且该方法没有考虑系统的安全性。等人 迭代地收集数据并更新系统的控制器,使用控制 函数以减少模型的不确定性,最终实现系统的安全行为,但是该方法没有考虑系统的可达性。最近,等人 在控制器合成任务中通过 ()使控制系统满足安全性和可达性,但是未对该控制器和系统进行验证,实际上该方法建立的系统在状态空间中有稀疏的状态点违背了安全性和可达性。目前,在动态系统的学习任务中,同时保证安全性和可达性的研究几乎处于空白状态。受到 等人 的启发,本文提出了一个基于数据驱动的学习方法 (),该方法通过联合学习非线性动态系统和 函数(),为系统的安全性和可达性提
6、供保障。既要满足安第 卷第 期 年 月计 算 机 应 用 研 究 全条件也要满足可达条件。但由于神经网络的引入导致模型具有不可解释性,这使得人们难以分析其行为。为了给系统的安全性和可达性提供一个形式化的保证,有必要验证所学的系统以及 。为此将系统和 的验证问题转换为混合整数线性规划(,)问题,并通过数值求解器 对该问题求解,以确保 的有效性。最后,将 和深度强化学习中常用的 方法进行对比,实验表明,对系统的长远预测准确度明显优于 方法,而且 有效地约束了神经网络形式的动态系统模型。本文主要贡献如下:)提出了一个学习框架,该框架同时考虑了系统的安全性和可达性,并且使用 作为系统具有安全性和可达性
7、的通用证书,而不是像多数研究将各个性质分开考虑,简化了证书的表达;)提出了一个验证框架,通过以 为激活函数的神经网络表示证书,并将神经网络的验证问题转换为 优化问题,使用优化求解器 编码和求解;)在一组基准样例中成功合成了 ,证明了算法框架的有效性。相关工作 动态系统建模不同场景下的动态系统各自具有不同特点,也不存在一种统一的方法能够为所有系统建立模型。线性系统相比其他系统更易于处理,因此如何学习稳定线性动态系统 ,较早地受到了关注,近来有更多学者着手研究稳定非线性系统的学习问题 。等人 较早地探索了深度学习和 分析的交叉点,文献 ,以联合学习方式学习动态系统和 函数,并且在学习过程中通过 函
8、数投影方法来限制系统的稳定性,其优点是无须验证即可保证所学系统的稳定性,但是对系统的限制可能过强,无法发挥出神经网络的灵活性。等人 提出的学习方法针对单调稳定系统,该方法认为系统的某一状态不仅依赖于上一个状态,之前的 个状态都对当前状态有贡献,因而训练了 个神经网络并将其输出取凸组合。等人 实现了一个名为 的工具,对给定了常微分方程()形式的动态系统,用反例制导的方法合成 和 函数,以证明系统的安全性和稳定性,反例由可满足性模理论()求解器解得。动态系统在数学上通常用微分方程表示,一些研究工作聚焦于如何建立系统的微分方程,该方法已广泛用于时间序列预测和常微分方程估计 ,。等人 提出了一类名为
9、的新型神经网络,该模型训练时间明显增加,但是空间复杂度为(),发表后被给予很高期望。等人 考虑到物理系统的部分行为通常可由微分方程或方程组给出,提出了一种将这些先验知识融入 的方法。基于 的方法现已被应用到概率分布变换 和图像识别 ,中,这些方法都非常新颖,但是关于这些系统具体性质的研究较少报道。等人 提出了另一种用于学习连续系统的方法,使用插值技术将离散轨迹连续化,在学习连续系统的同时求出 函数以保证系统的稳定性,该方法把吸引域作为先验信息引入学习过程。上述方法针对的系统各有特点,但考虑系统稳定性的研究较多,安全性和可达性相对较少被考虑到,后两个性质的研究主要集中在控制领域。要保证这些性质在
10、神经网络上成立,必须依赖形式化技术。形式化技术在学习控制任务中的应用基于严格数学基础的形式化方法已经被公认为验证系统是否具有安全性的有效方法,在工业领域中得到越来越广泛的应用 。在这一背景下,形式化方法被引入到深度学习领域以训练满足条件的神经网络。和 函数主要应用于控制领域,这类函数也被称为证书(),因为它们为控制器或系统的行为提供了某种保障。通过学习基于神经网络的 或 函数以及相应的控制策略,使系统满足相应性质,如 等人 用这种方法得到了安全和可达的控制器,但是没有进一步验证。等人 对问题做了简化,他们对给定的 函数求稳定控制器,但实际上 函数很难事先给出;等人 提出了安全控制器的合成方法,
11、其安全性由 函数保证,但是该方法针对连续系统,由于连续系统 函数定义与离散系统有所不同,验证方法也不一样。等人 采用神经网络表示标称控制器和 ,求得满足要求的 后,通过解一个特定的优化问题得到安全和稳定的控制器。这项工作受到 的启发,通过联合学习动态系统和对应的 保证了系统的安全性和可达性。通过深度学习方法合成 函数或 函数需要进一步验证,这涉及到神经网络的可信性分析 。为解决这一问题,、输入精化()、线性逼近 、等方法被引入到神经网络的形式化验证中。等人 用 评估神经网络的鲁棒性;后来 等人 用这一技术验证屏障证书,其原理是将 函数替换为一系列线性约束和二值约束,从而用 计算神经网络在给定输
12、入区域上的最大或最小输出。文献 处理的系统是连续的,而在本项工作中合成的是离散系统,验证过程中的编码方式有较大差异。基础知识 动态系统及其性质原系统的具体数学形式往往是不可知的,主要考虑通过深度学习建立离散动态系统模型,训练数据是从初始区域出发的状态序列。首先,引入离散动态系统的差分方程表示方法:()()()其中:?表示时间,?表示系统状态,():表示定义在?上的 连续函数。同时系统还需要满足可达性和安全性。定义 可达性。给定紧集?和紧集?,如果对于任意初始状态?,都存在?,使得?,则称该系统是可达的,分别称?和?为初始集和目标集。定义 安全性。给定紧集?和紧集?,且?,如果对于任意?和任意?
13、都有?,则称该系统是安全的,分别称?和?为初始集和不安全集。综合考虑这两个性质,即系统状态从初始区域?出发,存在有限时间?,经过 步后系统状态必能进入目标区域?,而且这期间不会进入不安全区域?。形式上,将从 出发,经过 步演化后形成的状态序列记为,简记为 :。对目标区域的可达性可由稳定性扩展得到 ,通过证明动态系统存在一个与之匹配的 函数以确保系统具有可达性,而系统的安全性则是通过找到系统的 函数来保证,这两个函数的使用和推广在控制领域已经得到广泛研究和应用 。基于这两个函数,以保证所学动态系统的安全性和可达性。定义 函数。若有函数 :?,:,使得下述条件:()?()()?()()?()计 算
14、 机 应 用 研 究 第 卷()?()()()?()成立,则称 为离散动态系统 的 函数。如果上述 存在,则系统是安全且可达的,因为 确定的水平集?是该系统的一个前向不变集,初始区域被包含在该不变集中,而不安全区域与该不变集没有交集,从而使得从?出发的任意轨迹都不可能进入?。类似地,由 确定的水平集?也是该系统的一个前向不变集,该不变集正是目标区域?,从状态空间中任意状态出发的轨迹随系统演化必将进入?,并且在无限时间内都不会离开?。基于以上理论,如果能够在学习系统的同时学习相应的 ,则最终学到的系统将具有安全性和可达性保障。但是仅通过神经网络学习动态系统及其 仍然不够,因为由神经网络表示的 本
15、身就缺乏可解释性,所以必须对网络进行验证。为便于后续验证过程的描述,下面给出神经网络的形式化表示方法。神经网络验证方法用 表示神经网络 的输入,和 表示第 个隐藏层的输出和激活函数,和 分别表示第 个隐藏层的系数和偏置,表示的网络的最后输出,则神经网络的运算过程 ()可以形式化地描述为 (),()为了便于验证系统 及其 ,使用 作为激活函数,基于 的神经网络的验证问题可以转换为 问题。关于神经网络输出求最大或最小值的问题,涉及到将网络的前向传播过程转换为 问题的约束 ,记为 (,),其具体形式如下:,(),()()其中:()表示第 个隐藏层的输入 的维度;向量 维度与 相同,其每个元素都是属于
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- 一种 针对 安全 动态 系统 形式化 学习方法
1、咨信平台为文档C2C交易模式,即用户上传的文档直接被用户下载,收益归上传人(含作者)所有;本站仅是提供信息存储空间和展示预览,仅对用户上传内容的表现方式做保护处理,对上载内容不做任何修改或编辑。所展示的作品文档包括内容和图片全部来源于网络用户和作者上传投稿,我们不确定上传用户享有完全著作权,根据《信息网络传播权保护条例》,如果侵犯了您的版权、权益或隐私,请联系我们,核实后会尽快下架及时删除,并可随时和客服了解处理情况,尊重保护知识产权我们共同努力。
2、文档的总页数、文档格式和文档大小以系统显示为准(内容中显示的页数不一定正确),网站客服只以系统显示的页数、文件格式、文档大小作为仲裁依据,平台无法对文档的真实性、完整性、权威性、准确性、专业性及其观点立场做任何保证或承诺,下载前须认真查看,确认无误后再购买,务必慎重购买;若有违法违纪将进行移交司法处理,若涉侵权平台将进行基本处罚并下架。
3、本站所有内容均由用户上传,付费前请自行鉴别,如您付费,意味着您已接受本站规则且自行承担风险,本站不进行额外附加服务,虚拟产品一经售出概不退款(未进行购买下载可退充值款),文档一经付费(服务费)、不意味着购买了该文档的版权,仅供个人/单位学习、研究之用,不得用于商业用途,未经授权,严禁复制、发行、汇编、翻译或者网络传播等,侵权必究。
4、如你看到网页展示的文档有www.zixin.com.cn水印,是因预览和防盗链等技术需要对页面进行转换压缩成图而已,我们并不对上传的文档进行任何编辑或修改,文档下载后都不会有水印标识(原文档上传前个别存留的除外),下载后原文更清晰;试题试卷类文档,如果标题没有明确说明有答案则都视为没有答案,请知晓;PPT和DOC文档可被视为“模板”,允许上传人保留章节、目录结构的情况下删减部份的内容;PDF文档不管是原文档转换或图片扫描而得,本站不作要求视为允许,下载前自行私信或留言给上传者【自信****多点】。
5、本文档所展示的图片、画像、字体、音乐的版权可能需版权方额外授权,请谨慎使用;网站提供的党政主题相关内容(国旗、国徽、党徽--等)目的在于配合国家政策宣传,仅限个人学习分享使用,禁止用于任何广告和商用目的。
6、文档遇到问题,请及时私信或留言给本站上传会员【自信****多点】,需本站解决可联系【 微信客服】、【 QQ客服】,若有其他问题请点击或扫码反馈【 服务填表】;文档侵犯商业秘密、侵犯著作权、侵犯人身权等,请点击“【 版权申诉】”(推荐),意见反馈和侵权处理邮箱:1219186828@qq.com;也可以拔打客服电话:4008-655-100;投诉/维权电话:4009-655-100。