Liveness
A liveness property is, informally, that “good things always happen”. Like “the database will eventually commit the data” or “if the worker continually retries, it will eventually succeed” or “if someone requests a book, they eventually get a chance to borrow it.”
These are much less common than safety property but often core business requirements. A system satisfies all safety properties if it just sits there and does nothing, since it never does anything bad. But it never does anything good, either. Liveness properties are only violatible by infinite traces: you have to show you never eventually do the thing to have a problem.
Some common genres of liveness properties:
- thing eventually is true. We eventually show an alert, even if it disappears later.
- thing eventually is true and stays true. The database nodes can disagree on what was written, but eventually they will all converge on the same thing and it stays that way.
- thing always comes back to true. The vehicle can temporarily go over the speed limit, but it can’t stay above the speed limit forever, and must eventually come back down.
- condition leads to thing being true in the future. If I send a message, you eventually receive it.
- Fairness
证明程序的终止性就是一种liveness属性（it will eventually terminate, see 终止性分析)
liveness property可以用它代表的模型形式化地定义, see temporal liveness property。
一般而言，liveness property比safety property更难验证。