Definition. Obligation properties [ltp-0011]

An obligation property is comprised of (finite) boolean combinations of safety and guarantee properties. That is:

  • Every guarantee property is an obligation property.
  • If P is an obligation property, then P^\complement is an obligation property.
  • If P and Q are obligation properties, then P \cap Q is an obligation property.
  • If P and Q are obligation properties, then P \cup Q is an obligation property.

Topologically, this is called the constructible sets of our topology.