=Paper=
{{Paper
|id=Vol-1195/short2
|storemode=property
|title=A First Study of the Horn Fragment of the Modal Logic of Time Intervals
|pdfUrl=https://ceur-ws.org/Vol-1195/short2.pdf
|volume=Vol-1195
|dblpUrl=https://dblp.org/rec/conf/cilc/BresolinMS14
}}
==A First Study of the Horn Fragment of the Modal Logic of Time Intervals==
https://ceur-ws.org/Vol-1195/short2.pdf
A First Study of the Horn Fragment of the Modal Logic
of Time Intervals?
D. Bresolin1 , E. Muñoz-Velasco2 , and G. Sciavicco3
1
Department of Computer Science and Engineering
University of Bologna (Italy) (davide.bresolin@unibo.it)
2
Department of Applied Mathematics
University of Malaga (Spain) (emilio@ctima.uma.es)
3
Department of Information, Engineering and Communications
University of Murcia (Spain) (guido@um.es)
Abstract. Interval temporal logics provide a natural framework for temporal rea-
soning about interval structures over linearly ordered domains, where intervals
are taken as the primitive ontological entities. The most influential propositional
interval-based logic is probably Halpern’s and Shoham Modal Logic of Time In-
tervals, a.k.a. HS. While most studies focused on the computational properties of
the syntactic fragments that arise by considering only a subset of the set of modal-
ities, the fragments that are obtained by weakening the propositional side of HS
have received much less attention. Here, we approach this problem by consider-
ing the Horn fragment of HS and proving that the satisfiability problem remains
undecidable, at least for discrete linear orders.
1 Introduction
Most temporal logics proposed in the literature assume a point-based model of time, and
they have been successfully applied in a variety of fields. However, there are examples
of relevant application domains, such as planning and temporal databases, where inter-
esting problems are dealt with in an unsatisfactory way by point-based formalisms [9,
10]. Interval temporal logics provide a natural framework for temporal reasoning about
interval structures over linearly (or partially) ordered domains. They take time intervals
as the primitive ontological entities and define truth of formulas relative to time inter-
vals, rather than time points; their modalities correspond to various relations between
pairs of intervals. In particular, the well-known logic HS [6] features a set of modali-
ties that make it possible to express all Allen’s interval relations [1]. Unfortunately, in
interval temporal logic undecidability is the rule and decidability the exception: HS is
undecidable when interpreted on most meaningful classes of linearly ordered sets, and
limiting the set of temporal modalities of the logic is not always sufficient to achieve
decidability. For example, when formulas are interpreted over strongly discrete linear
orders, only 44 decidable fragments exist [3].
?
The authors acknowledge the support from the Italian GNCS Project “Automata, games and
temporal logics for verification and synthesis of safety-critical systems” (D. Bresolin), the
Spanish Project TIN12-39353-C04-01 (E. Muñoz-Velasco), and the Spanish fellowship pro-
gram ‘Ramon y Cajal’ RYC-2011-07821 (G. Sciavicco).
314
D. Bresolin et al. A First Study of the Horn Fragment of the Modal Logic of Time Intervals
In this context, it makes sense to study sub-propositional fragments of HS, such as
the Horn fragment. Horn fragments of modal and temporal logics have been studied,
for example, in [2, 4, 5, 7]. Being sub-propositional, the obvious question is whether
or not the satisfiability problem of Horn HS remains undecidable, and, if so, on which
classes of linearly ordered sets. The results presented in this preliminary study proves
that, unfortunately, at least in the class of models built over Z and other strongly discrete
linear orders, this is the case. While discouraging, these results should be seen as the
first attempt of studying sub-propositional fragments of interval temporal logics. Horn
HS is still undecidable, but we might find out that the decidability frontier is different
from the one for the syntactical fragments of full HS, and/or that some of the decidable
fragments present a better computational behaviour.
2 The Logic HS and its Horn Fragment
Halpern and Shoham’s logic HS is a multi-modal logic with formulas built on a set
AP of proposition letters, the Boolean connectives _ and ¬, plus the six modalities to
capture the existence of an interval in a particular Allen’s relation with the current one:
' ::= p | ¬' | ' _ ' | ' ^ ' | hAi' | hAi' | hBi' | hBi' | hEi' | hEi'
The other Boolean connectives, the box modalities, and the temporal modalities cor-
responding to other Allen’s relations (such as during, hDi, later, hLi, and overlaps,
hOi) are definable in the language (e.g. [A]' ⌘ ¬hAi¬', hDi' = hEihBi', and
hLi' = hAihAi').
Let D = hD, y such that M, [y, z] ';
– M, [x, y] hAi' iff there exists z < x such that M, [z, x] ';
– M, [x, y] hBi' iff there exists x < z < y such that M, [x, z] ';
– M, [x, y] hBi' iff there exists z > y such that M, [x, z] ';
– M, [x, y] hEi' iff there exists x < z < y such that M, [z, y] ';
– M, [x, y] hEi' iff there exists z < x such that M, [z, y] '.
A HS-formula ' is satisfiable if and only if there exists a model M and an interval [x, y]
such that M, [x, y] '. The satisfiability problem for HS is the problem of finding a
model and an interval that satisfies a formula.
Following [7], we define the Horn fragment of HS. First, consider only formulas in
negative normal form (nnf) (i.e., with only ^ and _ as Boolean connectives and such
that ¬ occurs only in front of propositions). A formula in nnf is called negative if and
315
D. Bresolin et al. A First Study of the Horn Fragment of the Modal Logic of Time Intervals
only if every proposition is prefixed by negation; it is non-negative if it is not negative,
and positive if its negation is a negative formula. An HS-formula ' is called a Horn
HS-formula (or, simply, Horn) if and only if (i) ' is a proposition; (ii) ' is a negative
formula; (iii) ' = [X] , ' = hXi , or ' = ^ ⇢, where and ⇢ are Horn and
hXi is any HS modality; (iv) ' = ! ⇢, where is positive and ⇢ is Horn; (v) '
is a disjunction of a negative formula and a Horn formula. Alternative definitions of
modal Horn clauses can be found, for example, in [2, 4, 5]. However, these definitions
are equivalent to Nguyen’s one [7], in the sense that every given set of Horn formulas
(or clauses) in the latter can be translated into set of equi-satisfiable Horn clauses of any
of the formers.
In the following we will make use of the universal modality [U ], that can be defined
in Horn HS as a conjunction of boxes ([U ]' = [A][A][A]' ^ [A][A]' ^ [A][A][A]'),
and of the difference modality [6=], meaning for every interval, except the current one,
that can be defined in a similar way.
3 Undecidability of Horn HS
In this section, we assume that Horn HS is interpreted over Z. Notice that this assump-
tion can be immediately relaxed, to include Horn HS interpreted over N, over the class
of all strongly discrete linear orders, and over the class of finite linear orders. Our con-
struction, that closely follows both the original undecidability proof for full HS [6] and
more recent undecidability proofs for fragments of HS [3], is based on a reduction from
the halting problem of a deterministic Turing Machine on empty input [8].
A Turing Machine is defined as a tuple A = (Q, ⌃, , , q0 , qf ), where Q is the set
of states, q0 (resp., qf ) is the initial (resp., final) state, ⌃ is the machine’s alphabet that
does not contain t (blank), = ⌃ [{t} is the tape alphabet, and : Q⇥ ! Q⇥ ⇥
{L, R} is the transition function (L, R represent the possible moves on the machine’s
tape: left, right). Even under the assumption that ⌃ = {0, 1} and that the input is empty,
the halting problem for a deterministic Turing Machine is undecidable [8].
In the following, we reduce the halting problem of a Turing Machine to the satisfia-
bility problem for Horn HS over Z. The underlying idea is to represent the computation
history of the machine using the propositional symbol ⇤ to separate successive configu-
rations, the propositional symbols 0, 1, t to represent tape cells not under the machine’s
head, and propositional symbols q c , with q 2 Q \ {qf } and c 2 {0, 1, t}, to represent
the tape cell under the head and the current (non-final) state of the machine. We will use
the propositional symbols Fr to encode the initial configuration, u to represent the units,
Co to represent a generic configuration, and Cr to connect successive configurations.
When the machine is in the final state qf the computation immediately halts. For this
reason we can discard the symbol under the head and use a unique propositional letter
qf . We denote by L the set {0, 1, t, ⇤} [ {q c | q 2 Q \ {qf } ^ c 2 {0, 1, t}} [ {qf }.
Any terminating run of the Turing Machine will make use of only a finite portion of the
tape. Hence, we can assume w.l.o.g. that all configurations have the same length and
that they are long enough to contain the relevant part of the tape.
hAiu ^ [U ](u ! (hAiu ^ [B]?)) units’ structure
316
D. Bresolin et al. A First Study of the Horn Fragment of the Modal Logic of Time Intervals
V
[U ] Vl2L (l ! u) tape/state propositions and ⇤ are units
[U ] l,l0 2L,l6=l0 (l ! ¬l0 ) tape/state propositions and ⇤ are unique
hAi(⇤ ^ hAiFr ) ^ hAiCo ^ [U ](Fr ! [6=]¬Fr ) initial configuration
[U ](Fr ! (hBiq0t ^ hEi ⇤ ^([D](u ! t)))) Fr structure
[U ](Co ! (hAiCo ^ hBi ⇤ ^hEi ⇤ ^[D]¬⇤) configuration sequence
[U ](Co ! ([D]¬Co ^ [B]¬Co ^ [E]¬Co)) configuration structure
Intuitively, the above formulas guarantee that configurations (denoted by Co) are built
of units, each one of them contains either ⇤ or a tape/head element and that there is an
infinite and unique sequence of configurations. The proposition Fr sets the structure of
the first configuration: a single ⇤, followed by q0 reading blank, and a number of blanks,
followed by a ⇤.
The relation between successive configurations is maintained by the proposition Cr
(corresponds), constrained by the following formulas. These are also used to guarantee
that all configurations have the same length.
[U ](u ! (hAiCr ^ hAiCr )) each unit starts and ends a “Cr”
[U ](Cr ! ([B]¬Cr ^ [D]¬Cr ^ [E]¬Cr )) “Cr” structure
[U ](Co ! (¬Cr ^ [D]¬Cr ^ [D]¬Cr ^ [E]¬Cr ) “Cr/Co” relation
It remains to ensure that the machine A behaves as imposed by . In the encoding
of the transition function, we treat as special cases the situations in which (i) the head is
at the last cell of the segment of the tape currently shown and the head must be moved
to the right and, (ii) the head is at the first cell of the tape and the head must be moved to
the left. In the following formulas, c, c0 , c00 2 {0, 1, t}, d 2 {0, 1, t, ⇤}, and q, q 0 2 Q
(by a little abuse of notation, we assume that all symbols qfc are equal to qf ).
V c 00
d, (q,c)=(q 0 ,c0 ,R),c00 [U ]((q ^ hAic ^ hAid) ! to the right, not the last cell
0 0c00
V [A](Cr ! hAi(c ^ hAiq ^ hAid)))
(q,c)=(q 0 ,c0 ,R) [U ]((q c ^ hAi⇤) ! ?) to the right, last cell: forbidden
V
0 0
d, (q,c)=(q ,c ,L),c 00 [U ]((q c
^ hAic 00
^ hAid) ! to the left, not the first cell
00
V [A](Cr ! hAi(c0 ^ hAiq 0c ^ hAid)))
d, (q,c)=(q 0 ,c0 ,L) [U ]((q c ^ hAi ⇤ ^hAid) ! to the left, first cell
0c0
[A](Cr ! hAi(q ^ hAi ⇤ ^hAid)))
Finally, we force cells located away from the head to remain unchanged.
V 0 00
c,c0 ,c00 [U ]((c ^ hAic ^ hAic ) ! [A](Cr ! hAic))
The conjunction 'A of all formulas above encodes a computation of the Turing
Machine.
Theorem 1. Let A be a deterministic Turing Machine. Then, A halts on an empty input
if and only if the Horn HS-formula 'A ^ hLiqf is satisfiable over Z.
This proves that the satisfiability problem for Horn HS interpreted over Z is unde-
cidable. The construction can be rephrased to deal with the cases where Horn HS is
interpreted over N, or in the class of all strongly discrete linear orders, or over finite
linear orders.
317
D. Bresolin et al. A First Study of the Horn Fragment of the Modal Logic of Time Intervals
4 Conclusions
Sub-propositional fragments, such as the Horn fragment, of classical and modal logics
have been extensively studied. The generally high complexity of the (few) decidable in-
terval temporal logics justifies the study of sub-propositional fragments of interval log-
ics in search of expressive languages that present a better computational behaviour. In
this paper we proved a first negative result in this sense, by showing that the well-known
interval temporal logic HS is still undecidable when its Horn fragment is considered, at
least in the discrete case. Nevertheless, we believe that syntactical fragments of Horn
HS should be studied in the same way in which syntactical fragments of full HS have
been. In the long run, we plan to consider the Horn fragments of decidable interval log-
ics like AA and ABBL, to understand whether or not their satisfiability problem present
a better computational behaviour.
References
1. J. F. Allen. Maintaining knowledge about temporal intervals. Communications of the ACM,
26(11):832–843, 1983.
2. A. Artale, R. Kontchakov, V. Ryzhikov, and M. Zakharyaschev. The complexity of clausal
fragments of LTL. In Proc. of the 19th International Conference on Logic for Programming,
Artificial Intelligence, and Reasoning (LPAR), volume 8312 of LNCS, pages 35–52. Springer,
2013.
3. D. Bresolin, D. Della Monica, A. Montanari, P. Sala, and G. Sciavicco. Interval temporal log-
ics over strongly discrete linear orders: the complete picture. In Proc. of the 4th International
Symposium on Games, Automata, Logics, and Formal Verification (GANDALF), volume 96
of EPTCS, pages 155–169, 2012.
4. C. Chen and I. Lin. The computational complexity of the satisfiability of modal Horn clauses
for modal propositional logics. Theoretical Computer Science, 129(1):95–121, 1994.
5. L. Fariñas Del Cerro and M. Penttonen. A note on the complexity of the satisfiability of
modal Horn clauses. Journal of Logic Programming, 4(1):1–10, 1987.
6. J. Halpern and Y. Shoham. A propositional modal logic of time intervals. Journal of the
ACM, 38(4):935–962, 1991.
7. L. Nguyen. On the complexity of fragments of modal logics. Advances in Modal Logic,
5:318–330, 2004.
8. M. Sipser. Introduction to the theory of computation. PWS Publishing Company, 1997.
9. D. E. Smith. The case for durative actions: a commentary on PDDL2.1. Journal of Artificial
Intelligence Reasoning, 20(1):149–154, Dec. 2003.
10. D. Toman. Point vs. interval-based query languages for temporal databases. In Proceed-
ings of the fifteenth ACM SIGACT-SIGMOD-SIGART symposium on Principles of Database
Systems, pages 58–67. ACM, 1996.
318