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
- Standort
-
Deutsche Nationalbibliothek Frankfurt am Main
- Umfang
-
Online-Ressource
- Sprache
-
Englisch
- Anmerkungen
-
ISSN: 1571-0661
- Ereignis
-
Veröffentlichung
- (wo)
-
Freiburg
- (wer)
-
Universität
- (wann)
-
2023
- Urheber
- DOI
-
10.1016/s1571-0661(04)80410-9
- URN
-
urn:nbn:de:bsz:25-freidok-2395248
- Rechteinformation
-
Open Access; Der Zugriff auf das Objekt ist unbeschränkt möglich.
- Letzte Aktualisierung
-
25.03.2025, 13:53 MEZ
Datenpartner
Dieses Objekt wird bereitgestellt von:
Deutsche Nationalbibliothek. Bei Fragen zum Objekt wenden Sie sich bitte an den Datenpartner.
Deutsche Nationalbibliothek. Bei Fragen zum Objekt wenden Sie sich bitte an den Datenpartner.
Beteiligte
- Biere, Armin
- Artho, Cyrille
- Schuppan, Viktor
- Universität
Entstanden
- 2023
Ähnliche Objekte (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
Causality Checking of Safety-Critical Software and Systems
Specifying and model checking distributed control algorithms at meta-level
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
Causality Checking of Safety-Critical Software and Systems
Specifying and model checking distributed control algorithms at meta-level
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
Causality Checking of Safety-Critical Software and Systems
Specifying and model checking distributed control algorithms at meta-level
Type-checking AHEAD