Linear time property

A safety property is informally of the form "a bad thing does not happen".[5] For instance, if a system models an automated teller machine (ATM) then such a property is "money should not be dispensed unless a PIN has been entered".[6] Formally, a safety property is an LT property such that any word that violates the property has a "bad prefix", for which no word with that prefix satisfies the property. That is,[7]

${\displaystyle \forall \sigma \in (2^{AP})^{\omega }\setminus P\ \exists {\text{ a finite prefix}}\ {\hat {\sigma }}:P\cap \{\sigma '\mid {\hat {\sigma }}\ {\text{is a prefix of}}\ \sigma '\}=\emptyset }$

In the ATM example, a minimal bad prefix is a finite set of steps carried out in which money is dispensed in the last step and a PIN is not entered at any step. To verify a safety property, it is sufficient to consider only the finite traces of a Kripke structure and check whether any such trace is a bad prefix.[8]

An LT property P is a safety property if and only if ${\displaystyle {\mathit {closure}}(P)=P}$.[9]

An invariant property is a type of safety property in which the condition only refers to the current state.[10] For instance, the ATM example is not an invariant because we cannot tell whether the property is violated by seeing that the current state is "dispense money", only by seeing that the current state is "dispense money" and no previous state was "read PIN". An example of an invariant is the traffic light condition "the traffic lights cannot both be green at the same time" above. Another is "the variable x is never negative", in a model of a computer program.

Formally, an invariant is of the form:

${\displaystyle P=\{A_{0}A_{1}....\in (2^{AP})^{\omega }\mid \forall j\in \mathbb {N} :A_{j}\ {\text{satisfies}}\ \Phi \}}$

for some propositional logic formula ${\displaystyle \Phi }$.[10]

A Kripke structure satisfies an invariant if and only if every reachable state satisfies the invariant, which can be checked by a breadth-first search or depth-first search.[11] Safety properties can be verified inductively using invariants.[12]

A liveness property is informally of the form "something good eventually happens".[5] Formally, P is a liveness property if ${\displaystyle {\mathit {pref}}(P)=(2^{AP})^{*}}$ i.e. any finite string can be continued to a valid trace.[13][7] An example of a liveness property is the previous LT property "the set of words that contain a infinitely often". No finite prefix of a word can prove that the word does not satisfy this property, as the word could continue on to have infinitely many as.

In terms of computer programs, useful liveness properties include "the program eventually terminates" and, in concurrent computing, "every process must eventually be served".[14]

A persistence property is a liveness property of the form "eventually forever ${\displaystyle \Phi }$". That is, a property of the form:[15]

${\displaystyle P=\{A_{0}A_{1}...\in (2^{AP})^{\omega }\mid \exists N\in \mathbb {N}$ :\forall n\geq N:A_{n}\ {\text{satisfies}}\ \Phi \}}

No LT property other than ${\displaystyle (2^{AP})^{\omega }}$ (the set of all words over ${\displaystyle 2^{AP}}$) is both a safety and a liveness property.[16] Though not every property is a safety property or a liveness property (consider "a occurs exactly once"), every property is the intersection of a safety and a liveness property.[5]

In topology, the set of all words ${\displaystyle (2^{AP})^{\omega }}$ can be equipped with the metric:

${\displaystyle d(w,x):=\inf\{2^{-|s|}\mid s\in {\mathit {pref}}(w)\cap {\mathit {pref}}(x)\}}$

Then a safety property is a closed set and a liveness property is a dense set.[17]

Fairness properties are preconditions imposed on a system to rule out unrealistic traces.[18][19] Unconditional fairness is of the form "every process gets its turn infinitely often". Strong fairness is of the form "every process gets its turn infinitely often if it is enabled infinitely often". Weak fairness is of the form "every process gets its turn infinitely often if it is continuously enabled from a particular point".[20]

In some systems, a fairness constraint is defined by a set of states, and a "fair path" is one that passes through some state in the fairness constraint infinitely often. If there are multiple fairness constraints, then a fair path must pass infinitely often through one state per constraint.[21] A program "fairly satisfies" an LT property P with respect to a set of fairness conditions if for every path, either the path fails a fairness condition or it satisfies P. That is, the property P is satisfied for all fair paths.[22]

A fairness property is realizable for a Kripke structure if every reachable state has a fair path starting from that state. So long as a set of fairness conditions are realizable, they are irrelevant to safety properties.[23]