Efficient Dynamic Error Reduction for Hybrid Systems Reachability Analysis
Efficient Dynamic Error Reduction for Hybrid Systems Reachability Analysis
复制标题
混合系统可达性分析的高效动态误差减少
DOI：
10.1007/978-3-319-89963-3_17
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Erika Ábrahám
中科院分区：
文献类型：
--
作者：
Stefan Schupp;Erika Ábrahám
为了确定一组状态在混合系统中是否可达，可以使用过近似的符号后继计算，其中状态集的符号表示以及后继计算具有多个参数，这些参数决定了计算的效率和精度。当然，更快的计算伴随着更低的精度和更多的虚假反例。要删除虚假的反例，当前工具提供的唯一可能是通过使用不同的参数重新开始完整搜索来减少错误。在本文中，我们提出了一种CEGAR方法，该方法以用户定义的搜索配置的有序列表作为输入，用于沿着潜在的虚假反例动态地精化搜索树。专用数据结构允许从以前的计算中提取尽可能多的有用信息，以减少精化开销。
To decide whether a set of states is reachable in a hybrid system, over-approximative symbolic successor computations can be used, where the symbolic representation of state sets as well as the successor computations have several parameters which determine the efficiency and the precision of the computations. Naturally, faster computations come with less precision and more spurious counterexamples. To remove a spurious counterexample, the only possibility offered by current tools is to reduce the error by re-starting the complete search with different parameters. In this paper we propose a CEGAR approach that takes as input a user-defined ordered list of search configurations, which are used to dynamically refine the search tree along potentially spurious counterexamples. Dedicated datastructures allow to extract as much useful information as possible from previous computations in order to reduce the refinement overhead.
登录
查看更多内容
两种基于 CEGAR 的 PLC 控制工厂安全验证方法
影响因子：
5.9
作者：
J. Nellen;Kai Driessen;M. R. Neuhäußer;E. Ábrahám;Benedikt Wolters
通讯作者：
Benedikt Wolters
混合系统可达性分析的基准套件
DOI：
--
发表时间：
2015
期刊：
NASA Formal Methods
影响因子：
--
作者：
Xin Chen;Stefan Schupp;Ibtissem Ben Makhlouf;E. Ábrahám;Goran Frehse;S. Kowalewski
通讯作者：
S. Kowalewski
使用严格函数微积分计算混合系统的演化
DOI：
10.3182/20120606-3-nl-3011.00063
发表时间：
2012
期刊：
Acta endocrinologica
影响因子：
--
作者：
P. Collins;D. Bresolin;Luca Geretti;T. Villa
通讯作者：
T. Villa
工具介绍：Isabelle/HOL 用于连续系统的可达性分析
DOI：
10.29007/b3wr
发表时间：
2015
期刊：
影响因子：
--
作者：
Fabian Immler
通讯作者：
Fabian Immler
DOI：
10.1007/978-3-319-57288-8_20
发表时间：
2017-05
期刊：
--
影响因子：
--
作者：
Stefan Schupp;E. Ábrahám;Ibtissem Ben Makhlouf;S. Kowalewski
通讯作者：
Stefan Schupp;E. Ábrahám;Ibtissem Ben Makhlouf;S. Kowalewski