Temporal logic
From The Art and Popular Culture Encyclopedia
|
Related e |
|
Featured: |
In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time (for example, "I am always hungry", "I will eventually be hungry", or "I will be hungry until I eat something"). It is sometimes also used to refer to tense logic, a modal logic-based system of temporal logic introduced by Arthur Prior in the late 1950s, with important contributions by Hans Kamp. It has been further developed by computer scientists, notably Amir Pnueli, and logicians.
Temporal logic has found an important application in formal verification, where it is used to state requirements of hardware or software systems. For instance, one may wish to say that whenever a request is made, access to a resource is eventually granted, but it is never granted to two requestors simultaneously. Such a statement can conveniently be expressed in a temporal logic.
See also
- HPO formalism
- Kripke structure
- Automata theory
- Chomsky grammar
- State transition system
- Duration calculus (DC)
- Hybrid logic
- Temporal logic in finite-state verification
- Temporal logic of actions (TLA)
- Important publications in formal verification (including the use of temporal logic in formal verification)
- Reo Coordination Language
- Modal logic
- Research Materials: Max Planck Society Archive
