{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T16:42:27Z","timestamp":1740156147173,"version":"3.37.3"},"reference-count":33,"publisher":"MDPI AG","issue":"1","license":[{"start":{"date-parts":[[2021,12,25]],"date-time":"2021-12-25T00:00:00Z","timestamp":1640390400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61772006"],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"name":"the Special Fund for Bagui Scholars of Guangx","award":["2017"]},{"name":"the Science and Technology Major Project of Guangxi","award":["AA 17204096"]},{"name":"the key research and development project of Guangxi","award":["AB17129012"]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Symmetry"],"abstract":"Error parameters are inevitable in systems. In formal verification, previous reasoning methods seldom considered the probability information of errors. In this article, errors are described as symmetric truncated normal intervals consisting of the intervals and symmetric truncated normal probability density. Furthermore, we also rigorously prove lemmas and a theorem to partially simplify the calculation process of truncated normal intervals and independently verify the formulas of variance and expectation of symmetric truncated interval given by some scholars. The mathematical derivation process or verification codes are provided for most of the key formulas in this article. Hence, we propose a new reasoning method that combines the probability information of errors with the previous statistical reasoning methods. Finally, an engineering example of the reasoning verification of train acceleration is provided. After simulating the large-scale cases, it is shown that the simulation results are consistent with the theoretical reasoning results. This method needs more calculation, while it is more effective in detecting non-error\u2019s fault factors than other error reasoning methods.<\/jats:p>","DOI":"10.3390\/sym14010025","type":"journal-article","created":{"date-parts":[[2021,12,27]],"date-time":"2021-12-27T06:03:37Z","timestamp":1640585017000},"page":"25","source":"Crossref","is-referenced-by-count":0,"title":["Reasoning Method Based on Intervals with Symmetric Truncated Normal Density"],"prefix":"10.3390","volume":"14","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4784-8984","authenticated-orcid":false,"given":"Peng","family":"Wu","sequence":"first","affiliation":[{"name":"School of Computer and Information Technology, Beijing Jiaotong University, Beijing 100044, China"}]},{"given":"Zhenjie","family":"Hou","sequence":"additional","affiliation":[{"name":"School of Computer and Artificial Intelligence, Changzhou University, Changzhou 213164, China"}]},{"given":"Jiqiang","family":"Liu","sequence":"additional","affiliation":[{"name":"School of Computer and Information Technology, Beijing Jiaotong University, Beijing 100044, China"}]},{"given":"Jinzhao","family":"Wu","sequence":"additional","affiliation":[{"name":"School of Computer and Information Technology, Beijing Jiaotong University, Beijing 100044, China"},{"name":"School of Mathematics and Physics, Guangxi University for Nationalities, Nanning 530006, China"},{"name":"School of Computer, Electronics and Information, Guangxi University, Nanning 530004, China"}]}],"member":"1968","published-online":{"date-parts":[[2021,12,25]]},"reference":[{"key":"ref_1","doi-asserted-by":"crossref","unstructured":"Fisher, M., Cardoso, R.C., Collins, E.C., Dadswell, C., Dennis, L.A., Dixon, C., Farrell, M., Ferrando, A., Huang, X., and Jump, M. (2021). An Overview of Verification and Validation Challenges for Inspection Robots. Robotics, 10.","DOI":"10.3390\/robotics10020067"},{"key":"ref_2","doi-asserted-by":"crossref","unstructured":"Sun, M., Lu, Y., Feng, Y., Zhang, Q., and Liu, S. (2021). Modeling and Verifying the CKB Blockchain Consensus Protocol. Mathematics, 9.","DOI":"10.3390\/math9222954"},{"key":"ref_3","first-page":"33","article-title":"Overview of formal methods","volume":"30","author":"Wang","year":"2019","journal-title":"J. Softw."},{"key":"ref_4","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., and Bloem, R. (2018). Handbook of Model Checking, Springer. Chapter 12.","DOI":"10.1007\/978-3-319-10575-8"},{"key":"ref_5","doi-asserted-by":"crossref","unstructured":"Desai, A., Dreossi, T., and Seshia, S.A. (2017). Combining Model Checking and Runtime Verification for Safe Robotics. Runtime Verification, Proceedings of the International Conference on Runtime Verification, Seattle, WA, USA, 13\u201316 September 2017, Springer.","DOI":"10.1007\/978-3-319-67531-2_11"},{"key":"ref_6","doi-asserted-by":"crossref","unstructured":"Uribe, T.E. (2000, January 22\u201324). Combinations of model checking and theorem proving. Proceedings of the International Workshop on Frontiers of Combining Systems, Nancy, France.","DOI":"10.1007\/10720084_11"},{"key":"ref_7","first-page":"1","article-title":"Combining theorem proving and model checking through symbolic analysis","volume":"1877","author":"Shankar","year":"2000","journal-title":"Int. Conf. Concurr. Theory"},{"key":"ref_8","first-page":"773","article-title":"Algebraic methods for mechanical theorem proving in many-valued logics","volume":"10","author":"Wu","year":"1996","journal-title":"Chin. J. Comput."},{"key":"ref_9","doi-asserted-by":"crossref","unstructured":"Fu, J., Wu, J., and Tan, H. (2015). A deductive approach towards reasoning about algebraic transition systems. Math. Probl. Eng., 607013.","DOI":"10.1155\/2015\/607013"},{"key":"ref_10","doi-asserted-by":"crossref","unstructured":"Platzer, A. (2010). Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Springer Science & Business Media.","DOI":"10.1007\/978-3-642-14509-4"},{"key":"ref_11","doi-asserted-by":"crossref","unstructured":"Liu, J., Zhan, N., and Zhao, H. (2011, January 9\u201314). Computing semi-algebraic invariants for polynomial dynamical systems. Proceedings of the Ninth ACM International Conference on Embedded Software, Taipei, Taiwan.","DOI":"10.1145\/2038642.2038659"},{"key":"ref_12","doi-asserted-by":"crossref","unstructured":"Elias, J. (2006). Automated Geometric Theorem Proving: Wu\u2019s Method. [Master\u2019s Thesis, University of Montana].","DOI":"10.54870\/1551-3440.1034"},{"key":"ref_13","doi-asserted-by":"crossref","unstructured":"Buchberger, B. (1995). Gr\u00f6bner bases: An algorithmic method in polynomial ideal theory. Multidimens. Syst. Theory, 89\u2013127.","DOI":"10.1007\/978-94-017-0275-1_4"},{"key":"ref_14","doi-asserted-by":"crossref","first-page":"865","DOI":"10.1137\/0213054","article-title":"Cylindrical algebraic decomposition. I. The basic algorithm","volume":"13","author":"Arnon","year":"1984","journal-title":"SIAM J. Comput."},{"key":"ref_15","doi-asserted-by":"crossref","unstructured":"Wang, D. (2001). Elimination Methods. Springer.","DOI":"10.1007\/978-3-7091-6202-6"},{"key":"ref_16","doi-asserted-by":"crossref","unstructured":"Fulton, N., Mitsch, S., Quesel, J.D., V\u00f6lp, M., and Platzer, A. (2015, January 1\u20137). KeYmaera X: An axiomatic tactical theorem prover for hybrid systems. Proceedings of the Conference on Automated Deduction, Berlin, Germany.","DOI":"10.1007\/978-3-319-21401-6_36"},{"key":"ref_17","doi-asserted-by":"crossref","first-page":"20150399","DOI":"10.1098\/rsta.2015.0399","article-title":"Industrial hardware and software verification with acl2","volume":"375","author":"Hunt","year":"2017","journal-title":"Philos. Trans. R. Soc. A"},{"key":"ref_18","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Zavadskas, E.K., Tamo\u0161aitien\u0117, J., Adhikary, K., and Kar, S. (2018). A Hybrid MCDM Technique for Risk Management in Construction Projects. Symmetry, 10.","DOI":"10.3390\/sym10020046"},{"key":"ref_19","unstructured":"Kondratyev, A., Stetter, H.J., and Winkler, S. (2004, January 11\u201315). Numerical computation of Gr\u00f6bner bases. Proceedings of the CASC2004 (Computer Algebra in Scientific Computing), Chi\u015fin\u0103u, Moldova."},{"key":"ref_20","doi-asserted-by":"crossref","unstructured":"Wu, P., Xiong, N., Liu, J., Huang, L., Ju, Z., Ji, Y., and Wu, J. (2021). Interval number-based safety reasoning method for verification of decentralized power systems in high-speed trains. Math. Probl. Eng., 6624528.","DOI":"10.1155\/2021\/6624528"},{"key":"ref_21","first-page":"2199","article-title":"Reasoning method based on linear error assertion","volume":"41","author":"Wu","year":"2021","journal-title":"J. Comput. Appl."},{"key":"ref_22","doi-asserted-by":"crossref","unstructured":"Wu, P., Xiong, N., Xiong, J., and Wu, J. (2021). Reasoning method between polynomial error assertions. Information, 12.","DOI":"10.3390\/info12080309"},{"key":"ref_23","unstructured":"Burkardt, J. (2021, November 16). The Truncated Normal Distribution. Available online: https:\/\/people.sc.fsu.edu\/~jburkardt\/presentations\/truncated_normal.pdf."},{"key":"ref_24","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1007\/BF00143942","article-title":"Simulation of truncated normal variables","volume":"5","author":"Robert","year":"1995","journal-title":"Stat. Comput."},{"key":"ref_25","doi-asserted-by":"crossref","unstructured":"Castillo, N.O., Gallardo, D.I., Bolfarine, H., and G\u00f3mez, H.W. (2018). Truncated Power-Normal Distribution with Application to Non-Negative Measurements. Entropy, 20.","DOI":"10.3390\/e20060433"},{"key":"ref_26","doi-asserted-by":"crossref","first-page":"357","DOI":"10.1080\/00031305.1999.10474490","article-title":"Mean and variance of truncated normal distributions","volume":"53","author":"Barr","year":"1999","journal-title":"Am. Stat."},{"key":"ref_27","unstructured":"Shoenfield, J.R. (2001). Mathematical Logic, AK Peters\/CRC Press."},{"key":"ref_28","doi-asserted-by":"crossref","unstructured":"Cs\u00f6rg\u0151, M. (1983). Quantile Processes with Statistical Applications, Society for Industrial and Applied Mathematics.","DOI":"10.1137\/1.9781611970289"},{"key":"ref_29","doi-asserted-by":"crossref","first-page":"1634","DOI":"10.1214\/18-AOS1730","article-title":"Distributed inference for quantile regression processes","volume":"47","author":"Volgushev","year":"2019","journal-title":"Ann. Stat."},{"key":"ref_30","doi-asserted-by":"crossref","unstructured":"Belohlavek, R., Dauben, J.W., and Klir, G.J. (2017). Fuzzy Logic and Mathematics: A Historical Perspective, Oxford University Press.","DOI":"10.1093\/oso\/9780190200015.001.0001"},{"key":"ref_31","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1016\/j.eswa.2017.11.001","article-title":"A fuzzy inference-fuzzy analytic hierarchy process-based clinical decision support system for diagnosis of heart diseases","volume":"95","author":"Nazari","year":"2018","journal-title":"Expert Syst. Appl."},{"key":"ref_32","doi-asserted-by":"crossref","unstructured":"Mehrabi, M., Pradhan, B., Moayedi, H., and Alamri, A. (2020). Optimizing an Adaptive Neuro-Fuzzy Inference System for Spatial Prediction of Landslide Susceptibility Using Four State-of-the-art Metaheuristic Techniques. Sensors, 20.","DOI":"10.3390\/s20061723"},{"key":"ref_33","first-page":"101","article-title":"A fuzzy inference and big data analysis algorithm for the prediction of forest fire based on rechargeable wireless sensor networks","volume":"18","author":"Lin","year":"2018","journal-title":"Sustain. Comput. Infor. Syst."}],"container-title":["Symmetry"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.mdpi.com\/2073-8994\/14\/1\/25\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T17:34:33Z","timestamp":1736271273000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.mdpi.com\/2073-8994\/14\/1\/25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,12,25]]},"references-count":33,"journal-issue":{"issue":"1","published-online":{"date-parts":[[2022,1]]}},"alternative-id":["sym14010025"],"URL":"https:\/\/doi.org\/10.3390\/sym14010025","relation":{},"ISSN":["2073-8994"],"issn-type":[{"type":"electronic","value":"2073-8994"}],"subject":[],"published":{"date-parts":[[2021,12,25]]}}}