Menu
Home
People
Places
Arts
History
Plants & Animals
Science
Life & Culture
Technology
Reference.org
Linear time property
open-in-new
<p>In <a href="/facts/Model_checking/FwvKMlw9">model checking</a>, a branch of <a href="/facts/Computer_science/lN3pEyPz">computer science</a>, linear time properties are used to describe requirements of a model of a <a href="/facts/Computer_system/SQe1aK05">computer system</a>. Example properties include "the vending machine does not dispense a drink until money has been entered" (a <a href="/facts/Safety_property/B5mBFLVR">safety property</a>) or "the computer program eventually terminates" (a <a href="/facts/Liveness_property/hFd5W0uN">liveness property</a>). Fairness properties can be used to rule out unrealistic paths of a model. For instance, in a model of two traffic lights, the liveness property "both traffic lights are green infinitely often" may only be true under the unconditional fairness constraint "each traffic light changes colour infinitely often" (to exclude the case where one traffic light is "infinitely faster" than the other). </p><p>Formally, a linear time property is an <a href="/facts/Omega_language/sJwjxW2U">ω-language</a> over the <a href="/facts/Power_set/FVuf8PDD">power set</a> of "atomic propositions". That is, the property contains sequences of sets of propositions, each sequence known as a "word". Every property can be rewritten as "<i>P</i> and <i>Q</i> both occur" for some safety property <i>P</i> and liveness property <i>Q</i>. An invariant for a system is something that is true or false for a particular state. Invariant properties describe an invariant that every reachable state of a model must satisfy, while persistence properties are of the form "eventually forever some invariant holds". </p><p><a href="/facts/Temporal_logic/vANP39lc">Temporal logics</a> such as <a href="/facts/Linear_temporal_logic/Gh5yxXK7">linear temporal logic</a> describe types of linear time properties using formulae. </p><p>This article is about <a href="/facts/Propositional_formula/eEV8YrAI">propositional</a> linear-time properties and cannot handle predicates about program states, so it cannot define a property like: <i>the current value of y determines the number of times that x toggles between 0 and 1 before termination.</i> The more general formalism used in <a href="/facts/Safety_and_liveness_properties/B5mBFLVR">Safety and liveness properties</a> can handle this. </p>