Name
Abstract | ||
|---|---|---|
Temporal logic is widely used for specifying hardware and software systems. Typically two types of properties are distinguished, safety and liveness properties. While safety can easily be checked by reachability analysis, and many efficient checkers for safety properties exist, more sophisticated algorithms have always been considered to be necessary for checking liveness. In this paper we describe an efficient translation of liveness checking problems into safety checking problems. A counter example is detected by saving a previously visited state in an additional state recording component and checking a loop closing condition. The approach handles fairness and thus extends to full LTL. |
Year | DOI | Venue |
|---|---|---|
2002 | 10.1016/S1571-0661(04)80410-9 | Electronic Notes in Theoretical Computer Science |
Keywords | Field | DocType |
software systems,temporal logic | Computation tree logic,Discrete mathematics,Abstraction model checking,Model checking,Computer science,Software system,Real-time computing,Theoretical computer science,Reachability,Temporal logic,Counterexample,Liveness | Journal |
Volume | Issue | ISSN |
66 | 2 | 1571-0661 |
Citations | PageRank | References |
53 | 2.20 | 19 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Armin Biere | 1 | 4106 | 245.11 |
| Cyrille Artho | 2 | 588 | 44.46 |
| Viktor Schuppan | 3 | 409 | 17.49 |