temporal logic


Also found in: Dictionary, Wikipedia.

temporal logic

(logic)
An extension of predicate calculus which includes notation for arguing about *when* statements are true. Time is discrete and extends indefinitely into the future. Three prefix operators, represented by a circle, square and diamond mean "is true at the next time instant", "is true from now on" and "is eventually true". x U y means x is true until y is true. x P y means x precedes y.

There are two types of formula: "state formulae" about things true at one point in time, and "path formulae" about things true for a sequence of steps. An example of a path formula is "x U y", and example of a state formula is "next x" or a simple atomic formula such at "waiting".

"true until" in this context means that a state formula holds at every point in time up to a point when another formula holds. "x U y" is the "strong until" and implies that there is a time when y is true. "x W y" is the "weak until" in which it is not necessary that y holds eventually.

There are two types of temporal logic used: branching time and linear time. The basic propositional temporal logic cannot differentiate between the two, though. Linear time considers only one possible future, in branching time you have several alternative futures. In branching temporal logic you have the extra operators "A" (for "all futures") and "E" (for "some future"). For example, "A(work U go_home)" means "I will work until I go home" and "E(work U go_home)" means "I may work until I go home".
This article is provided by FOLDOC - Free Online Dictionary of Computing (foldoc.org)
References in periodicals archive ?
In coverage-based testing, the test purpose is specified in temporal logic and then converted to what is called a never-claim by negation; to assert that the test purpose never becomes true.
Pomarlan, "Visibility-based planners for mobile robots capable to handle path existence queries in temporal logic," Advances In Electrical and Computer Engineering, pp 55-64, Feb.
In order to describe the different temporal properties, some different temporal logic types have been proposed.
These artworks focus on the inherent temporal logic of reading as a process of digital mediation.
Temporal Logic formulae are adopted for the formalization of liveness requirements.
Foucauldian scholars will find Lachmann's proposition that historical sociology must view historical transformations according to this temporal logic unconvincing.
Formal linear temporal logic language is used to present the whole tasks of the robot system, which is almost the same with the natural language in structure.
Fuzzy temporal logic based passenger flow forecast model (FTLPFFM) is proposed in this paper.
These requirements are expressed as formal properties, such as temporal logic formulas.
Morrison deals with the law and sacrifice as a burnt offering, and in this we also see the temporal logic of Morrison's modernist apocalyptic.
In Rueda and Valencia (2002) some musical properties were formally proved using the linear temporal logic of NTCC.

Full browser ?