2
$\begingroup$

A property $P$ is simply a set of sequences of states and a certain program is characterized by its set of sequences of states, let's call it $T$. A program is compliant to a specific property P if $T\subseteq P$.

Intuitively, a specific liveness property LP1 is the set of traces (sequences of states ) in each of which "something good" will happen, based on the specific property LP1 (for example "termination"). This means that if a program it's compliant with LP1 in each of its traces the "good thing" will happen, that is the program will terminate.

However, I don't understand how the formal definition of liveness property contains what was said, can you explain me? This definition to me makes no sense (i know all the terminology)...

$\forall t\in S^{*}\,(\exists t'\in S^{\omega }:t\leq t^{'}\wedge t^{'}\in LP1)$

$\endgroup$
2
$\begingroup$

I'm not sure where the particular liveness definition you wrote comes from, but the definition given in Defining Liveness (Schneider, Alpern, 1985) is as follows.

A property $P$ is a liveness property if and only if: $$ \forall \alpha \in S^* : (\exists \beta \in S^\omega : \alpha\beta \vDash P) $$

where $S^*$ is the set of all partial executions and $S^\omega$ is the set of all infinite executions.

This definition captures the intuition that the "good thing" (the "something good" that you mentioned) specified by a liveness property can always occur in the future. That is, no matter the finite prefix $\alpha$ you choose, you can always find an infinite suffix $\beta$ to extend it with that will satisfy a liveness property $P$. I am assuming that the $\leq$ symbol in the definition you gave is used to express a prefix relationship between traces, which makes it analogous to the definition from the paper.

You might make an argument for defining liveness in some alternative way. Indeed, two slightly different characterizations of liveness are given in that same paper (see uniform liveness and absolute liveness). The definition given above, though, provides a basis for the topological characterization of safety and liveness properties which they use to prove the decomposition theorem i.e. that any property can be expressed as a conjunction of a safety and liveness property. So, it would seem that the definition is relatively "natural".

As they remark in the final paragraph of that paper:

It seems naive to hope for a proof that a formal definition for liveness (or safety) is correct, because "good things" and "bad things" are not well-defined concepts. However, the simple topological characterization of the definitions suggests that they do indeed capture fundamental distinctions.

| cite | improve this answer | |
$\endgroup$

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.