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".
References in periodicals archive ?
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.
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.
The basic claim of this paradigm is that these rhythmic components represent different temporal logics, or temporalities, what I call cyclical, centroidal, linear, and relative time.
Thus, within the temporal logic of Ts'ui Pen's novel, which privileges a present in which every possibility necessarily actualizes itself, then all possible futures are in fact necessary and the decision can make no difference.
Accordingly, the reader will meet logics that support individual agent specification--intention logic and BDI logic--and will also see logics of cooperative ability--coalition logic and alternating-time temporal logic.
Some formal methods such as Communicating Sequential Processes [2], a Calculus of Communicating Systems [3], Statecharts [4], Temporal logic [5, 6, 7], and I/O automata [8] focus on specifying the behavior of concurrent systems, while others such as Larch [9], Z [10], and VDM [11] focus on specifying the behavior of sequential systems.
Suddenly, the film cuts to a medium close-up of Kin ski's face as she confronts an unseen assailant; this point of view endeavors to make the viewer complicit with (or an extension of) the tormentor (and, in turn, the artist), and foreshadows a proliferation of intercepting that shreds temporal logic and at once splinters and compresses an already claustrophobic space of representation (the bedroom or hotel unit).
Marsden, Alan (2007), "Timing in Music and Modal Temporal Logic," Journal of Mathematics and Music 1(3): 173-189.
Promela model has no assertions or temporal logic LTL formula.
Several of the papers propose extensions to metric interval temporal logic, linear temporal logic, and computation tree logic.
Going into such logic, the present work shows the related epistemological features, detailing the origin and evolution of temporal logic from the first concepts about logics introduced by Aristotle to its conception as a key tool for verifying critical software systems.