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)$


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.