NationMaster - Encyclopedia: Linear temporal logic

Linear temporal logic (LTL) is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths such as that a condition will eventually be true, that a condition will be true until another fact becomes true, etc. In formal logic, a modal logic is any logic for handling modalities: concepts like possibility, existence, and necessity. ... In logic, the term temporal logic is used to describe any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time. ... In graph theory, a path in a graph is a sequence of vertices such that from each of its vertices there is an edge to the next vertex in the sequence. ...

1 Syntax
2 Semantics
3 Nonstandard connectives
4 Important properties
5 Relations with other logics
6 Automata theoretic Linear temporal logic model checking
7 See also
8 External links

Syntax

LTL is built up from a set of proposition variables $p 1, p 2,...$ , the usual logic connectives $neg,or,and,rightarrow$ and the following temporal modal operators: In mathematical logic, a propositional variable (also called a sentential variable) is a variable which can either be true or false. ... For alternate uses of time, see Time (disambiguation) or see TIME (magazine). ... A modal operator is a logical connective, in the language of a modal logic, which forms propositions from propositions. ...

X for next;
G for always (globally);
F for eventually (in the future);
U for until;
R for release.

The first three operators are unary, so that X $φ$ is a well-formed formula whenever $φ$ is a well-formed formula. The last two operators are binary, so that $φ$ U $ψ$ is a well-formed formula whenever $φ$ and $ψ$ are well-formed formulas. In logic, WFF is an abbreviation for well-formed formula. ...

Semantics

An LTL formula can be evaluated over an infinite sequence of truth evaluations and a position on that path. An LTL formula is satisfied by a path if and only if it is satisfied for position 0 on that path. The semantics for the modal operators is given as follows.

Textual	Symbolic	Explanation	Diagram
Unary operators:
X $φ$	$circ phi$	neXt: $φ$ has to hold at the next state. (N is used synonymously.)
G $φ$	$Box phi$	Globally: $φ$ has to hold on the entire subsequent path.
F $φ$	$Diamond phi$	Finally: $φ$ eventually has to hold (somewhere on the subsequent path).
Binary operators:
$ψ$ U $φ$	$psimathcal{U}phi$	Until: $φ$ holds at the current or a future position, and $ψ$ has to hold until that position. At that position $ψ$ does not have to hold any more.
$ψ$ R $φ$	$psimathcal{R}phi$	Release: $ψ$ releases $φ$ if $φ$ is true until the first position in which $ψ$ is true (or forever if such a position does not exist).	In mathematics, a unary operation is an operation with only one operand. ... Image File history File links Ltlnext. ... Image File history File links Ltlalways. ... Image File history File links Ltlevently. ... In mathematics, a binary operation, or binary operator, is a calculation involving two input quantities and one kind of a specific operation. ... Image File history File links Ltluntil. ... Image File history File links Ltlrelease1. ... Image File history File links Ltlrelease2. ...

One can reduce to two of those operators since the following is always satisfied:

F $φ$ = true U $φ$
G $φ$ = false R $φ$ = $neg$ F $neg$ $φ$
$ψ$ R $φ$ = $neg$ ( $neg$ $ψ$ U $neg$ $φ$ )

Nonstandard connectives

Some authors also define a weak until binary operator, denoted W, with semantics similar to that of the until operator but the stop condition is not required to occur (similar to release). It is sometimes useful since both U and R can be defined in terms of the weak until:

$ψ$ U $φ$ = F $φ$ $land$ ( $ψ$ W $φ$ )
$ψ$ R $φ$ = $φ$ W ( $ψ$ $land$ $φ$ )

Important properties

There are two main types of properties that can be expressed using linear temporal logic: safety properties usually state that something bad never happens (G $neg$ $φ$ ), while liveness properties state that something good keeps happening (GF $ψ$ or G $(phi rightarrow$ F $ψ)$ ). More generally: Safety properties are those for which every counterexample has a finite prefix such that, however it is extended to an infinite path, it is still a counterexample. For liveness properties, on the other hand, every finite prefix of a counterexample can be extended to an infinite path that satisfies the formula. In logic, and especially in its applications to mathematics and philosophy, a counterexample is an exception to a proposed general rule, i. ...

Relations with other logics

Linear temporal logic (LTL) is a subset of CTL*.

LTL can be shown to be equivalent to the first-order logic over one successor and the smaller relation, FO[S,<] as well as star-free regular expressions or deterministic finite automata with loop complexity 0. First-order logic (FOL) is a universal language in symbolic science, and is in use everyday by mathematicians, philosophers, linguists, computer scientists and practitioners of artificial intelligence. ... Look up Relation in Wiktionary, the free dictionary In mathematics, a relation is a generalization of arithmetic relations, such as = and <, which occur in statements, such as 5 < 6 or 2 + 2 = 4. See relation (mathematics), binary relation (of set theory and logic) and relational algebra. ... A regular language is said to be star-free if it can be described by a regular expression constructed from the letters of the alphabet, the empty set symbol, boolean operators and concatenation but no Kleene star. ... In computing, a regular expression is a string that is used to describe or match a set of strings, according to certain syntax rules. ... In the theory of computation, a deterministic finite state machine or deterministic finite automaton (DFA) is a finite state machine where for each pair of state and input symbol there is one and only one transition to a next state. ...

Automata theoretic Linear temporal logic model checking

An important way to model check is to express desired properties (such as the ones described above) using LTL operators and actually check if the model satisfies this property. One technique is to obtain a Büchi automaton that is "equivalent" to the model and one that is "equivalent" to the property. Obtain a synchronized product of the two non-deterministic Büchi automata and then do an emptiness check of this product. Another possibility is to develop the negated version of the same property and make sure that the product is not empty. A BÃ¼chi automaton is the extension of a finite state automaton to infinite inputs. ...

External links

A presentation of LTL
Linear-Time Temporal Logic and Büchi Automata
Teaching slides of professor Alessandro Artale at the Free University of Bozen-Bolzano

Category: Logic The Free University of Bolzano (Italian: Libera UniversitÃ di Bolzano, German: Freie UniversitÃ¤t Bozen) is a university located in Bolzano, Italy. ...

COMMENTARY

Share your thoughts, questions and commentary here

Want to know more?
Search encyclopedia, statistics and forums:

Feeds | Contact
The Wikipedia article included on this page is licensed under the GFDL.
Images may be subject to relevant owners' copyright.
All other elements are (c) copyright NationMaster.com 2003-5. All Rights Reserved.
Usage implies agreement with terms.

Contents

Syntax GA_googleFillSlot("encyclopedia_square");