• 文献检索
  • 文档翻译
  • 深度研究
  • 学术资讯
  • Suppr Zotero 插件Zotero 插件
  • 邀请有礼
  • 套餐&价格
  • 历史记录
应用&插件
Suppr Zotero 插件Zotero 插件浏览器插件Mac 客户端Windows 客户端微信小程序
定价
高级版会员购买积分包购买API积分包
服务
文献检索文档翻译深度研究API 文档MCP 服务
关于我们
关于 Suppr公司介绍联系我们用户协议隐私条款
关注我们

Suppr 超能文献

核心技术专利：CN118964589B侵权必究
粤ICP备2023148730 号-1Suppr @ 2026

文献检索

告别复杂PubMed语法，用中文像聊天一样搜索，搜遍4000万医学文献。AI智能推荐，让科研检索更轻松。

立即免费搜索

文件翻译

保留排版，准确专业，支持PDF/Word/PPT等文件格式，支持 12+语言互译。

免费翻译文档

深度研究

AI帮你快速写综述，25分钟生成高质量综述，智能提取关键信息，辅助科研写作。

立即免费体验

通过抽象加速对带输入的受保护线性时不变模型进行无界时间安全验证。

Unbounded-Time Safety Verification of Guarded LTI Models with Inputs by Abstract Acceleration.

作者信息

Cattaruzza Dario, Abate Alessandro, Schrammel Peter, Kroening Daniel

机构信息

Department of Computer Science, University of Oxford, Oxford, UK.

School of Engineering and Informatics, University of Sussex, Brighton, UK.

出版信息

J Autom Reason. 2021;65(2):157-203. doi: 10.1007/s10817-020-09562-z. Epub 2020 May 29.

DOI:10.1007/s10817-020-09562-z
PMID:33678930
原文链接:https://pmc.ncbi.nlm.nih.gov/articles/PMC7900086/
Abstract

Reachability analysis of dynamical models is a relevant problem that has seen much progress in the last decades, however with clear limitations pertaining to the nature of the dynamics and the soundness of the results. This article focuses on sound safety verification of unbounded-time (infinite-horizon) linear time-invariant (LTI) models with inputs using reachability analysis. We achieve this using counterexample-guided Abstract Acceleration: this approach over-approximates the reachability tube of the LTI model over an unbounded time horizon by using abstraction, possibly finding concrete counterexamples for refinement based on the given safety specification. The technique is applied to a number of LTI models and the results show robust performance when compared to state-of-the-art tools.

摘要

动态模型的可达性分析是一个相关问题，在过去几十年中取得了很大进展，然而在动力学性质和结果的可靠性方面存在明显局限性。本文重点使用可达性分析对具有输入的无界时间（无限时域）线性时不变（LTI）模型进行可靠的安全性验证。我们通过反例引导的抽象加速来实现这一点：该方法通过使用抽象来过度近似LTI模型在无界时间范围内的可达性管，可能会根据给定的安全规范找到具体的反例用于细化。该技术应用于多个LTI模型，结果表明与现有工具相比具有强大的性能。

https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/5b88daa74205/10817_2020_9562_Fig13_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/1fd3eeda8f47/10817_2020_9562_Fig1_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/78b88fdecc9e/10817_2020_9562_Fig2_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/7c16779b2fbe/10817_2020_9562_Fig3_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/31e854bb9f33/10817_2020_9562_Fig4_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/7115d1aac600/10817_2020_9562_Fig5_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/ab2aef28b01c/10817_2020_9562_Fig6_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/994c2ea4def5/10817_2020_9562_Fig7_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/71525e23c6f8/10817_2020_9562_Fig8_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/5a57c6f72a7b/10817_2020_9562_Fig9_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/3b6307600ada/10817_2020_9562_Fig10_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/72d72b14cb35/10817_2020_9562_Fig11_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/4d686f24bdc5/10817_2020_9562_Fig12_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/5b88daa74205/10817_2020_9562_Fig13_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/1fd3eeda8f47/10817_2020_9562_Fig1_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/78b88fdecc9e/10817_2020_9562_Fig2_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/7c16779b2fbe/10817_2020_9562_Fig3_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/31e854bb9f33/10817_2020_9562_Fig4_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/7115d1aac600/10817_2020_9562_Fig5_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/ab2aef28b01c/10817_2020_9562_Fig6_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/994c2ea4def5/10817_2020_9562_Fig7_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/71525e23c6f8/10817_2020_9562_Fig8_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/5a57c6f72a7b/10817_2020_9562_Fig9_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/3b6307600ada/10817_2020_9562_Fig10_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/72d72b14cb35/10817_2020_9562_Fig11_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/4d686f24bdc5/10817_2020_9562_Fig12_HTML.jpg
https://cdn.ncbi.nlm.nih.gov/pmc/blobs/6617/7900086/5b88daa74205/10817_2020_9562_Fig13_HTML.jpg

相似文献

1
Unbounded-Time Safety Verification of Guarded LTI Models with Inputs by Abstract Acceleration.通过抽象加速对带输入的受保护线性时不变模型进行无界时间安全验证。
J Autom Reason. 2021;65(2):157-203. doi: 10.1007/s10817-020-09562-z. Epub 2020 May 29.
2
Para : parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms.段落：用于阈值保护分布式算法可达性的参数化路径约简、加速和SMT（满足性模态理论）
Form Methods Syst Des. 2017;51(2):270-307. doi: 10.1007/s10703-017-0297-4. Epub 2017 Sep 20.
3
Reachability analysis of real-time systems using time Petri nets.使用时间Petri网的实时系统可达性分析
IEEE Trans Syst Man Cybern B Cybern. 2000;30(5):725-36. doi: 10.1109/3477.875448.
4
Comments on "A modified reachability tree approach to analysis of unbounded Petri nets".关于《一种用于无界Petri网分析的改进可达性树方法》的评论
IEEE Trans Syst Man Cybern B Cybern. 2006 Oct;36(5):1210. doi: 10.1109/tcsi.2006.876811.
5
INNAbstract: An INN-Based Abstraction Method for Large-Scale Neural Network Verification.基于国际非专利药品名称的大规模神经网络验证抽象方法摘要
IEEE Trans Neural Netw Learn Syst. 2024 Dec;35(12):18455-18469. doi: 10.1109/TNNLS.2023.3316551. Epub 2024 Dec 2.
6
Under-approximating loops in C programs for fast counterexample detection.用于快速反例检测的C程序中的欠近似循环。
Form Methods Syst Des. 2015;47:75-92. doi: 10.1007/s10703-015-0228-1. Epub 2015 Apr 17.
7
An input-output linear time invariant model captures neuronal firing responses to external and behavioral events.一个输入-输出线性时不变模型可捕捉神经元对外部和行为事件的放电反应。
Annu Int Conf IEEE Eng Med Biol Soc. 2017 Jul;2017:970-973. doi: 10.1109/EMBC.2017.8036987.
8
A modified reachability tree approach to analysis of unbounded Petri nets.一种用于无界Petri网分析的改进可达性树方法。
IEEE Trans Syst Man Cybern B Cybern. 2004 Feb;34(1):303-8. doi: 10.1109/tsmcb.2003.811516.
9
Reachability Analysis of Cyber-Physical Systems Under Stealthy Attacks.隐蔽攻击下信息物理系统的可达性分析
IEEE Trans Cybern. 2022 Jun;52(6):4926-4934. doi: 10.1109/TCYB.2020.3025307. Epub 2022 Jun 16.
10
Automated formal synthesis of provably safe digital controllers for continuous plants.用于连续工厂的可证明安全数字控制器的自动化形式合成。
Acta Inform. 2020;57(1):223-244. doi: 10.1007/s00236-019-00359-1. Epub 2019 Dec 6.