Sciweavers

Share
ENTCS
2006

Liveness Checking as Safety Checking for Infinite State Spaces

10 years 2 months ago
Liveness Checking as Safety Checking for Infinite State Spaces
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. Key words: liveness, safety, linear temporal logic, model checking, infinite state space
Viktor Schuppan, Armin Biere
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ENTCS
Authors Viktor Schuppan, Armin Biere
Comments (0)
books