词条 | Linear temporal logic | |||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
释义 |
In logic, linear temporal logic or linear-time temporal logic[1][2] (LTL) is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths, e.g., a condition will eventually be true, a condition will be true until another fact becomes true, etc. It is a fragment of the more complex CTL*, which additionally allows branching time and quantifiers. Subsequently LTL is sometimes called propositional temporal logic, abbreviated PTL.[3] Linear temporal logic (LTL) is a fragment of S1S (monadic second-order logic of one successor).[4] LTL was first proposed for the formal verification of computer programs by Amir Pnueli in 1977.[5] SyntaxLTL is built up from a finite set of propositional variables AP, the logical operators ¬ and ∨, and the temporal modal operators X (some literature uses O or N) and U. Formally, the set of LTL formulas over AP is inductively defined as follows:
X is read as next and U is read as until. Other than these fundamental operators, there are additional logical and temporal operators defined in terms of the fundamental operators to write LTL formulas succinctly. The additional logical operators are ∧, →, ↔, true, and false. Following are the additional temporal operators.
SemanticsAn LTL formula can be satisfied by an infinite sequence of truth evaluations of variables in AP. These sequences can be viewed as a word on a path of a Kripke structure (an ω-word over alphabet 2AP). Let w = a0,a1,a2,... be such an ω-word. Let w(i) = ai. Let wi = ai,ai+1,..., which is a suffix of w. Formally, the satisfaction relation between a word and an LTL formula is defined as follows:
We say an ω-word w satisfies an LTL formula ψ when w ψ. The ω-language L(ψ) defined by ψ is {w | w ψ}, which is the set of ω-words that satisfy ψ. A formula ψ is satisfiable if there exist an ω-word w such that w ψ. A formula ψ is valid if for each ω-word w over alphabet 2AP, w ψ. The additional logical operators are defined as follows:
The additional temporal operators R, F, and G are defined as follows:
Weak until and strong releaseSome 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).[7] It is sometimes useful since both U and R can be defined in terms of the weak until:
The strong release binary operator, denoted M, is the dual of weak until. It is defined similar to the until operator, so that the release condition has to hold at some point. Therefore, it is stronger than the release operator.
The semantics for the temporal operators are pictorially presented as follows.
EquivalencesLet φ, ψ, and ρ be LTL formulas. The following tables list some of the useful equivalences which extend standard equivalences among the usual logical operators.
Negation normal formAll the formulas of LTL can be transformed into negation normal form, where
Using the above equivalences for negation propagation, it is possible to derive the normal form. This normal form allows R, true, false, and ∧ to appear in the formula, which are not fundamental operators of LTL. Note that the transformation to the negation normal form does not blow up the size of the formula. This normal form is useful in translation from LTL to Büchi automaton. Relations with other logicsLTL can be shown to be equivalent to the monadic first-order logic of order, FO[<]—a result known as Kamp's theorem—[8] or equivalently star-free languages.[9] Computation tree logic (CTL) and linear temporal logic (LTL) are both a subset of CTL*, but are incomparable. For example,
However, a subset of CTL* exists that is a proper superset of both CTL and LTL. Applications
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 another one that is equivalent to the negation of the property (cf. Linear temporal logic to Büchi automaton).{{Clarify|reason=Under what equivalence(s)?|date=February 2014}} The intersection of the two non-deterministic Büchi automata is empty if the model satisfies the property.[10]
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), while liveness properties state that something good keeps happening (GF or GF). 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.
One of the applications of linear temporal logic is the specification of preferences in the Planning Domain Definition Language for the purpose of preference-based planning.{{citation needed|date=January 2011}} See also{{Commons category|Linear temporal logic}}
References1. ^[https://books.google.com/books?id=eUggAwAAQBAJ&printsec=frontcover#v=onepage&q=%22temporal%20logic%22&f=false Logic in Computer Science: Modelling and Reasoning about Systems]: page 175 2. ^Linear-time Temporal Logic 3. ^{{cite book|author1=Dov M. Gabbay|author2= A. Kurucz|author3= F. Wolter|author4= M. Zakharyaschev|title=Many-dimensional modal logics: theory and applications|url=https://books.google.com/books?id=P8jZwiExZYEC&pg=PA46|year=2003|publisher=Elsevier|isbn=978-0-444-50826-3|page=46}} 4. ^{{Cite web|url=https://www.cs.ox.ac.uk/people/luke.ong/personal/talks/s1s.pdf|title=Automata, Logic and Games: Theory and Application, 1. Buchi Automata and S1S|last=Ong|first=Luke|date=|website=|publication-place=Oxford University|access-date=}} 5. ^Amir Pnueli, The temporal logic of programs. Proceedings of the 18th Annual Symposium on Foundations of Computer Science (FOCS), 1977, 46–57. {{doi|10.1109/SFCS.1977.32}} 6. ^Sec. 5.1 of Christel Baier and Joost-Pieter Katoen, Principles of Model Checking, MIT Press {{cite web|url=http://mitpress.mit.edu/catalog/item/default.asp?tid%3D11481%26ttype%3D2 |title=Archived copy |accessdate=2011-05-17 |deadurl=yes |archiveurl=https://web.archive.org/web/20101204043002/http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=11481 |archivedate=2010-12-04 |df= }} 7. ^Sec. 5.1.5 "Weak Until, Release, and Positive Normal Form" of Principles of Model Checking. 8. ^{{cite book|url=https://books.google.com/books?id=TLpcI2axv8kC&pg=PA22 |title=Automata, Languages and Programming: 37th International Colloquium, ICALP ... - Google Books |publisher=Books.google.com |date=2010-06-30 |accessdate=2014-07-30}} 9. ^{{cite book|editor1=Orna Grumberg |editor2=Helmut Veith |title=25 years of model checking: history, achievements, perspectives|year=2008|publisher=Springer|isbn=978-3-540-69849-4|chapter=From Church and Prior to PSL|author=Moshe Y. Vardi}} preprint 10. ^Moshe Y. Vardi. An Automata-Theoretic Approach to Linear Temporal Logic. Proceedings of the 8th Banff Higher Order Workshop (Banff'94). Lecture Notes in Computer Science, vol. 1043, pp. 238--266, Springer-Verlag, 1996. {{ISBN|3-540-60915-6}}.
2 : Computer-related introductions in 1977|Temporal logic |
|||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识,基本涵盖了大多数领域的百科知识,是一部内容自由、开放的电子版国际百科全书。