@inproceedings{f03a8c4d0d5a4017abe3ec3e5b007056,
title = "Model checking bounded continuous-time Extended Linear Duration Invariants",
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.",
keywords = "Duration calculus, ELDI, Model checking, Quantified linear real arithmetic, Timed automata",
author = "Jie An and Naijun Zhan and Xiaoshan Li and Miaomiao Zhang and Wang Yi",
note = "Publisher Copyright: {\textcopyright} 2018 Copyright held by the owner/author(s).; 21st International Conference on Hybrid Systems: Computation and Control, HSCC 2018 ; Conference date: 11-04-2018 Through 13-04-2018",
year = "2018",
month = apr,
day = "11",
doi = "10.1145/3178126.3178147",
language = "英语",
series = "HSCC 2018 - Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week)",
publisher = "Association for Computing Machinery, Inc",
pages = "81--90",
booktitle = "HSCC 2018 - Proceedings of the 21st International Conference on Hybrid Systems",
}