Model checking bounded continuous-time Extended Linear Duration Invariants
An J.3; Zhan N.1; Li X.4; Zhang M.3; Yi W.2
Source PublicationHSCC 2018 - Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)
AbstractExtended 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
URLView the original
Fulltext Access
Citation statistics
Cited Times [WOS]:0   [WOS Record]     [Related Records in WOS]
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.
Files in This Item:
There are no files associated with this item.
Related Services
Recommend this item
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.