A safety property P defines a deterministic process that asserts that any trace including actions in the alphabet of P, is accepted by P.
Progress progress
progress P = {a1,a2..an} defines a progress property P which asserts that in an infinite execution of a target system, at least one of the actions a1,a2..an will be executed infinitely often.