The kinds of properties you have seen so far are sometimes called safety properties, properties that say that ``nothing bad happens.'' Another class of properties that people often discuss are called liveness properties, properties that say that ``something good eventually happens.'' For a sequential system, computing the correct answer is an example of a safety property and termination of a program is an example of a liveness property (this program ``eventually'' terminates). For a concurrent system, deadlock freedom and mutual exclusion are examples of safety properties; for a distributed system, the property that a message sent is eventually received is an example of a liveness property.
For concurrent and distributed systems, there are many interesting liveness properties so we will defer discussing them until later in the course.