Temporal normal form for Linear Temporal Logic formulae 1

1 Introduction

Model checking is a verification technique that automatically examines all relevant system states to check whether the system model satisfies the desired properties. Since it was proposed independently by Clarke and Emerson [3] as well as Queille and Sifakis [15], this breakthrough was the first step towards the automated verification of concurrent programs. Over the last three decades, model checking has received a lot of attention and becomes a subject of rapidly growing research community [1, 12]. Given a model TS of the system and a specification φ of the property to be considered, model checking can systematically checks the validity of the property in the model. Here the model TS is a transition system [1, 9], and the specification φ is typically represented in temporal logic such as LTL (Linear Temporal Logic) [1, 12], an extension of propositional or predicate logic by modalities that permit to referral to the infinite behavior of a reactive system.

Temporal logics and related modal logics [2, 17] have been studied in ancient times in different areas such as philosophy. Their application to verifying complex computer systems was proposed by Pnueli and greatly developed recently [6, 14]. In this paper, we will focus our attention on LTL, a temporal logic that is based on a linear-time perspective [1, 12]. First, we introduce the concepts of characters as well as the least characters for LTL formulae and form the bounded case for LTL formulae, i.e., LTL _n formulae. Meanwhile, we prove that all LTL _n formulae have characters as well as the least characters and show that those LTL formulae with characters have good properties. That is, they can be equivalently written in a simple form without containing the logical connective ⊔, and more importantly they can always be checked within finite steps during model checking even in some cases when the underlying transition system contains infinite states. What is more, the class of LTL formulae with characters can be characterized by full LTL _n , which provides reasonable intuition for the notion of characters. After that, we propose TDNF (temporal disjunctive normal form) and TCNF (temporal conjunctive normal form) for LTL as well as LTL _n formulae and obtain a similar result as in classical propositional logic [11, 18]: The class of TDNF (TCNF) formulae is as expressive as full LTL _n . Besides, a necessary and sufficient condition is given in which an LTL formula has an equivalent TDNF (TCNF) formula.

2 Preliminaries

In this section, we briefly overview some preliminaries that we need. For more details, please see [1, 4].

Definition 2.1. [1] A transition system TS is a tuple (S, Act, → , I, AP, L), where

S is a set of states,

For convenience, we write s → s′ instead of (s, α, s′)∈ → when there is no confusion. s′ is called a successor of s, and Post (s) denotes the set of all successors of s. A path π of TS is a non-empty sequence of states s₀s₁s₂⋯ such that s _i  ∈ Post (s_i-1) for all i ≥ 1. Paths (TS) denotes the set of all initial, infinite paths of TS. For path π = s₀s₁s₂⋯ of TS, the trace of π is defined as trace ( π ) = L ( s 0 ) L ( s 1 ) L ( s 2 ) ⋯ ( ∈ ( 2 AP ) ω ) , and Traces ( TS ) = { trace ( π ) | π ∈ Paths ( TS ) } .

Definition 2.2. [1] LTL formulae over AP are formed according to the following grammar: φ : : = true | a | ¬ φ | φ 1 ∧ φ 2 | ○ φ | φ 1 ⊔ φ 2 where a ∈ AP. Other connectives can be derived as follows: false = ¬ ture , φ 1 ∨ φ 2 = ¬ ( ¬ φ 1 ∧ ¬ φ 2 ) , φ 1 → φ 2 = ¬ φ 1 ∨ φ 2 , ♦ φ = true ⊔ φ , □ φ = ¬ ♦ ¬ φ , ○ k φ = ○ k - 1 ( ○ φ ) , k ≥ 1 , ○ 0 φ = φ .

The precedence order on the operators is as follows. The unary operators ¬, ○ , ♦ and □ bind stronger than the binary ones, and ⊔ takes precedence over ∧, ∨ and →.

Definition 2.3. [1] Let φ be an LTL formula over AP. Define Words ( φ ) = { σ ∈ ( 2 AP ) ω ∣ σ ⊨ φ }(1) where ⊨ is the smallest relation with the following properties:

σ ⊨ true,

For path π of TS, define π ⊨ φ iff trace ( π ) ⊨ φ , and TS ⊨ φ iff Traces ( TS ) ⊆ Words ( φ ) , i.e., π ⊨ φ holds for every π ∈ Paths (TS).

Corollary 2.4. Let φ, φ₁, φ₂ be LTL formulae over AP and σ ∈ (2 ^AP )  ^ω . Then

Words (true) = (2 ^AP )  ^ω ,

Definition 2.5. [1] LTL formulae φ, ψ are equivalent, denoted φ ≡ ψ, if Words (φ) = Words (ψ).

Let φ be an LTL formula. If Words (φ) = (2 ^AP )  ^ω , then it is easily seen that φ ≡ true, and we call φ a tautology in this sense. Similarly, if Words (φ) =∅, then φ ≡ false, and we call φ a contradiction.

Definition 3.1. Let σ ∈ E ⊆ (2 ^AP )  ^ω . We say that σ is eventually free in E if there exists m ≥ 0 such thatσ′ ∈ E holds for every σ′ ∈ (2 ^AP )  ^ω with σ′ [k] = σ [k] (k = 0, 1, ⋯ , m - 1). In this case, we also say that σ is m-free in E.

Obviously, if σ is m-free in E, then it is n-free in E for all n ≥ m.

Definition 3.2. Let φ be an LTL formula with Words (φ)≠ ∅. If there exists k ≥ 0 such that σ is k-free in Words(φ) for every σ ∈ Words (φ), then k is called a character of φ. Furthermore, if k is the least, then we say that k is the least character of φ, denoted Ch (φ) = k.

Obviously, if k is a character of φ, then m is also a character of φ for every m ≥ k, and Ch (φ) exists in this case.

For a tautology φ, since Words (φ) = (2 ^AP )  ^ω , we can easily get Ch (φ) =0. Note that Definition 3.2 is not suitable for any contradiction ψ since Words(ψ) =∅, however, we can still reach an agreement and let Ch (ψ) =0.

Example 3.3. Let a, b ∈ AP. Since Words(a ∧ b)= {σ ∈ (2 ^AP )  ^ω  ∣ a, b ∈ σ [0]}, we can obtain that Ch (a ∧ b) =1. Similarly, Ch (¬ a) =1, Ch (○ a) =2. However, a ⊔ b does not have any character, since for σ = {a}  ^k  {b}  ^ω (k > 0), σ′ = {a}  ^ω , we have σ [j] = σ′ [j] (j = 0, 1, ⋯ , k - 1), σ∈Words(a ⊔ b), but σ′∉Words(a ⊔ b) for arbitrary natural number k > 0. Similarly, one can prove that there are many other LTL formulae, such as □a, ¬c ∧ (○ b ⊔ a) and □ (b → ○ d) etc., having no characters.

From Example 3.3, it is not true that each LTL formula has a character. To make up this situation, we introduce a binary connective ⊔^≤n as the bounded form for ⊔, and also ♦^≤n, □^≤n corresponding to ♦, □ respectively. Here for every σ ∈ (2 ^AP )  ^ω , σ ⊨ φ₁ ⊔ ^≤nφ₂ iff ∃j with 0 ≤ j ≤ n s.t. σ [j . . .] ⊨ φ₂ and σ [i . . .] ⊨ φ₁ (0 ≤ i < j). Moreover, by substituting ⊔^≤n for each ⊔ in LTL formulae, we obtain LTL _n formulae, the bounded form for LTL. In the sequel, we can see that every LTL _n formula has a character (also the least character). To prove this, we need a lemma whose proof is simple and consequently omitted.

Lemma 3.4. Let φ, ψ be LTL or LTL _n formulae. Ifφ ≡ ψ, then Ch (φ) = Ch (ψ).

Proposition 3.5. Each LTL _n formula has a character as well as the least character. Furthermore, for a contingent formula (i.e., neither a tautology nor a contradiction) φ, the upper bound of Ch (φ) can be computed by induction in the following way:

Ch (a) =1 for every a ∈ AP;

Proof. For a tautology or a contradiction, we have already known that the least character is 0. Let φ be a contingent formula. In what follows we prove by induction on the complexity of φ.

(i) Let φ = a where a ∈ AP. Then σ∈Words(φ) iff a ∈ σ [0]. Thus each k ≥ 1 is a character of φ, and consequently Ch (φ) =1.

(ii) Let φ = ¬ ψ and k be a character of ψ. Since φ is a contingent formula, so does ψ, thus k > 0. Arbitrarily choose σ ∈ (2 ^AP )  ^ω . Suppose that there exists σ′∈Words(φ) such that σ′ [i] = σ [i] for i = 0, 1, ⋯ , k - 1, then it can be obtained that σ∈Words(φ). Since otherwise, if σ∉Words(φ), then σ ∈ (2 ^AP )  ^ω -Words(φ)=Words(ψ). Consequently σ′∈Words(ψ) by Definition 3.2, which contradicts with σ′∈Words(φ)=(2 ^AP )  ^ω -Words(ψ). Therefore, k is a character of φ, and Ch (φ) exists. Furthermore, it is easy to get Ch (φ) = Ch (ψ).

(iii) Let φ = φ₁ ∧ φ₂ and k₁, k₂ be characters of φ₁, φ₂ respectively. Since Words (φ) = Words (φ₁) ∩ Words (φ₂), it can be similarly obtained that k = max {k₁, k₂} is a character of φ, thus Ch (φ) ≤ max {Ch (φ₁) , Ch (φ₂)}.

(iv) Let φ = ○ ψ and k be a character of ψ. Then we can similarly prove that k + 1 is a character of φ, and Ch (φ) = Ch (ψ) +1.

(v) Let φ = φ₁ ⊔ ^≤nφ₂, k₁, k₂ be characters of φ₁, φ₂ respectively, and k = n + max {k₁ - 1, k₂}. Arbitrarily choose σ ∈ (2 ^AP )  ^ω , and suppose that there exists σ′∈Words(φ) such that σ′ [m] = σ [m] for m = 0, 1, ⋯ , k - 1. Since σ′∈Words(φ), there exists j with 0 ≤ j ≤ n such that σ′ [j . . .]∈Words(φ₂) and σ′ [i . . .]∈Words(φ₁) for 0 ≤ i < j. Note thatk - j ≥ k - n ≥ k₂, k - i ≥ k₁, and σ [m] = σ′ [m] holds for all m with i ≤ m < k. Thus σ [j . . .]∈Words(φ₂), σ [i . . .]∈Words(φ₁) for 0 ≤ i < j, and consequently σ∈Words(φ), which proves that k is a character of φ. Thus, Ch (φ) ≤ n + max {Ch (φ₁) -1, Ch (φ₂)}. Furthermore, it is easy to obtain that Ch (φ) = Ch (φ₁) = Ch (φ₂) in case φ₁ ≡ φ₂ by Lemma 3.4.□

Corollary 3.6. Let φ, ψ, φ₁, φ₂ be LTL _n formulae with Ch (φ) >0.

If φ = φ₁ ∨ φ₂ or φ₁ → φ₂, then Ch (φ) ≤ max {Ch (φ₁) , Ch (φ₂)};

Definition 3.7. Let φ be an LTL or LTL _n formula. Define for j = 1, 2, ⋯, Words ( j ) ( φ ) = { σ [ . . . j - 1 ] ∣ σ ∈ Words ( φ ) } .(2)

For an LTL or LTL _n formula φ with Ch (φ) = k, one can easily infer that Words ( φ ) = { δ σ ∣ δ ∈ Words ( k ) ( φ ) , σ ∈ ( 2 AP ) ω }(3) holds by Equations. (1)-(2), where δσ denotes the string concatenation of δ and σ. In this case, if one wants to check whether a σ ∈ (2 ^AP )  ^ω satisfies the formula φ, he (she) only needs to check whether the k-length prefix of σ satisfies φ. In another words, the set Words(φ) is completely decided by Words ^(k)  (φ). As a result, the formula φ can be checked as a specification within finite steps during model checking, that is, for any given transition system TS, we can always check the validity of φ in TS within finite steps. In fact, in order to check whether TS ⊨ φ holds, we only need to check whether the k-length prefix of each trace σ ∈ Traces (TS) satisfies φ. To be more in detail, we suppose that TS = (S, Act, → , I, AP, L) has finite initial states, i.e., |I| is finite, and each state has finite successors, i.e., |Post (s) | ≤ t holds for some t ∈ N and all s ∈ S. In this case, it is easy to obtain that there are no more than M = |I| · t^k-1 many k-length traces (i.e., k-length prefix of traces) of TS. According to above analysis, we need to check whether each k-length trace of TS belongs to Words^(k) (φ), and after M times of computation we would check out whether TS ⊨ φ holds. During this procedure, the key issue lies in that we only need to consider those states no more than k steps from some initial state in TS, instead of considering all states (as some LTL formulae, such as a ⊔ b, do). To conclude these, when a specification φ has a character, we are lucky that the procedure of model checking would be finished within finite steps even in some cases when TS contains infinite states. Under this circumstance, the original model checking would be greatly simplified since the state-space explosion problem is avoided to some extent.

Proposition 3.8. Let φ be an LTL formula. If Ch (φ) exists, then φ is equivalent to some LTL formula without containing the logical connective ⊔.

Proof. Let Ch (φ) = k. If k = 0, then φ is a tautology or a contradiction, and the conclusion obviously holds in this case. Suppose k > 0 and |AP| = m. Then Words ^(k)  (φ) is a finite set. Assume that Words ^(k)  (φ) = {δ₁, ⋯ , δ _t } ≠ ∅, where δ _i  ∈ (2 ^AP )  ^k (i = 1, ⋯ , t) and t ≤ 2 ^m k. Define ψ = ∨ i = 1 t ( ψ 0 ( i ) ∧ ○ ψ 1 ( i ) ∧ ⋯ ∧ ○ k - 1 ψ k - 1 ( i ) ) ,(4) where ψ j ( i ) = [ ( ∧ a ∈ δ i [ j ] a ) ∧ ( ∧ b ∈ AP - δ i [ j ] ¬ b ) ] for j = 0, ⋯ , k - 1 and i = 1, ⋯ , t . Obviously, ψ is an LTL formula without containing the logical connective ⊔. In what follows we prove that φ ≡ ψ. Firstly, we can infer from Proposition 3.5 that Ch (ψ) ≤ k. Meanwhile, by Corollary 2.4 and Equation. (3) we obtain that Words ( k ) ( ψ ) = ∪ i = 1 t Words ( k ) ( ψ 0 ( i ) ∧ ○ ψ 1 ( i ) ∧ ⋯ ∧ ○ k - 1 ψ k - 1 ( i ) ) . For every j ∈ {0, ⋯ , k - 1}, i ∈ {1, ⋯ , t} and δ∈Words( k ) ( ψ j ( i ) ), we can easily get that δ [j] = δ _i  [j]. Thus Words ( k ) ( ψ 0 ( i ) ∧ ○ ψ 1 ( i ) ∧ ⋯ ∧ ○ k - 1 ψ k - 1 ( i ) ) = Words ( ψ 0 ( i ) ) ∩ Words ( ○ ψ 1 ( i ) ) ∩ ⋯ ∩ Words ( ○ k - 1 ψ k - 1 ( i ) ) = { δ i } . As a result, Words ( k ) ( ψ ) = { δ 1 , ⋯ , δ t } = Words ( k ) ( φ ) , and Words(φ)=Words(ψ) consequently holds by Equation. (3). By Definition 2.5, we conclude that φ ≡ ψ.

Since an LTL formula without containing ⊔ can also be seen as an LTL _n formula, Proposition 3.8 states that each LTL formula with characters is equivalent to some LTL _n formula. Meanwhile, if an LTL formula φ is equivalent to some LTL _n formula, then by Proposition 3.5 and Lemma 3.4 we can easily infer that Ch (φ) exists. In a word, the following corollary holds.

Corollary 3.9. Let φ be an LTL formula. Then Ch (φ) exists if and only if φ is equivalent to some LTL _n formula.

Corollary 3.9 states that the class of LTL formulae with characters is as expressive as full LTL _n . In another words, they can be characterized by LTL _n formulae, which provides reasonable intuition for the notion of characters.

Example 4.1. Let a, b ∈ AP. Then we can get Ch (a ∧ ○ b) =2, and a ∧ ○ b ≡ [ a ∨ ○ ( a ∧ ¬ a ) ] ∧ [ ( a ∧ ¬ a ) ∨ ○ b ] .

Similarly, Ch (a ⊔ ^≤2b) =3, and a ⊔ ≤ 2 b ≡ b ∨ ( a ∧ ○ b ) ∨ ( a ∧ ○ a ∧ ○ 2 b ) ≡ [ b ∧ ○ ( a ∨ ¬ a ) ∧ ○ 2 ( a ∨ ¬ a ) ] ∨ [ a ∧ ○ b ∧ ○ 2 ( a ∨ ¬ a ) ] ∨ ( a ∧ ○ a ∧ ○ 2 b ) .

It can be seen that the two LTL _n formulae in Example 4.1 can be equivalently written in a special form similarly to disjunctive (conjunctive) normal form in classical propositional logic (see [11, 18] in detail). More generally, we give the following definition.

Definition 4.2. Let φ be an LTL or LTL _n formula. φ is said to be in temporal disjunctive normal form (TDNF for short) and in temporal conjunctive normal form (TCNF for short) with order k, respectively, if φ has the respective forms ( A 10 ∧ ○ A 11 ∧ ⋯ ∧ ○ k A 1 k ) ∨ ⋯ ∨ ( A t 0 ∧ ○ A t 1 ∧ ⋯ ∧ ○ k A tk )(5) and ( A 10 ∨ ○ A 11 ∨ ⋯ ∨ ○ k A 1 k ) ∧ ⋯ ∧ ( A t 0 ∨ ○ A t 1 ∨ ⋯ ∨ ○ k A tk )(6) where A _ij (i = 1, ⋯ , t ; j = 0, 1, ⋯ , k) are propositional formulae over AP, and at least one of A _ik (i = 1, ⋯ , t) is contingent.

Note that each tautology is equivalent to a ∨ ¬ a which can be seen in either TDNF or TCNF, and each contradiction is equivalent to a ∧ ¬ a in either TDNF or TCNF where a ∈ AP. In what follows we obtain a similar result also for contingent formulae. First of all, we need two lemmas.

Lemma 4.3. [1] Let φ, ψ be LTL or LTL _n formulae. Then ¬ ( ○ k φ ) ≡ ○ k ( ¬ φ ) , ○ k ( φ ∧ ψ ) ≡ ○ k φ ∧ ○ k ψ , ○ k ( φ ∨ ψ ) ≡ ○ k φ ∨ ○ k ψ .

By Lemma 4.3 and distributive laws for ∨,∧ (see [1] in detail) we get:

Lemma 4.4. If φ has an equivalent TDNF (TCNF) formula, then φ also has an equivalent TCNF (TDNF) formula with the same order.

Proposition 4.5. Let φ be a contingent LTL _n formula. Then φ has an equivalent TDNF (TCNF) formula with order k iff Ch (φ) = k + 1.

Proof. On one hand, suppose that φ is equivalent to a formula ψ in TDNF (TCNF) with order k as shown in Eq. (5)-(6). By Lemma 3.4 and Proposition 3.5 we get Ch (φ) = Ch (ψ) = k + 1, which proves the necessity.

On the other hand, let ⊥ = a ∧ ¬ a and ⊤ = a ∨ ¬ a where a ∈ AP. In what follows we prove the sufficiency by induction on the complexity of φ.

(i) Let φ = b where b ∈ AP. Obviously Ch (φ) =1 and φ is in TDNF with order 0.

(ii) Let φ = ¬ ψ with Ch (ψ) = k + 1. Then Ch (φ) = Ch (ψ) = k + 1. Assume that ψ≡ (A₁₀ ∧ ○ A₁₁ ∧ ⋯ ∧ ○  ^k A_1k) ∨ ⋯ ∨ (A_t0 ∧ ○A_t1 ∧ ⋯ ∧ ○  ^k A _tk ). Then by Lemma 4.3 we get φ =¬ ψ ≡ ¬ ((A₁₀ ∧ ○ A₁₁ ∧ ⋯ ∧ ○  ^k A_1k) ∨ ⋯ ∨(A_t0 ∧ ○ A_t1 ∧ ⋯ ∧ ○  ^k A _tk )) ≡ (¬ A₁₀ ∨ ○ (¬ A₁₁)∨ ⋯ ∨ ○  ^k  (¬ A_1k)) ∧ ⋯ ∧ (¬ A_t0 ∨ ○ (¬ A_t1) ∨ ⋯ ∨ ○  ^k  (¬ A _tk )), which is in TCNF with order k. Consequently, φ has an equivalent TDNF formula with order k by Lemma 4.4.

(iii) Let φ = φ₁ ∧ φ₂ with Ch (φ₁) = k₁ + 1, Ch (φ₂) = k₂ + 1, and k = max {k₁, k₂}. Assume that φ₁ ≡ (A₁₀ ∨ ○ A₁₁ ∨ ⋯ ∨ ○  ^{k ₁} A_1k1) ∧ ⋯ ∧ (A_i0 ∨ ○ A_i1 ∨ ⋯ ∨ ○  ^{k ₁} A _{ik 1} ), φ₂ ≡ (B₁₀ ∨ ○ B₁₁ ∨ ⋯ ∨ ○  ^{k ₂} B_1k2) ∧ ⋯ ∧ (B_j0 ∨ ○ B_j1 ∨ ⋯ ∨ ○  ^{k ₂} B _{jk 2} ). Suppose that k₁ ≤ k₂, then k = k₂, and φ = φ₁ ∧ φ₂ ≡ (A₁₀ ∨ ○ A₁₁ ∨ ⋯ ∨ ○  ^{k ₁} A_1k1 ∨ ○ ^k₁+1 ⊥ ∨ ⋯ ∨ ○  ^k  ⊥) ∧ ⋯ ∧ (A_i0 ∨ ○ A_i1 ∨ ⋯ ∨ ○  ^{k ₁} A _{ik 1}  ∨ ○ ^k₁+1 ⊥ ∨ ⋯ ∨ ○  ^k  ⊥) ∧ (B₁₀ ∨ ○ B₁₁ ∨ ⋯ ∨ ○  ^k B_1k) ∧ ⋯ ∧ (B_j0 ∨ ○ B_j1 ∨ ⋯ ∨ ○  ^k B _jk ), which is in TCNF. Consequently, φ has an equivalent TDNF formula by Lemma 4.4.

(iv) Let φ = ○ ψ with Ch (ψ) = k + 1. Then Ch (φ) = k + 2. Assume that ψ ≡ (A₁₀ ∧ ○ A₁₁ ∧ ⋯ ∧ ○  ^k A_1k) ∨ ⋯ ∨ (A_t0 ∧ ○ A_t1 ∧ ⋯ ∧ ○  ^k A _tk ). Then φ = ○ ψ ≡ (⊤ ∧ ○ A₁₀ ∧ ○ ²A₁₁ ∧ ⋯ ∧ ○ ^k+1A_1k) ∨ ⋯ ∨ (⊤ ∧ ○ A_t0 ∧ ○ ²A_t1 ∧ ⋯ ∧ ○ ^k+1A _tk ), which is in TDNF with order k + 1.

(v) Let φ = φ₁ ⊔ ^≤nφ₂. Then φ ≡ φ₂ ∨ (φ₁ ∧ ○ φ₂) ∨ (φ₁ ∧ ○ φ₁ ∧ ○ ²φ₂) ∨ ⋯ ∨ (φ₁ ∧ ○ φ₁ ∧ ⋯ ∧ ○ ^n-1φ₁ ∧ ○  ⁿ φ₂) . Thus the proof of this case can be converted to cases (i)-(iv).

As a result, every contingent formula φ with Ch (φ) = k + 1 has an equivalent TDNF formula (also an equivalent TCNF formula by Lemma 4.4) with order k.

Corollary 4.6. Each LTL _n formula has an equivalent TDNF (TCNF) formula.

By Corollary 3.9 and 4.6, we can also get the following corollary.

Corollary 4.7. Let φ be an LTL formula. Then φ has an equivalent TDNF (TCNF) formula if and only if Ch (φ) exists.

It should be noted that an LTL formulae φ in TDNF or TCNF has a good property, that is, the set Words(φ) can be easily computed, which would simplify the procedure of model checking. For example, let φ = [b ∧ ○ (a ∨ ¬ a)] ∨ (a ∧ ○ b). We can easily obtain that Ch (φ) =2, and Words ⁽²⁾  (φ) =Words ⁽²⁾  (b∧ ○ (a ∨ ¬ a)) ∪ Words ⁽²⁾  (a ∧ ○ b) ={AB ∈ (2 ^AP ) ² ∣ b ∈ A or a ∈ A, b ∈ B}. Then by Equation (3), the set Words(φ) can be computed without difficulty.

The present paper introduced the concepts of characters as well as the least characters for LTL and LTL _n formulae. It was proved that all LTL _n formulae have characters as well as the least characters, and that those LTL formulae with characters can always be checked within finite steps during model checking. Besides, two types of temporal normal form, TDNF and TCNF, for LTL as well as LTL _n formulae were proposed. It was obtained that the class of TDNF (TCNF) formulae is as expressive as full LTL _n . Finally, a necessary and sufficient condition was given in which an LTL formula has an equivalent TDNF (TCNF) formula. As one can see, TDNF and TCNF formulae are simple in form and consequently easy to be checked during model checking. The application of TDNF and TCNF formulae in model checking will be studied in a forthcoming paper.