• 人工智能 •

### 基于线性误差断言的推理方法

1. 1. 北京交通大学 计算机与信息技术学院, 北京 100044;
2. 中国科学院 成都计算机应用研究所, 成都 610041;
3. 广西大学 计算机与电子信息学院, 南宁 530004;
4. 广西民族大学 人工智能学院, 南宁 530006
• 收稿日期:2021-03-16 修回日期:2021-05-24 出版日期:2021-08-10 发布日期:2021-07-12
• 通讯作者: 吴尽昭
• 作者简介:武鹏(1981-),男,山西太原人,博士研究生,主要研究方向:形式化验证;吴尽昭(1965-),男,黑龙江齐齐哈尔人,教授,博士,主要研究方向:形式化方法、符号计算。
• 基金资助:
国家自然科学基金资助项目（61772006）。

### Reasoning method based on linear error assertion

WU Peng1, WU Jinzhao1,2,3,4

1. 1. School of Computer and Information Technology, Beijing Jiaotong University, Beijing 100044, China;
2. Chengdu Institute of Computer Application, Chinese Academy of Sciences, Chengdu Sichuan 610041, China;
3. School of Computer, Electronics and Information, Guangxi University, Nanning Guangxi 530004, China;
4. School of Artificial Intelligence, Guangxi University for Nationalities, Nanning Guangxi 530006, China
• Received:2021-03-16 Revised:2021-05-24 Online:2021-08-10 Published:2021-07-12
• Supported by:
This work is partially supported by the National Natural Science Foundation of China (61772006).

Abstract: Errors are common to the system. In safety-critical systems, quantitative analysis of errors is necessary. However, the previous reasoning and verification methods rarely consider errors. The errors are usually described with the interval numbers, so that the linear assertion was spread and the concept of linear error assertion was given. Furthermore, combined with the properties of convex set, a method to solve the vertices of linear error assertion was proposed, and the correctness of this method was proved. By analyzing the related concepts and theorems, the problem to judge whether there was implication relationship between linear error assertions was converted to the problem to judge whether the vertices of the precursor assertion were contained in the zero set of the successor assertion, so as to give the easy-to-program steps of judging the implication relationship between linear error assertions. Finally, the application of this method to train acceleration was given, and the correctness of the method was tested with the large-scale random examples. Compared with the reasoning methods without error semantics, this method has advantages in the field of reasoning and verification of systems with error parameters.