Linear time property
In model checking, a branch of computer science, linear time properties are used to describe requirements of a model of a computer system.
Fairness properties can be used to rule out unrealistic paths of a model.
[1] Formally, a linear time property is an ω-language over the power set of "atomic propositions".
An invariant for a system is something that is true or false for a particular state.
This article is about propositional linear-time properties and cannot handle predicates about program states, so it cannot define a property like: the current value of y determines the number of times that x toggles between 0 and 1 before termination.
The more general formalism used in Safety and liveness properties can handle this.
A linear time (LT) property over AP is a subset of
The closure of an LT property P is: Using the theory of finite-state machines, a program or computer system can be modelled by a Kripke structure.
LT properties then describe restrictions on the traces (outputs) of a Kripke structure.
For instance, if two traffic lights at an intersection are represented by a Kripke structure then the atomic propositions may be the possible colours of each light and it may be desirable that the traces satisfy the LT property "the traffic lights cannot both be green at the same time" (to avoid car collisions).
[4] 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".
Another is "the variable x is never negative", in a model of a computer program.
Formally, an invariant is of the form: for some propositional logic formula
[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".
i.e. any finite string can be continued to a valid trace.
In terms of computer programs, useful liveness properties include "the program eventually terminates" and, in concurrent computing, "every process must eventually be served".
[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".
Weak fairness is of the form "every process gets its turn infinitely often if it is continuously enabled from a particular point".
So long as a set of fairness conditions are realizable, they are irrelevant to safety properties.
[24] All linear temporal logic (LTL) formulae are LT properties.
By a counting argument, we see that any logic in which each formula is a finite string cannot represent all LT properties, as there must be countably many formulae but there are uncountably many LT properties.
