LTL

Created: 2012/11/21 16:47:39+0000

Linear Temporal Logic is an extension to propositional logic that allows the description of changes over time and repeated behavior. The propositions can be replaced by predicates to represent the state of Event-B machines. LTL allows reasoning about the state at different points in time. It does not allow time to be measured but ensures that different points in time are distinct. It provides temporal operators that can be used for this.

Several temporal operators are provided, others can be constructed from the basic ones and boolean operators. The operators apply to all paths from the state. The Next temporal operator is a unary operator that is satisfied by the paths where the operator's proposition holds in the next state of the path. The Until operator is a binary operator that is satisfied by the paths where the operator's first proposition is true until the operator's second proposition is true, the first proposition does not need to hold if the second proposition holds from the first state and the second proposition must eventually hold.