Residential College | false |
Status | 已發表Published |
Model checking bounded continuous-time Extended Linear Duration Invariants | |
An J.3; Zhan N.1; Li X.4; Zhang M.3; Yi W.2 | |
2018-04-11 | |
Conference Name | 21st ACM International Conference on Hybrid Systems - Computation and Control (HSCC) |
Source Publication | HSCC 2018 - Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week) |
Pages | 81-90 |
Conference Date | APR 11-13, 2018 |
Conference Place | Porto, PORTUGAL |
Abstract | Extended Linear Duration Invariants (ELDI), an important subset of Duration Calculus, extends well-studied Linear Duration Invariants with logical connectives and the chop modality. It is known that the model checking problem of ELDI is undecidable with both the standard continuous-time and discrete-time semantics [12, 13], but it turns out to be decidable if only bounded execution fragments of timed automata are concerned in the context of the discrete-time semantics [36]. In this paper, we prove that this problem is still decidable in the continuous-time semantics, although it is well-known that model-checking Duration Calculus with the continuous-time semantics is much more complicated than the one with the discrete-time semantics. This is achieved by reduction to the validity of Quantified Linear Real Arithmetic (QLRA). Some examples are provided to illustrate the eficiency of our approach. |
Keyword | Duration Calculus Eldi Model Checking Quantified Linear Real Arithmetic Timed Automata |
DOI | 10.1145/3178126.3178147 |
URL | View the original |
Language | 英語English |
WOS ID | WOS:000474781600009 |
Scopus ID | 2-s2.0-85049445470 |
Fulltext Access | |
Citation statistics | |
Document Type | Conference paper |
Collection | University of Macau |
Affiliation | 1.Institute of Software Chinese Academy of Sciences 2.Uppsala Universitet 3.Tongji University 4.Universidade de Macau |
Recommended Citation GB/T 7714 | An J.,Zhan N.,Li X.,et al. Model checking bounded continuous-time Extended Linear Duration Invariants[C], 2018, 81-90. |
APA | An J.., Zhan N.., Li X.., Zhang M.., & Yi W. (2018). Model checking bounded continuous-time Extended Linear Duration Invariants. HSCC 2018 - Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), 81-90. |
Files in This Item: | There are no files associated with this item. |
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment