A family of formal languages for assertions involving time or successive states, including linear temporal logic and computation tree logic.
A branching temporal logic whose operators quantify over paths in a transition system from a state. In particular, , also written , holds at when every infinite path in a transition system from satisfies at every position, including its initial position.
A temporal logic interpreted along infinite paths in a transition system. At position , requires at , requires it at some , and requires it at every . Strong until and weak until express conditions that hold up to a later event. A system satisfies a specification when all relevant initial paths in a transition system satisfy it.
In linear temporal logic, means . Thus it permits the left operand to hold forever without the right operand ever becoming true, unlike strong until.
In linear temporal logic, holds at position exactly when some satisfies and every position with satisfies . The witness must exist. The case imposes no condition on .
The linear temporal logic operator , true at position of a path in a transition system exactly when is true at position . Thus tests two positions ahead.
Articles by others on the same topic
Temporal logic is a formal system used in fields such as computer science, artificial intelligence, and mathematics to reason about propositions qualified in terms of time. It extends classical logic by incorporating temporal aspects, allowing reasoning about the order and timing of events. There are two main types of temporal logic: 1. **Linear Time Temporal Logic (LTL)**: In LTL, time is viewed as a linear progression, where every moment in time has a unique successor.