temporal logic
In plain wordsA logic for statements about time — 'eventually the light turns green', 'the door is never open while the train moves' — used to specify and check how systems must behave over time.
A family of modal logics for reasoning about how the truth of propositions changes over time, using operators such as G ('always'), F ('eventually'), X ('next') and U ('until'). Linear temporal logic (LTL) describes individual execution traces; computation tree logic (CTL) quantifies over branching futures; metric and signal temporal logics add real-time bounds. Temporal logic is the standard specification language of model checking and formal verificationformal verification, n.: Using mathematics, not just testing, to prove that a computer system always behaves as specified — for example, that a chip never adds wrongly or that a program can never crash in a particular way., expressing safety properties (nothing bad ever happens) and liveness properties (something good eventually happens). In AI it specifies temporally extended goals for automated planningautomated planning, n.: The branch of AI that works out a sequence of actions to reach a goal, such as the steps a robot must take to assemble a part, from descriptions of what each action needs and what it changes. (as in PDDL3), shapes or constrains reinforcement learningreinforcement learning, n.: A way of teaching a computer program by trial and error: it tries actions, earns points for good results and penalties for bad ones, and gradually learns which choices pay off over time. agents through automata compiled from formulas (reward machines, shielding), and defines runtime monitors for autonomous systems and agentsAI agent, n.: An AI system that does not just answer but acts: given a goal, it decides on steps, uses tools such as a browser or code editor, checks the results and keeps going until the job is done..
The safety requirement in temporal logic reads G(braking → F stopped): whenever the train brakes, it eventually stops.
Origin
The philosopher Arthur Prior developed tense logic in the 1950s (Time and Modality, 1957). Amir Pnueli introduced temporal logic into program verification in 1977, work recognized by the 1996 Turing Award, and Edmund Clarke and E. Allen Emerson defined CTL in 1981.
Related
- formal verificationformal verification, n.: Using mathematics, not just testing, to prove that a computer system always behaves as specified — for example, that a chip never adds wrongly or that a program can never crash in a particular way.
- automated planningautomated planning, n.: The branch of AI that works out a sequence of actions to reach a goal, such as the steps a robot must take to assemble a part, from descriptions of what each action needs and what it changes.
- first-order logicfirst-order logic, n.: A precise formal language for statements about objects and their relations, using 'for all' and 'there exists', such as 'every person has a mother'. It is the standard logic of mathematics and of classic AI.
- reinforcement learningreinforcement learning, n.: A way of teaching a computer program by trial and error: it tries actions, earns points for good results and penalties for bad ones, and gradually learns which choices pay off over time.
- situation calculussituation calculus, n.: A logical language for describing how the world changes as actions happen, so that a program can work out what will be true after any sequence of actions.
- Planning Domain Definition LanguagePlanning Domain Definition Language, prop. n.: A standard computer language for describing planning problems — the available actions, the starting situation and the goal — so that any automated planner can read and solve them.
Sources
- Prior, A. N. (1957). Time and Modality. Oxford University Press.
- Pnueli, A. (1977). The Temporal Logic of Programs. Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, 46–57.