# Definition of liveness property in model checking

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