Reasoning Method between Polynomial Error Assertions
Open Access
- 30 July 2021
- journal article
- research article
- Published by MDPI AG in Information
- Vol. 12 (8), 309
- https://doi.org/10.3390/info12080309
Abstract
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.Keywords
Funding Information
- National Natural Science Foundation of China (61772006)
This publication has 14 references indexed in Scilit:
- A Formal Verification Framework for Security Issues of Blockchain Smart ContractsElectronics, 2020
- Analytical and triangular solutions to operational flexibility analysis using quantifier eliminationAIChE Journal, 2018
- Hybrid Control Scheme Consisting of Adaptive and Optimal Controllers for Flexible-Base Flexible-Joint Space Manipulator with Uncertain ParametersPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2017
- Uncertain multi-attributes decision making method based on interval number with probability distribution weighted operators and stochastic dominance degreeKnowledge-Based Systems, 2016
- Limited Rationality and Its Quantification Through the Interval Number Judgments With PermutationsIEEE Transactions on Cybernetics, 2016
- A Deductive Approach towards Reasoning about Algebraic Transition SystemsMathematical Problems in Engineering, 2015
- A Survey of Automated Techniques for Formal Software VerificationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2008
- DISCOVERERACM Communications in Computer Algebra, 2007
- 22 Labelled Transition SystemsLecture Notes in Computer Science, 2005
- Cylindrical Algebraic Decomposition I: The Basic AlgorithmSIAM Journal on Computing, 1984