Exact definition of "Liveness" and "Safety" properties in a consensus? Two main properties of a consensus are "Liveness" and "Safety".

What are the exact and precised definition of "Liveness" and "Safety" properties in a consensus ?

Are the following definitions correct?


Safety: Achieving an agreement on a single state by all participants ?
Liveness: Possibility of updating this state with keeping the agreement ?
Safety: Any transaction deemed final by one properly-operating node will eventually be deemed final by every properly-operating node. No two transactions ever deemed final by two properly-operating nodes will ever conflict.

Liveness: So long as there is always at least one transaction suitable for inclusion that has not been deemed final by any properly-operating nodes, the set of transactions deemed final by at least one properly-operating node will increase in number.

Note that these are very, very minimal definitions and generally not sufficient for realistic systems. Also, for some systems (where a transaction can produce different results depending on the context in which it executes), you have to understand "transaction" to mean the results of executing the transaction.