Name
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, (@w-)regular model checking, push-down systems, and timed automata. |
Year | DOI | Venue |
|---|---|---|
2006 | 10.1016/j.entcs.2005.11.018 | Electr. Notes Theor. Comput. Sci. |
Keywords | Field | DocType |
safety checking,linear temporal logic,infinite state space,syntactic reduction,previous work,liveness property,finite state system,infinite state system,regular model checking,repeated reachability,liveness,safety,model checking,closed-source model-checking tool,similar reduction,infinite state spaces,state space | Discrete mathematics,Abstraction model checking,Model checking,Computer science,Automaton,Linear temporal logic,Reachability,Theoretical computer science,Mathematical proof,Counterexample,Liveness | Journal |
Volume | Issue | ISSN |
149 | 1 | Electronic Notes in Theoretical Computer Science |
Citations | PageRank | References |
19 | 0.83 | 28 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Viktor Schuppan | 1 | 409 | 17.49 |
| Armin Biere | 2 | 4106 | 245.11 |