REASONING ABOUT BOUNDED TIME DOMAIN
An Alternative to NP-Complete Fragments of LTL
Norihiro Kamide
Waseda Institute for Advanced Study, 1-6-1 Nishi Waseda, Shinjuku-ku, Tokyo 169-8050, Japan
Keywords:
Temporal reasoning, Bounded time domain, Linear-time temporal logic, Satisfiability, NP-completeness.
Abstract:
It is known that linear-time temporal logic (LTL) is one of the most useful logics for reasoning about time and
for verifying concurrent systems. It is also known that the satisfiability problem for LTL is PSPACE-complete
and that finding NP-complete fragments of LTL is an important issue for constructing efficiently executable
temporal logics. In this paper, an alternative NP-complete logic called bounded linear-time temporal logic is
obtained from LTL by restricting the time domain of temporal operators.
1 INTRODUCTION
It is known that linear-time temporal logic (LTL)
(Pnueli, 1977) is one of the most useful logics for rea-
soning about time and for verifying concurrent sys-
tems by model checking (Clarke et al., 1999; Holz-
mann, 2006). It is also known that in almost all
cases, the model checking problems for LTL and its
fragments are equivalent to the satisfiability problems
for them. For this reason, the satisfiability prob-
lems for LTL fragments are known to be an im-
portant issue for constructing efficiently executable
temporal logics. The satisfiability problem for LTL
is PSPACE-complete (Sistla and Clarke, 1985) and
finding NP-complete fragments of LTL has been
well-studied (Demri and Schnoebelen, 2002; Etes-
sami et al., 1997; Muscholl and Walukiewicz, 2005;
Walukiewicz, 1998). This paper tries to construct an
alternative to such an NP-complete fragment by re-
stricting the time domain of temporal operators. Al-
though the standard temporal operators of LTL have
an infinite (unbounded) time domain, i.e., the set ω
of natural numbers, the bounded operators which are
presented in this paper have a bounded time domain
which is restricted by a fixed positive integer l, i.e.,
the set ω
l
:= {x ∈ ω | x ≤ l}. Despite this restriction,
the proposed bounded operators can derive almost all
the typical LTL axioms including the temporal induc-
tion axiom.
To restrict the time domain of temporal operators
is not a new idea. Such an idea has been discussed
(Biere et al., 2003; Cerrito et al., 1999; Cerrito and
Mayer, 1998; Hodkinson et al., 2000; Kamide, 2008).
It is known that to restrict the time domain is a tech-
nique to obtain a decidable or efficient fragment of
first-order LTL (Hodkinson et al., 2000). Restricting
the time domain implies not only some purely theo-
retical merits, but also some practical merits for de-
scribing temporal databases and planning specifica-
tions (Cerrito et al., 1999; Cerrito and Mayer, 1998),
and for implementing an efficient model checking al-
gorithm called bounded model checking (Biere et al.,
2003). Such practical merits are due to the fact that
there are problems in computer science and artificial
intelligence where only a finite fragment of the time
sequence is of interest (Cerrito et al., 1999).
The contents of this paper are then summarized as
follows. In Section 2, a logic called bounded linear-
time temporal logic (BLTL) is obtained from LTL by
restricting the time domain of temporal operators. In
order to obtain a theorem for embedding BLTL into
classical propositional logic (CL), a semantics for CL
is also defined. In Section 3, the NP-completeness of
the satisfiability problem for BLTL is shown using the
embedding theorem of BLTL into CL. In Section 4,
conclusions and related works are briefly addressed.
2 BOUNDED LINEAR-TIME
TEMPORAL LOGIC
Formulas of BLTL are constructed from (countably
many) propositional variables, → (implication), ∧
(conjunction), ∨ (disjunction), ¬ (negation), X (next),
G (globally) and F (eventually) where X, G and F are
536
Kamide N. (2010).
REASONING ABOUT BOUNDED TIME DOMAIN - An Alternative to NP-Complete Fragments of LTL.
In Proceedings of the 2nd International Conference on Agents and Artificial Intelligence - Artificial Intelligence, pages 536-539
DOI: 10.5220/0002714805360539
Copyright
c
SciTePress
bounded versions of the standard operators of LTL.
Lower-case letters p, q, ... are used to denote proposi-
tional variables, and Greek lower-case letters α, β, ...
are used to denote formulas. We write A ≡ B to in-
dicate the syntactical identity between A and B. The
symbol ω is used to represent the set of natural num-
bers. Lower-case letters i, j and k are used to denote
any natural numbers. The symbol ≥ or ≤ is used to
represent a linear order on ω. Let l be a fixed positive
integer. Then, the symbol ω
l
is used to denote the set
{i ∈ ω | i ≤ l}. In the following discussion, l is fixed
as a certain positive integer.
Definition 2.1 (BLTL). Let S be a non-empty set of
states. A structure M := (σ, I) is a model if
1. σ is an infinite sequence s
0
, s
1
, s
2
, ... of states in S,
2. I is a mapping from the set Φ of propositional
variables to the power set of S.
A satisfaction relation (M, i) |= α for any formula
α, where M is a model (σ, I) and i (∈ ω) represents
some position within σ, is defined inductively by
1. for any p ∈ Φ, (M, i) |= p iff s
i
∈ I(p),
2. (M, i) |= α∧ β iff (M, i) |= α and (M, i) |= β,
3. (M, i) |= α∨ β iff (M, i) |= α or (M, i) |= β,
4. (M, i) |= α→β iff (M, i) |= α implies (M, i) |= β,
5. (M, i) |= ¬α iff not-[(M, i) |= α],
6. for any i ≤ l − 1, (M, i) |= Xα iff (M, i+ 1) |= α,
7. for any i ≥ l, (M, i) |= Xα iff (M, l) |= α,
8. (M, i) |= Gα iff ∀ j ≥ i with j ∈ ω
l
[(M, j) |= α],
9. (M, i) |= Fα iff ∃ j ≥ i with j ∈ ω
l
[(M, j) |= α],
10. for any m ∈ ω, (M, l + m) |= α iff (M, l) |= α.
A formula α is valid in BLTL if (M, 0) |= α for any
model M := (σ, I). A formula α is satisfiable in LTL
if (M, 0) |= α for some model M := (σ, I).
Since BLTL depents on l, it should precisely be
named e.g., BLTL[l], but, for the sake of simplicity,
we use the name BLTL in the following.
An expression α ↔ β means (α→β) ∧ (β→α).
Expressions
V
C and
W
C are used to represent the fi-
nite conjunction and disjunction of the formulas in C,
respectively.
Proposition 2.2. The following formulas are valid in
BLTL:
1. X(α◦ β) ↔ Xα◦ Xβ where ◦ ∈ {→, ∧, ∨},
2. X(¬α) ↔ ¬(Xα),
3. Gα→α,
4. Gα → Xα,
5. Gα → XGα,
6. Gα → GGα,
7. α∧ G(α→Xα)→Gα (temporal induction),
8. for any m ∈ ω, X
l+m
α ↔ X
l
α,
9. Gα ↔
^
{X
i
α | i ∈ ω
l
},
10. Fα ↔
_
{X
i
α | i ∈ ω
l
}.
Proof. We show some critical cases. Let M be an
arbitrary model and |= be an arbitrary satisfaction re-
lation on M.
(7): We show (M, 0) |= α ∧ G(α→Xα)→Gα.
Suppose (M, 0) |= α ∧ G(α→Xα), i.e., (a): (M, 0) |=
α and (b): (M, 0) |= G(α→Xα). We will show
(M, 0) |= Gα, i.e., ∀ j ∈ ω
l
[(M, i) |= α]. From (b),
we obtain:
(M, 0) |= G(α→Xα)
iff ∀ j ∈ ω
l
[(M, j) |= α→Xα]
iff ∀ j ∈ ω
l
[(M, j) |= α =⇒ (M, j) |= Xα]
iff (c): ∀j ∈ ω
l
[(M, j) |= α =⇒ (M, j + 1) |=
α (if j ≤ l − 1) or (M, l) |= α (if j ≥ l)].
We now show the required fact ∀i ∈ ω
l
[(M, i) |= α]
by mathematical induction on i. Base step: We have
(M, 0) |= α by (a). Induction step: Suppose (M, k) |=
α with k ≤ l − 1. Then, we obtain (M, k+ 1) |= α by
(c). Suppose (M, k) |= α with k ≥ l. Then, we obtain
(M, l) |= α by (c), and hence obtain (M, k + 1) |= α
where k+ 1 = l + m with m ∈ ω.
(8): We obtain: (M, 0) |= X
l+n
α iff (M, l) |= α iff
(M, 0) |= X
l
α.
(9): We obtain: (M, 0) |= Gα iff ∀ j ∈
ω
l
[(M, j) |= α] iff ∀ j ∈ ω
l
[(M, 0) |= X
j
α] iff
(M, 0) |=
^
{X
j
α | j ∈ ω
l
}.
Remark that 8, 9 and 10 in Proposition 2.2 are re-
garded as characteristic axioms concerning the time
bound l. Note that 9 and 10 in Proposition 2.2 be-
come the axioms of LTL if ω
l
is replaced by ω. Thus,
BLTL is quite natural as a bounded time formalism.
Formulas of classical logic (CL) are constructed
from (countably many) propositional variables, →, ¬,
V
(finite conjunction) and
W
(finite disjunction).
Definition 2.3 (CL). Let Θ be a finite (non-empty) set
of formulas. V is a mapping from the set Φ of propo-
sitional variables to the set {t, f} of truth values. V is
called a valuation. A satisfaction relation V |= α for
any formula α is defined inductively by
1. V |= p iff V(p) = t for any p ∈ Φ,
2. V |= ¬α iff not-(V |= α),
3. V |= α→β iff V |= α implies V |= β,
4. V |=
V
Θ iff V |= α for any α ∈ Θ,
5. V |=
W
Θ iff V |= α for some α ∈ Θ.
A formula α is valid (satisfiable) in CL if V |= α
for any (some) valuation V.
REASONING ABOUT BOUNDED TIME DOMAIN - An Alternative to NP-Complete Fragments of LTL
537
3 NP-COMPLETENESS
Definition 3.1. Fix a countable non-empty set Φ
of propositional variables. Define the sets Φ
i
:=
{p
i
| p ∈ Φ} (i ∈ ω) of propositional variables where
p
0
= p (i.e., Φ
0
:= Φ). The language L
b
of BLTL
is defined using Φ, →, ∧, ∨, ¬, X, G and F. The lan-
guage L of CL is defined using
[
i∈ω
Φ
i
, →, ¬,
V
and
W
. The binary versions of
V
and
W
are also denoted
as ∧ and ∨, respectively, and these binary symbols
are included in the definition of L .
A mapping f from L
b
to L is defined by
1. for any p ∈ Φ, f(X
i
p) := p
i
∈ Φ
i
, especially,
f(p) := p ∈ Φ,
2. f(X
i
(α ◦ β)) := f(X
i
α) ◦ f(X
i
β) where ◦ ∈
{→, ∧, ∨},
3. f(X
i
¬α) := ¬ f(X
i
α),
4. for any m ≥ l, f(X
m
Xα) := f(X
l
α),
5. f(X
i
Gα) :=
V
{ f(X
i+ j
α) | j ∈ ω
l
},
6. f(X
i
Fα) :=
W
{ f(X
i+ j
α) | j ∈ ω
l
}.
Remark that the mapping f in Definition 3.1 is
a polynomial-time reduction since f(α) can be com-
puted by subformulas of α.
Lemma 3.2. Let f be the mapping defined in Defini-
tion 3.1, and S be a non-empty set of states. For any
model M := (σ, I) of BLTL, any satisfaction relation
|= on M and any state s
i
in σ, we can construct a val-
uation V of CL and a satisfaction relation |= of CL
such that for any formula α in L
b
,
(M, i) |= α iff V |= f(X
i
α).
Proof. Let Φ be a non-empty set of propositional
variables and Φ
i
be the set {p
i
| p ∈ Φ}. Suppose
that M is a model (σ, I) where
I is a mapping from Φ to the power set of S.
Suppose that
V is a mapping from
[
i∈ω
Φ
i
to {t, f}.
Suppose moreover that I and V satisfy the following
condition:
∀i ∈ ω, ∀p ∈ Φ [s
i
∈ I(p) iff V(p
i
) = t].
Then, the lemma is proved by induction on the
complexity of α. For the sake of simplicity, V of V |=
is omitted in the following.
• Base step: α ≡ p ∈ Φ. (M, i) |= p iff s
i
∈ I(p)
iff V(p
i
) = t iff |= p
i
iff |= f(X
i
p) (by the definition
of f).
• Induction step.
(Case α ≡ β∧ γ): (M, i) |= β∧ γ iff (M, i) |= β and
(M, i) |= γ iff |= f(X
i
β) and |= f(X
i
γ) (by induction
hypothesis) iff |= f(X
i
β) ∧ f(X
i
γ) iff |= f(X
i
(β∧ γ))
(by the definition of f).
(Cases α ≡ β ∨ γ and α ≡ β→γ): Similar to the
above case.
(Case α ≡ ¬β): (M, i) |= ¬β iff not-[(M, i) |= β]
iff not-[|= f(X
i
β)] (by induction hypothesis) iff |=
¬ f (X
i
β) iff |= f(X
i
¬β) (by the definition of f ).
(Case α ≡ Xβ):
Subcase (i ≤ l − 1): (M, i) |= Xβ iff (M, i+ 1) |=
β iff |= f(X
i+1
β) (by induction hypothesis) iff |=
f(X
i
(Xβ)).
Subcase (i ≥ l): (M, i) |= Xβ iff (M, l) |= β iff |=
f(X
l
β) (by induction hypothesis) iff f(X
i
Xβ) (by the
definition of f).
(Case α ≡ Gβ): (M, i) |= Gβ iff ∀ j ≥ i with j ∈
ω
l
[(M, j) |= β] iff ∀ j ≥ i with j ∈ ω
l
[|= f(X
j
β)]
(by induction hypothesis) iff ∀k ∈ ω
l
[|= f(X
i+k
β)]
iff |= γ for all γ ∈ { f(X
i+k
β) | k ∈ ω
l
} iff |=
^
{ f(X
i+k
β) | k ∈ ω
l
} iff |= f(X
i
Gβ) (by the defini-
tion of f).
(Case α ≡ Fβ): Similar to the above case.
Lemma 3.3. Let f be the mapping defined in Defini-
tion 3.1, and S be a non-empty set of states. For any
valuation V of CL and any satisfaction relation |= of
CL, we can construct a model M := (σ, I) of BLTL
and a satisfaction relation |= on M such that for any
formula α in L
b
,
V |= f(X
i
α) iff (M, i) |= α.
Proof. Similar to the proof of Lemma 3.2.
Theorem 3.4 (Embedding). Let f be the mapping
defined in Definition 3.1. For any formula α, α is
valid (satisfiable) in BLTL iff f(α) is valid (satisfi-
able) in CL.
Proof. By Lemmas 3.2 and 3.3.
We then obtain the main theorem of this paper as
follows.
Theorem 3.5 (Complexity). The validity and satis-
fiability problems of BLTL are Co-NP-complete and
NP-complete, respectively.
Proof. The validity and satisfiability problems of CL
are known to be Co-NP-complete and NP-complete,
respectively. By decidability of CL, for each α, it
is possible to decide if f(α) is valid (satisfiable) in
BLTL. Then, by Theorem 3.4, the validity and satis-
fiability problems of BLTL are decidable. Since f is
a polynomial-time reduction, the validity and satisfi-
ability problems of BLTL are also Co-NP-complete
and NP-complete, respectively.
ICAART 2010 - 2nd International Conference on Agents and Artificial Intelligence
538
4 CONCLUSIONS AND RELATED
WORKS
In this paper, BLTL, which is obtained from LTL by
restricting the time domain of temporal operators, was
introduced, and the satisfiability problem for BLTL
was shown to be NP-complete by using a theorem for
embedding BLTL into CL. The embedding theorem
had a central role for showing the NP-completeness
of BLTL. The embedding theorem may also be justi-
fied by the usefulness of the bounded model checking
technique (Cerrito and Mayer, 1998), which uses a
propositional satisfiability checking technique. It was
thus shown in this paper that the existing satisfiability
checking techniques of CL are available for BLTL.
This is an advantage of BLTL.
In the following, some related works are briefly
reviewed. It is known (Sistla and Clarke, 1985) that
the LTL fragment endowed with the standard opera-
tors X, G and F are PSPACE-complete and that the
fragment endowed with either X or (F and G) has NP-
complete satisfiability problems. Some NP-complete
fragments of LTL have been well-studied (Demri and
Schnoebelen, 2002; Etessami et al., 1997; Muscholl
and Walukiewicz, 2005; Walukiewicz, 1998). Some
restrictions on the nesting of operators and on the
number of propositions were proposed by Demri and
Schnoebelen (Demri and Schnoebelen, 2002). Re-
stricting X to operators X
a
(a ∈ Σ) that enforce the
current letter to be a was proposed by Muscholl
and Walukiewicz (Muscholl and Walukiewicz, 2005).
The formula Xα is expressed as
W
a∈Σ
X
a
α where Σ is
the alphabet. They proved that the satisfiability prob-
lem for the LTL fragment with X
a
(a ∈ SI), F and G is
NP-complete. Finally it is mentioned that a Gentzen-
type sequent calculus for a modification of BLTL was
proposed by Kamide (Kamide, 2008).
ACKNOWLEDGEMENTS
This research was supported by the Alexander von
Humboldt Foundation and the Japanese Ministry of
Education, Culture, Sports, Science and Technology,
Grant-in-Aid for Young Scientists (B) 20700015.
REFERENCES
Biere, A., Cimatti, A., Clarke, E. M., Strichman, O., and
Zhu, Y. (2003). Bounded model checking. Advances
in Computers, 58:118–149.
Cerrito, S. and Mayer, M. C. (1998). Bounded model search
in linear temporal logic and its application to plan-
ning. In Lecture Notes in Computer Science, volume
1397, pages 124–140.
Cerrito, S., Mayer, M. C., and Prand, S. (1999). First or-
der linear temporal logic over finite time structures.
In Lecture Notes in Computer Science, volume 1705,
pages 62–76.
Clarke, E. M., Grumberg, O., and Peled, D. A. (1999).
Model checking. The MIT Press.
Demri, S. and Schnoebelen, P. (2002). The complexity of
propositional linear temporal logics in simple cases.
Infomation and Computation, 174 (1):84–103.
Etessami, K., Vardi, M. Y., and Wilke, T. (1997). First-order
logic with two variables and unary temporal logic.
In Proceedings of the 12th Annual IEEE Symposium
on Logic in Computer Science (LICS’97), pages 228–
235.
Hodkinson, I., Wolter, F., and Zakharyaschev, M. (2000).
Decidable fragments of first-order temporal logics.
Annals of Pure and Applied Logic, 106:85–134.
Holzmann, G. J. (2006). The SPIN model checker: Primer
and reference manual. Addison-Wesley.
Kamide, N. (2008). Bounded linear-time temporal logic:
From gentzen to robinson. manuscript.
Muscholl, A. and Walukiewicz, I. (2005). An np-complete
fragment of ltl. International Journal of Foundations
of Computer Science, 16 (4):743–753.
Pnueli, A. (1977). The temporal logic of programs. In Pro-
ceedings of the 18th IEEE Symposium on Foundations
of Computer Science, pages 46–57.
Sistla, A. P. and Clarke, E. M. (1985). The complexity
of propositional linear temporal logic. Journal of the
ACM, 32 (3):733–749.
Walukiewicz, I. (1998). Difficult configurations - on the
complexity of ltrl. In Lecture Notes in Computer Sci-
ence, volume 1443, pages 140–151.
REASONING ABOUT BOUNDED TIME DOMAIN - An Alternative to NP-Complete Fragments of LTL
539
