实时模型检测精确加速窗口的计算原理及算法

王国卿; 庄雷; 和孟佯; 宋玉; 马岭

doi:10.7544/issn1000-1239.2020.20190052

实时模型检测精确加速窗口的计算原理及算法

(郑州大学信息工程学院郑州 450001) (iegqwang@163.com)

基金项目: 国家自然科学基金重点项目(U1604262)；河南省高等学校重点科研项目(19A520003,17A520057)；河南省科技攻关计划项目(172102210478)

详细信息

中图分类号: TP301.1
计量
- 文章访问数: 900
- HTML全文浏览量: 0
- PDF下载量: 230
出版历程
- 发布日期: 2019-12-31

Calculation Principle and Algorithm for the Window of Exact Acceleration in Real-Time Model Checking

(School of Information Engineering, Zhengzhou University, Zhengzhou 450001)

Funds: This work was supported by the Key Program of the National Natural Science Foundation of China (U1604262), the Key Scientific Research Project of Higher Education of Henan (19A520003, 17A520057), and the Science and Technology Key Project of Henan (172102210478).

摘要

摘要: 时间自动机为实时系统进行建模时，通常会因不同的时间度量而产生大量状态片段，精确加速技术可以有效解决这一类片段问题.精确加速中的关键技术是可加速环窗口的计算，但其计算方法均为人工推演.通过对精确加速计算原理的分析，提出了一种精确加速中可加速环窗口的计算算法，可以选择环中任意入边有环时钟复位的节点作为起始，对识别出的可加速环进行进一步精准压缩.首先，识别出时间自动机中所有可加速环，选取1个未处理的可加速环检测环时钟复位的节点出边是否有环时钟复位；然后，将所记录的节点按照记录顺序连接成1个新环，并重新计算新环各边的边界约束；最后，计算可加速环的窗口.算法根据窗口计算原理，获取影响窗口大小的位置不变式、边界约束、时钟复位等数据，并对无用数据和节点进行约减，压缩了可加速环规模，提高了计算效率.算法为研发精确加速自动检测程序奠定了基础.
- 模型检测 /
- 时间自动机 /
- 精确加速 /
- 可加速环 /
- 窗口
Abstract: When real-time systems are modeled as timed automata, different time scales may lead to a lot of fragmentations of the symbolic state space. This problem can be solved by computing the zones which in practice use the abstraction technique. The state-of-the-art abstraction methods produce an approximation that is closer to the actual reachable clock valuation, which are coarser abstractions. The exact acceleration is a finer abstraction way to reduce the required storage space and it can solve or alleviate the state space explosion problem of the fragmentations. Calculating the acceleratable cycle’s window is the key technology in exact acceleration. The calculation of the window in acceleratable cycle depends on the location invariant, edge constraint and clock reset. By comprehensively analyzing the exact acceleration principle, an algorithm is proposed to calculate the window in exact acceleration. Firstly, it is important to identify all acceleratable cycles in time automaton. Choose one node with clock reset on incoming edge as the start and check whether there is a clock reset on outgoing edge for every nodes. Secondly, all the recorded nodes link as a new cycle according to the recording ordering. Each node in new cycle has the original location invariant and each edge contains clock reset. In addition, edge constraints need to calculate. Finally, the window of acceleratable cycle can denote an interval ［a,b］, where a means the sum of edge constraints and b means the sum of location invariants. The time complexity of the algorithm is O(n\+2). According to the calculation principle, the algorithm can get the valid data of the window, reduce other useless data and nodes, compress the acceleratable cycle, make the model simpler and enhance the computing efficiency. The algorithm lays the foundation for the research and development of the automatic model checking program.
- model checking /
- timed automata /
- exact acceleration /
- acceleratable cycle /
- window

HTML全文

参考文献(0)

施引文献(145)

期刊类型引用(48)

1.	范如国，吴婷. 考虑多重异质性的区域环境合作治理小世界网络演化博弈研究. 管理工程学报. 2025(01): 140-154 . 百度学术
2.	师庆科，李楠，叶枫. 机器学习在临床研究中的应用进展. 中国数字医学. 2025(03): 1-10 . 百度学术
3.	窦慧，张凌茗，韩峰，申富饶，赵健. 卷积神经网络的可解释性研究综述. 软件学报. 2024(01): 159-184 . 百度学术
4.	孙书魁，范菁，孙中强，曲金帅，代婷婷. 基于深度学习的图像数据增强研究综述. 计算机科学. 2024(01): 150-167 . 百度学术
5.	练志润，张家蔚，杨保林. 基于规则生成医案及Transformer算法构建中医方药推荐模型. 中国中医基础医学杂志. 2024(03): 437-442 . 百度学术
6.	廖才波，杨金鑫，邱志斌，胡雄，曾清霖，黄智勇. 一种基于夏普利值及油中溶解气体分析的可解释变压器故障诊断方法. 电网技术. 2024(04): 1752-1762 . 百度学术
7.	陈彩华，佘程熙，王庆阳. 可信机器学习综述. 工业工程. 2024(02): 14-26 . 百度学术
8.	闵继源，鲁统宇，任婷婷，陈汝昊. 基于规则集成的可解释机器学习算法及应用. 计算机科学与探索. 2024(06): 1476-1490 . 百度学术
9.	王贝伦，张嘉琦，蔡英豪，王兆阳，谈笑，沈典. 面向信息系统推荐与决策的高阶张量分析方法. 计算机研究与发展. 2024(07): 1697-1712 . 本站查看
10.	申采玉，王帅，周锐盈，汪雨贺，高琴，陈兴智，杨枢. 慢性心力衰竭合并肺部感染患者院内死亡风险预测：基于可解释性机器学习方法. 南方医科大学学报. 2024(06): 1141-1148 . 百度学术
11.	李志宏，蔡迎彬，王岩，樊华，伊丽米奴尔·阿合买，李紫梅. 基于机器学习算法预测早期结直肠腺癌病人内镜治疗后的癌症特异性生存状态. 护理研究. 2024(14): 2459-2467 . 百度学术
12.	许志伟，李海龙，李博，李涛，王嘉泰，谢学说，董泽辉. AIGC大模型测评综述：使能技术、安全隐患和应对. 计算机科学与探索. 2024(09): 2293-2325 . 百度学术
13.	魏光普，于晓燕，高耀辉，马明，马斌，董铁鑫. 省级一流风景园林规划设计虚拟仿真实验课程设计与用后评价研究——以内蒙古科技大学为例. 高教学刊. 2024(27): 25-28 . 百度学术
14.	王越，李勇，张文静. 面向可解释性的软件缺陷预测主动学习方法. 现代电子技术. 2024(20): 101-108 . 百度学术
15.	李二超，刘辰淼. Pareto解集旋转的分类多策略预测动态多目标优化. 计算机工程与应用. 2024(22): 87-104 . 百度学术
16.	龙享福，李少波，张仪宗，杨磊，李传江. 因果学习方法和应用概述. 计算机工程与应用. 2024(24): 1-19 . 百度学术
17.	赵方煜. 智能要素式审判的运行障碍与优化路径. 武汉交通职业学院学报. 2024(04): 40-46 . 百度学术
18.	杨朋波，桑基韬，张彪，冯耀功，于剑. 面向图像分类的深度模型可解释性研究综述. 软件学报. 2023(01): 230-254 . 百度学术
19.	李家宁，熊睿彬，兰艳艳，庞亮，郭嘉丰，程学旗. 因果机器学习的前沿进展综述. 计算机研究与发展. 2023(01): 59-84 . 本站查看
20.	姚帅君，闫敬来，杜彩凤，杨继红. 基于集成学习构建围绝经期综合征中医智能诊断模型. 中医杂志. 2023(06): 572-580 . 百度学术
21.	尤振飞，位一鸣，俞兴伟，宣科，邬凌云，王爱玉，张悦. 基于语义分割与证据理论的电杆倾斜检测及风险评估方法. 浙江电力. 2023(04): 79-87 . 百度学术
22.	赖界亨，卢洵，王克英，邱显欣，潘振宁. 基于广义加性模型的调温负荷测算方法. 广东电力. 2023(06): 40-49 . 百度学术
23.	刘泽润，刘超. 可持续建成环境研究的机器学习应用进展与展望. 风景园林. 2023(07): 51-59 . 百度学术
24.	向许，于洪，张晓霞，王国胤. IsomapVSG-LIME：一种新的模型无关解释方法. 智能系统学报. 2023(04): 841-848 . 百度学术
25.	徐鹤，郑群力，谢作玲，程海涛，李鹏，季一木. 基于知识表示向量的可解释深度学习模型及其疾病预测应用. 数据采集与处理. 2023(04): 777-791 . 百度学术
26.	龚善要. 人工智能司法应用的实践审思与完善. 国家检察官学院学报. 2023(05): 95-108 . 百度学术
27.	金东镇，郭城楠，彭芳，赵淑珍，李慧慧，夏喆铮，车明珠，王亚楠，张泽杰，毛广运. 从SHAP到概率——可解释性机器学习在糖尿病视网膜病变靶向脂质组学研究中的应用. 中国卫生统计. 2023(04): 511-515 . 百度学术
28.	邹琼，张杨，万毅，陈长生. 糖尿病相关预测模型构建的机器学习方法. 中国卫生统计. 2023(04): 631-635+640 . 百度学术
29.	韩富佳，王晓辉，乔骥，史梦洁，蒲天骄. 基于人工智能技术的新型电力系统负荷预测研究综述. 中国电机工程学报. 2023(22): 8569-8592 . 百度学术
30.	吕亚兰，徐媛媛，张恒汝. 一种可解释性泛化矩阵分解推荐算法. 南京大学学报(自然科学). 2022(01): 135-142 . 百度学术
31.	胡安宁. 以文本为基础的社会科学研究：从内容分析到算法模型. 学术论坛. 2022(01): 1-8 . 百度学术
32.	古天龙，李龙，常亮，罗义琴. 公平机器学习:概念、分析与设计. 计算机学报. 2022(05): 1018-1051 . 百度学术
33.	罗杨洋，韩锡斌. 混合课程学生成绩预测模型的可解释性探究. 中国远程教育. 2022(06): 46-55 . 百度学术
34.	符冉迪，司光，金炜. 深度网络与FSVM集成学习的卫星云图云分类. 光学精密工程. 2022(08): 917-927 . 百度学术
35.	李慧，焦雄. 基于影像组学的乳腺钼靶图像分类模型研究. 太原理工大学学报. 2022(04): 728-735 . 百度学术
36.	古天龙，郝峰锐，李龙，李晶晶，常亮. 社交网络中负责隐私协商的智能体行为追责. 软件学报. 2022(09): 3453-3469 . 百度学术
37.	袁高腾，周晓峰，郭宏乐. 基于特征选择算法的ECG信号分类. 山东大学学报(工学版). 2022(04): 38-44 . 百度学术
38.	姜婷婷，傅诗婷. 人本视角下的数字记忆：“人—记忆—技术”三位一体理论框架构建与启示. 中国图书馆学报. 2022(05): 103-115 . 百度学术
39.	李凌敏，侯梦然，陈琨，刘军民. 深度学习的可解释性研究综述. 计算机应用. 2022(12): 3639-3650 . 百度学术
40.	魏佳，蒋理，穆原，徐建. 机器学习在检验医学中的应用进展与挑战. 中华检验医学杂志. 2022(12): 1288-1292 . 百度学术
41.	辛瑞昊，董哲原，苗冯博，王甜甜，李英瑞，冯欣. 基于机器学习的心脏病预测模型研究. 吉林化工学院学报. 2022(09): 27-32 . 百度学术
42.	白林亭，海钰琳. 基于梯度分析的卷积神经网络可视化方法. 信息技术与信息化. 2021(04): 61-63 . 百度学术
43.	陈洞天，单杰，周文丹. 基于Xgboost的心血管疾病预测模型和指标分析研究. 现代医院. 2021(06): 958-961 . 百度学术
44.	王锦. 基于弹性BP算法的手写数字识别. 新乡学院学报. 2021(06): 24-27 . 百度学术
45.	戴宏，盛立杰，苗启广. 基于胶囊网络的对抗判别域适应算法. 计算机研究与发展. 2021(09): 1997-2012 . 本站查看
46.	杜静湄，廖思阳，徐箭. 基于动态迭代排序的电网项目投资决策方法. 武汉大学学报(工学版). 2021(10): 942-951 . 百度学术
47.	孙建文，周建鹏，刘三女牙，何绯娟，唐云. 基于多层注意力网络的可解释认知追踪方法. 计算机研究与发展. 2021(12): 2630-2644 . 本站查看
48.	徐良辰，郭崇慧. 智慧医院建设背景下的电子病历分析利用框架. 大数据. 2021(04): 141-156 . 百度学术