ACTL strong negation and its application to hybrid systems verification |
| |
| Affiliation: | 1. Department of Electrical and Computer Engineering, Carnegie Mellon University, Pittsburgh, PA, USA;2. The MathWorks, Inc., 3 Apple Hill Dr, Natick, MA 01760-2098, USA;1. IFAC Technical Committee on Discrete Event and Hybrid Systems, CReSTIC, University of Reims, Moulin de la housse, BP 1039, 51687 Reims cedex 2, France;2. IFAC Technical Committee on Discrete Event and Hybrid Systems, CReSTIC, University of Reims, Moulin de la housse, BP 1039, 51687 Reims cedex 2, France;1. Department of Chemical and Petroleum Engineering, University of Calgary, 2500 University Dr. N.W., Calgary, AB T2N 1N4, Canada;2. Thermochemical Processing, InnoTech Alberta, P.O. Bag 4000, Vegreville, T9C 1T4, Alberta, Canada;1. Faculty of Sciences, University of Sfax, Road of Soukra km 4 – BP n° 802, 3038 Sfax, Tunisia;2. School of Agricultural, Forestry, Food and Environmental Sciences, University of Basilicata, Viale dell’Ateneo Lucano, 10, 85100 Potenza, Italy;3. Department of Soil, Plant and Food Sciences, University of Bari, Via Amendola 165/A, 70126, Bari, Italy;1. MRC Human Genetics Unit at the MRC IGMM at the University of Edinburgh, Edinburgh EH4 2XU, United Kingdom;2. Institute of Molecular and Cell Biology, Agency for Science Technology and Research (A⁎STAR), Biopolis, Singapore 138673, Singapore;1. School of Environmental Science and Engineering, Zhejiang Gongshang University, 18 Xuezheng Street, Xiasha Gaojiaoyuan District, Hangzhou, Zhejiang, 310018, China;2. College of Engineering, Nanjing Agricultural University, 40 Dianjiangtai Road, Pukou District, Nanjing, Jiangsu, 210031, China;3. Department of Road Traffic and Engineering Planning, Zhejiang Urban & Rural Planning Design Institute, 238 Baochu Road, Xihu District, Hangzhou, Zhejiang, 310007, China;4. Department of Management and Information Technology, Nantong Shipping College, 185 Tongsheng Road, Nantong, Jiangsu, 226010, China;5. School of Environmental Science and Engineering, Huazhong University of Science & Technology, 1037 Luoyu Road, Wuhan, Hubei, 430074, China;1. Department of Medicine, Stony Brook University School of Medicine, HSC-T16 Room 020, Stony Brook, NY 11794, USA;2. Division of Digestive Diseases, Department of Medicine, Emory University School of Medicine, 615 Michael Street, Atlanta, GA 30322, USA;3. Department of Pathology, Stony Brook University School of Medicine, BST-9, Stony Brook Medicine, Stony Brook, NY 11794-8691, USA;4. Department of Morphogenesis and Intracellular Signalling, Institut Curie-CNRS, Paris, France |
| |
| Abstract: | Model checking procedures for verifying properties of hybrid dynamic systems are based on the construction of finite-state abstractions. If the property is not satisfied by the abstraction, the verification is inconclusive and the abstraction needs to be refined so that a less conservative model can be checked. If the hybrid system does not satisfy the property, this verify–refine procedure usually will not terminate. This paper introduces the concept of strong negation for ACTL formulas as an auxiliary condition that can be verified to obtain a conclusive negative verification result from a finite-state abstraction in certain cases. The concepts are illustrated with an example from automotive powertrain control. |
| |
| Keywords: | |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
