Liveness checking as safety checking
Abstract: Temporal logic is widely used for specifying hardware and software systems. Typically two types of properties are distinguished, safety and liveness properties. While safety can easily be checked by reachability analysis, and many efficient checkers for safety properties exist, more sophisticated algorithms have always been considered to be necessary for checking liveness. In this paper we describe an efficient translation of liveness checking problems into safety checking problems. A counter example is detected by saving a previously visited state in an additional state recording component and checking a loop closing condition. The approach handles fairness and thus extends to full LTL
- Location
-
Deutsche Nationalbibliothek Frankfurt am Main
- Extent
-
Online-Ressource
- Language
-
Englisch
- Notes
-
ISSN: 1571-0661
- Event
-
Veröffentlichung
- (where)
-
Freiburg
- (who)
-
Universität
- (when)
-
2023
- Creator
- DOI
-
10.1016/s1571-0661(04)80410-9
- URN
-
urn:nbn:de:bsz:25-freidok-2395248
- Rights
-
Open Access; Der Zugriff auf das Objekt ist unbeschränkt möglich.
- Last update
-
25.03.2025, 1:53 PM CET
Data provider
This object is provided by:
Deutsche Nationalbibliothek. If you have any questions about the object, please contact the data provider.
Deutsche Nationalbibliothek. If you have any questions about the object, please contact the data provider.
Associated
- Biere, Armin
- Artho, Cyrille
- Schuppan, Viktor
- Universität
Time of origin
- 2023
Other Objects (12)
Liveness checking as safety checking for infinite state spaces
Interpolation in software model checking and fault localization : = Interpolation in Software Model Checking und Defektlokalisierung
Combining local and global model checking
Transition-based directed model checking : = Transitionsbasierte gerichtete Modellprüfung
Model checking for time division multiple access systems
Symbolic Causality Checking Using Bounded Model Checking
Symbolic Causality Checking Using Bounded Model Checking
Monotonicity checking
Specifying and model checking distributed control algorithms at meta-level
Causality Checking of Safety-Critical Software and Systems
Type-checking AHEAD
RDF constraint checking
Liveness checking as safety checking for infinite state spaces
Interpolation in software model checking and fault localization : = Interpolation in Software Model Checking und Defektlokalisierung
Combining local and global model checking
Transition-based directed model checking : = Transitionsbasierte gerichtete Modellprüfung
Model checking for time division multiple access systems
Symbolic Causality Checking Using Bounded Model Checking
Symbolic Causality Checking Using Bounded Model Checking
Monotonicity checking
Specifying and model checking distributed control algorithms at meta-level
Causality Checking of Safety-Critical Software and Systems
Type-checking AHEAD
RDF constraint checking
Liveness checking as safety checking for infinite state spaces
Interpolation in software model checking and fault localization : = Interpolation in Software Model Checking und Defektlokalisierung
Combining local and global model checking
Transition-based directed model checking : = Transitionsbasierte gerichtete Modellprüfung
Model checking for time division multiple access systems
Symbolic Causality Checking Using Bounded Model Checking
Symbolic Causality Checking Using Bounded Model Checking
Monotonicity checking
Specifying and model checking distributed control algorithms at meta-level
Causality Checking of Safety-Critical Software and Systems
Type-checking AHEAD