UM
Residential Collegefalse
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 Name21st ACM International Conference on Hybrid Systems - Computation and Control (HSCC)
Source PublicationHSCC 2018 - Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)
Pages81-90
Conference DateAPR 11-13, 2018
Conference PlacePorto, 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.

KeywordDuration Calculus Eldi Model Checking Quantified Linear Real Arithmetic Timed Automata
DOI10.1145/3178126.3178147
URLView the original
Language英語English
WOS IDWOS:000474781600009
Scopus ID2-s2.0-85049445470
Fulltext Access
Citation statistics
Document TypeConference paper
CollectionUniversity of Macau
Affiliation1.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.
Related Services
Recommend this item
Bookmark
Usage statistics
Export to Endnote
Google Scholar
Similar articles in Google Scholar
[An J.]'s Articles
[Zhan N.]'s Articles
[Li X.]'s Articles
Baidu academic
Similar articles in Baidu academic
[An J.]'s Articles
[Zhan N.]'s Articles
[Li X.]'s Articles
Bing Scholar
Similar articles in Bing Scholar
[An J.]'s Articles
[Zhan N.]'s Articles
[Li X.]'s Articles
Terms of Use
No data!
Social Bookmark/Share
All comments (0)
No comment.
 

Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.