Sökning: id:"swepub:oai:research.chalmers.se:412aeb13-cd35-49c6-89a4-8a0a78e535d9" >
Efficient Temporal ...
Efficient Temporal Logic Verification by Incremental Abstraction
-
- Lennartson, Bengt, 1956 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Liang, Xudong (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
- Noori-Hosseini, Mona, 1982 (författare)
- Chalmers tekniska högskola,Chalmers University of Technology
-
(creator_code:org_t)
- 2020
- 2020
- Engelska.
-
Ingår i: IEEE International Conference on Automation Science and Engineering. - 2161-8070 .- 2161-8089. ; 2020-August, s. 894-899
- Relaterad länk:
-
https://doi.org/10.1...
-
visa fler...
-
https://research.cha...
-
https://research.cha...
-
visa färre...
Abstract
Ämnesord
Stäng
- A recently formulated incremental abstraction method that preserves CTL∗-X is further developed and evaluated in this paper. The temporal logic CTL∗-X includes both linear temporal logic (LTL) and computational tree logic (CTL), except for the next operator (often denoted by X). For a modular transition system, the incremental abstraction means that any local events, only included in one of the subsystems, are first abstracted. After synchronization more events become local. Repeated abstraction then means that further reduction of local transitions is achieved when more submodels are synchronized. This incremental abstraction is evaluated as a tool for temporal logic verification, and compared with a couple of competitive alternatives. In a preliminary evaluation, the proposed incremental abstraction is often shown to be the most efficient choice for verification of temporal logic properties, especially when some individual submodels are comparatively large.
Ämnesord
- TEKNIK OCH TEKNOLOGIER -- Annan teknik -- Övrig annan teknik (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Other Engineering and Technologies -- Other Engineering and Technologies not elsewhere specified (hsv//eng)
- TEKNIK OCH TEKNOLOGIER -- Elektroteknik och elektronik -- Inbäddad systemteknik (hsv//swe)
- ENGINEERING AND TECHNOLOGY -- Electrical Engineering, Electronic Engineering, Information Engineering -- Embedded Systems (hsv//eng)
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- nonblocking verification
- modular systems
- temporal logic verification
Publikations- och innehållstyp
- kon (ämneskategori)
- ref (ämneskategori)
Hitta via bibliotek
Till lärosätets databas