Liveness Checking as Safety Checking for Infinite State Spaces |
| |
Authors: | Viktor Schuppan Armin Biere |
| |
Affiliation: | ETH Zürich, Computer Systems Institute, CH-8092 Zürich, Switzerland;Johannes Kepler University, Institute for Formal Models and Verification, Altenbergerstrasse 69, A-4040 Linz, Austria |
| |
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. |
| |
Keywords: | liveness safety linear temporal logic model checking infinite state space |
本文献已被 ScienceDirect 等数据库收录! |
|