Reasoning Method between Polynomial Error Assertions
Error coefficients are ubiquitous in systems. In particular, errors in reasoning verification must be considered regarding safety-critical systems. We present a reasoning method that can be applied to systems described by the polynomial error assertion (PEA). The implication relationship between PEA...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
MDPI AG
2021-07-01
|
| Series: | Information |
| Subjects: | |
| Online Access: | https://www.mdpi.com/2078-2489/12/8/309 |
| _version_ | 1797523535160147968 |
|---|---|
| author | Peng Wu Ning Xiong Juxia Xiong Jinzhao Wu |
| author_facet | Peng Wu Ning Xiong Juxia Xiong Jinzhao Wu |
| author_sort | Peng Wu |
| collection | DOAJ |
| description | Error coefficients are ubiquitous in systems. In particular, errors in reasoning verification must be considered regarding safety-critical systems. We present a reasoning method that can be applied to systems described by the polynomial error assertion (PEA). The implication relationship between PEAs can be converted to an inclusion relationship between zero sets of PEAs; the PEAs are then transformed into first-order polynomial logic. Combined with the quantifier elimination method, based on cylindrical algebraic decomposition, the judgment of the inclusion relationship between zero sets of PEAs is transformed into judgment error parameters and specific error coefficient constraints, which can be obtained by the quantifier elimination method. The proposed reasoning method is validated by proving the related theorems. An example of intercepting target objects is provided, and the correctness of our method is tested through large-scale random cases. Compared with reasoning methods without error semantics, our reasoning method has the advantage of being able to deal with error parameters. |
| first_indexed | 2024-03-10T08:44:22Z |
| format | Article |
| id | doaj.art-e913d0586490495ea9cc0efe5183dc55 |
| institution | Directory Open Access Journal |
| issn | 2078-2489 |
| language | English |
| last_indexed | 2024-03-10T08:44:22Z |
| publishDate | 2021-07-01 |
| publisher | MDPI AG |
| record_format | Article |
| series | Information |
| spelling | doaj.art-e913d0586490495ea9cc0efe5183dc552023-11-22T08:05:55ZengMDPI AGInformation2078-24892021-07-0112830910.3390/info12080309Reasoning Method between Polynomial Error AssertionsPeng Wu0Ning Xiong1Juxia Xiong2Jinzhao Wu3School of Computer and Information Technology, Beijing Jiaotong University, Beijing 100044, ChinaSchool of Innovation, Design and Engineering, Mälardalen University, 72123 Västerås, SwedenSchool of Mathematics and Physics, Guangxi University for Nationalities, Nanning 530006, ChinaSchool of Computer and Information Technology, Beijing Jiaotong University, Beijing 100044, ChinaError coefficients are ubiquitous in systems. In particular, errors in reasoning verification must be considered regarding safety-critical systems. We present a reasoning method that can be applied to systems described by the polynomial error assertion (PEA). The implication relationship between PEAs can be converted to an inclusion relationship between zero sets of PEAs; the PEAs are then transformed into first-order polynomial logic. Combined with the quantifier elimination method, based on cylindrical algebraic decomposition, the judgment of the inclusion relationship between zero sets of PEAs is transformed into judgment error parameters and specific error coefficient constraints, which can be obtained by the quantifier elimination method. The proposed reasoning method is validated by proving the related theorems. An example of intercepting target objects is provided, and the correctness of our method is tested through large-scale random cases. Compared with reasoning methods without error semantics, our reasoning method has the advantage of being able to deal with error parameters.https://www.mdpi.com/2078-2489/12/8/309formal methodreasoning methodsystem verificationpolynomialerror control |
| spellingShingle | Peng Wu Ning Xiong Juxia Xiong Jinzhao Wu Reasoning Method between Polynomial Error Assertions Information formal method reasoning method system verification polynomial error control |
| title | Reasoning Method between Polynomial Error Assertions |
| title_full | Reasoning Method between Polynomial Error Assertions |
| title_fullStr | Reasoning Method between Polynomial Error Assertions |
| title_full_unstemmed | Reasoning Method between Polynomial Error Assertions |
| title_short | Reasoning Method between Polynomial Error Assertions |
| title_sort | reasoning method between polynomial error assertions |
| topic | formal method reasoning method system verification polynomial error control |
| url | https://www.mdpi.com/2078-2489/12/8/309 |
| work_keys_str_mv | AT pengwu reasoningmethodbetweenpolynomialerrorassertions AT ningxiong reasoningmethodbetweenpolynomialerrorassertions AT juxiaxiong reasoningmethodbetweenpolynomialerrorassertions AT jinzhaowu reasoningmethodbetweenpolynomialerrorassertions |