Sökning: id:"swepub:oai:DiVA.org:uu-390243" >
Model Checking Boun...
Model Checking Bounded Continuous-time Extended Linear Duration Invariants
-
- An, Jie (författare)
- Tongji Univ, Sch Software Engn, Shanghai, Peoples R China
-
- Zhan, Naijun (författare)
- Chinese Acad Sci, Inst Software, State Key Lab Comp Sci, Beijing, Peoples R China;Uni CAS, Beijing, Peoples R China
-
- Li, Xiaoshan (författare)
- Univ Macau, Fac Sci & Technol, Macau, Peoples R China
-
visa fler...
-
- Zhang, Miaomiao (författare)
- Tongji Univ, Sch Software Engn, Shanghai, Peoples R China
-
- Wang, Yi (författare)
- Uppsala universitet,Datorteknik,Uppsala Univ, Dept Informat Technol, Uppsala, Sweden
-
visa färre...
-
(creator_code:org_t)
- 2018-04-11
- 2018
- Engelska.
-
Ingår i: HSCC 2018. - New York, NY, USA : ASSOC COMPUTING MACHINERY. ; , s. 81-90
- Relaterad länk:
-
https://urn.kb.se/re...
-
visa fler...
-
https://doi.org/10.1...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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 efficiency of our approach.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- Model Checking
- Duration Calculus
- ELDI
- Timed Automata
- Quantified Linear Real Arithmetic
Publikations- och innehållstyp
- ref (ämneskategori)
- kon (ämneskategori)