Name
Abstract | ||
|---|---|---|
Two types of temporal properties are usually distinguished: safety and liveness. Recently we have shown how to verify liveness properties of finite state systems using safety checking. In this article we extend the translation scheme to typical combinations of temporal operators. We discuss optimizations that limit the overhead of our translation. Using the notions of predicated diameter and radius we obtain revised bounds for our translation scheme. These notions also give a tight bound on the minimal completeness bound for simple liveness properties. Experimental results show the feasibility of the approach for complex examples. For one example, even an exponential speedup can be observed. |
Year | DOI | Venue |
|---|---|---|
2004 | 10.1007/s10009-003-0121-x | STTT |
Keywords | Field | DocType |
complex example,safety checking,linear temporal logic,translation scheme,simple liveness property,temporal property,liveness property,finite state model checking,finite state system,liveness,efficient reduction,safety,model checking,exponential speedup,temporal operator | Model checking,Exponential function,Computer science,Algorithm,Reachability,Theoretical computer science,Linear temporal logic,Operator (computer programming),Completeness (statistics),Liveness,Speedup | Journal |
Volume | Issue | Citations |
5 | 2 | 39 |
PageRank | References | Authors |
1.47 | 27 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Viktor Schuppan | 1 | 409 | 17.49 |
| Armin Biere | 2 | 4106 | 245.11 |