Liveness checking as safety checking for infinite state spaces
Abstract: In previous work we have developed a syntactic reduction of repeated reachability to reachability for finite state systems. This may lead to simpler and more uniform proofs for model checking of liveness properties, help to find shortest counterexamples, and overcome limitations of closed-source model-checking tools. In this paper we show that a similar reduction can be applied to a number of infinite state systems, namely, (ω−)regular model checking, push-down systems, and timed automata
- 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/j.entcs.2005.11.018
- URN
-
urn:nbn:de:bsz:25-freidok-2395028
- Rechteinformation
-
Open Access; Der Zugriff auf das Objekt ist unbeschränkt möglich.
- Letzte Aktualisierung
-
14.08.2025, 10:58 MESZ
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
- Schuppan, Viktor
- Biere, Armin
- Universität
Entstanden
- 2023
Ähnliche Objekte (12)
Liveness checking as safety checking
Infinite state model checking of propositional dynamic logics
Infinite state AMC-model checking for cryptographic protocols
Decidability and complexity of model checking problems for infinite state systems
Towards Infinite-State Symbolic Model Checking for B and Event-B
Diagnostic checking in linear processes with infinit variance
Diagnostic checking in linear processes with infinite variance
Model checking abstract state machines
Symbolic Causality Checking Using Bounded Model Checking
Symbolic Causality Checking Using Bounded Model Checking
From non-disjoint combination to satisfiability and model checking of infinite state systems
Monotonicity checking
Liveness checking as safety checking
Infinite state model checking of propositional dynamic logics
Infinite state AMC-model checking for cryptographic protocols
Decidability and complexity of model checking problems for infinite state systems
Towards Infinite-State Symbolic Model Checking for B and Event-B
Diagnostic checking in linear processes with infinit variance
Diagnostic checking in linear processes with infinite variance
Model checking abstract state machines
Symbolic Causality Checking Using Bounded Model Checking
Symbolic Causality Checking Using Bounded Model Checking
From non-disjoint combination to satisfiability and model checking of infinite state systems
Monotonicity checking
Liveness checking as safety checking
Infinite state model checking of propositional dynamic logics
Infinite state AMC-model checking for cryptographic protocols
Decidability and complexity of model checking problems for infinite state systems
Towards Infinite-State Symbolic Model Checking for B and Event-B
Diagnostic checking in linear processes with infinit variance
Diagnostic checking in linear processes with infinite variance
Model checking abstract state machines
Symbolic Causality Checking Using Bounded Model Checking
Symbolic Causality Checking Using Bounded Model Checking
From non-disjoint combination to satisfiability and model checking of infinite state systems