Linear Temporal Logic - Applications

Applications

Automata theoretic Linear temporal logic model checking

An important way to model check is to express desired properties (such as the ones described above) using LTL operators and actually check if the model satisfies this property. One technique is to obtain a Büchi automaton that is "equivalent" to the model and one that is "equivalent" to the negation of the property. The intersection of the two non-deterministic Büchi automata is empty if the model satisfies the property.

Expressing important properties in formal verification

There are two main types of properties that can be expressed using linear temporal logic: safety properties usually state that something bad never happens (G), while liveness properties state that something good keeps happening (GF or GF). More generally: Safety properties are those for which every counterexample has a finite prefix such that, however it is extended to an infinite path, it is still a counterexample. For liveness properties, on the other hand, every finite prefix of a counterexample can be extended to an infinite path that satisfies the formula.

Specification language

One of the applications of linear temporal logic is the specification of preferences in the Planning Domain Definition Language for the purpose of preference-based planning.