In this thesis we get acquainted with a type of temporal logic that has a linear model of time. Time is modeled as a set of sequences of moments isomorphic with \(\mathbb{N}\). Roughly, we could describe LTL as classical propositional logic with the ability to express time. In LTL time is expressed through temporal operators X, F, W, U, G and R. Another peculiarity of LTL is that all of the temporal operators only refer to the future. In LTL we cannot refer to the past. A more pronounced difference between LTL and classical propostional logic is in the way formulas are interpreted. In LTL formulas are interpreted with the use of transitional systems, which are also called models. More precisely, LTL formulas are interpreted on sequences of states of a transitional system, that are labeled with propostional variables. Such sequences are called paths. If a state is labled with a certain variable, then it means that the propositional variable is true in that state. In other words, the static notion of truth in classical propostitional logic is replaced with a dynamic one, in which the formulas may change their truth values as the system evolves from state to state. As we already mentioned, in LTL there are no operators with which we could refer to the past. By studying an expansion of LTL (so called PLTL), that has operators that refer to the past, we see that by adding these operators we don't get anything as far as expressiveness is concerned, within the context of initial equivalence. So, for every PLTL formula \(\Phi\) there is an LTL formula that's equivalent to \(\Phi\) in the initial moment. This result can be easily deduced by using Gabbay's separation theorem. Separation is a fundamental concept for temporal logics, which was first introduced by Gabbay. Roughly, a temporal logic has the separation property if for every formula of that logic is an equivalent boolean combination of a future, past and present formula. By Gabbay's separation theorem we know that PLTL has the separation property. There are various results that describe the complexity of transforming PLTL formulas into initially equivalent LTL formulas and the difference in size between PLTL formulas and the shortest initally equivalent LTL formulas (this difference is also called the succinctness gap). One of the newer results is a characterization that we get by observing a strict subset of PLTL formulas that are called anchored PLTL formulas. It is shown that the complexity of the transformation is elementary if and only if the complexity of anchored PLTL separation is elementary. Also, the succinctness gap between LTL and PLTL is elementary if and only if the succinctness gap between anchored PLTL and seperated anchored PLTL is elementary. Linear temporal logic has shown to be a suitable logic for formal verification of systems. Formal verification is very important in the industry for determining the correctness of, so called, critical hardware \(\backslash\) software systems. There are various formal verification methods. One of the more popular for use is model checking. For a model \(\mathcal{M}\), initial state \(s_{0}\) and an LTL formula \(\Phi\), LTL model checking comes down to determining whether the formula \(\Phi\) is true on all paths beggining at \(s_{0}\) in model \(\mathcal{M}\). The models in formal verification represent abstractions of systems that need to be verified. With LTL formulas we express properties of the system that we want to check. There are different algorithms for model checking. The type of the property that we want to check has a significant influence on the way we shape the process of verification and on the selection of the algorithm for model checking. Within the context of models, properties are sets of paths. We distinguish different types of properties, some of which are safety properties, liveness properties, fairness... Because the type of the property influences the way systems are verified, it is important to determine the type of the property we want to check. For this purpose, characterization of properties, that is syntactic characterizations of LTL formulas that express a certain type of property, can be very helpful. In section 2.1. we give characterizations of different types of properties. Also, in this section we show that LTL is closed for topological closure, that is for every property that we can express with an LTL formula the smallest safety property that contains it can also be expressed with an LTL formula. Corollarily we get that LTL admits the saftey-liveness decomposition, which means that every LTL formula is equivalent to a conjunction of a safety formula and a liveness formula. The main literature for this thesis was Ben-Ari's book ([3 ]), but a significant contribution to the content of the thesis was also drawn from Grgur Petric-Maretic's articles ([18 ],[19 ]), A.P. Sistla's article [ 22 ] and the book [13 ] written by authors M.Huth and M.Ryan.