Could someone kindly explain why safety properties are commonly informally described as "something bad never happens"? This doesn't seem accurate at all. Rather, it seems that one should say "if something bad happens, you can always guarantee it will have happened in a finite amount of time" where "something bad happens" means the property is necessarily violated.

The corresponding definition for liveness properties that "something good should eventually happen" makes sense, though arguably the word "good" should be taken out.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.