Searching for Well-Behaved Fragments of Halpern-Shoham Logic

1 Halpern-ShohamLogic and its Fragments

Halpern-Shoham logic ([Halpern and Shoham, 1991]) is an elegant multimodal logic for reasoning about time intervals. Time line is modelled as a linear ordering of time-points, and an interval as an ordered pair of points: its beginning and ending points. Modal operators occurring in the language of HS enable us to access an interval that begins (B), is during (D), ends (E), overlaps (O), is adjacent to (A), or is later than (L) the current interval [x, y]. The listed relations are defined as:

The further 6 relations are inverses of the above ones. In total, there are 12 relations which give rise to semantics of 12 diamond and 12 box modal operators of the form 〈R〉, and [R], respectively, where R is any of the 12 relations described above. An expression 〈R〉ϕ states that a formula ϕ holds in some interval that is in a relation R with the current interval, and [R]ϕ states that ϕ holds in all intervals that are in a relation R with the current interval. The language of HS is very expressive but the satisfiability problem of its formulas is undecidable [Halpern and Shoham, 1991]. This negative result motivated a search for decidable HS fragments which would be still expressive enough for interesting applications.

The recently proposed method for obtaining HS fragments is to syntactically restrict the form of its formulas [Bresolin et al., 2014]. The set of formulas called the Horn fragment of HS (HShorn in short) is defined by the following grammar:

where [U] is the universal modality stating that a formula holds in all intervals, and λ is a positive temporal literal:

where p is a propositional variable and R is any of 12 relations that can hold between intervals. Further restrictions give rise to the fragment HS ✸horn , which is obtained by deleting an expression of the form [R]λ from the grammar (2), and HS ✷horn is obtained by deleting 〈R〉λ from (2) - see Figure 1 (for the meaning of i and i, @ see the subsequent section).

The main problem investigated within the research on HS fragments is determining their expressiveness, decidability, and computational complexity. Interestingly, the results depend on the assumed structure of time [Bresolin et al., Forthcoming]. Among the 3 main lines of division, the first one is between:

• (Den) Dense time lines - for any time-points x, y such that x < y there is some time-point z such that x < z < y;
• (Dis) Discrete time lines - any non-maximal timepoint has an immediate <-successor, and every non-minimal time-point has an immediate <-predecessor.

The second distinguishes between:

• (S) Strict semantics - punctual intervals, i.e., intervals in which the beginning and ending points coincide, are disallowed;
• (Non-S) Non-Strict semantics - punctual intervals are allowed.

The last line demarcates:

• (<) Irreflexive semantics - the ordering "<" exploited in the beginning of the section to define relations between intervals represents an irreflexive greaterthan ordering;
• (≤) Reflexive semantics - each occurrence of "<" is replaced by "≤" in the definition of relations under irreflexive semantics, where ≤ represents a greater-or-equal ordering.

The most striking result obtained so far is that the satisfiability problem of HS ✷horn -formulas is P-complete under (Den,<,S), (Den,<,Non-S), (Dis,≤,Non-S), (Den,≤,S), and (Den,≤,Non-S) semantics [Bresolin et al., Forthcoming]. Moreover, this fragment was already applied to solve a real-life problem [Kontchakov et al., 2016].

2 My Results and FutureWork

As showed in [Areces et al., 2000], full HS is expressive enough to enable referring to a single interval. More precisely, in the language of HS we can define the hybrid machinery [Blackburn, 2000], i.e., nominals - the special sort of atoms each of which is true in exactly one interval, and satisfaction operators @i indexed by nominals and stating that a formula is true in an interval in which a nominal i holds. Intuitively, a nominal labels a single interval and an @i operator enables us to access the interval labelled by i.

Referentiality seems to be an important property for a number of applications but it is not clear whether it is expressible in Horn fragments of HS. In [Wał˛ega, 2017] I have proposed adding hybrid machinery, i.e., nominals (denoted by i added to the superscript of fragment's symbol) as well as nominals and @ operators (denoted by i, @ added to the superscript) to HS fragments and to analyse the obtained extensions. The lattice including all these fragments is depicted in Figure 1. My main result concerns computational complexity of HS ✷,i,@ horn and is as follows.

Theorem ([Wał˛ega, 2017]) The satisfiability problems of HS ✷,i,@ horn and HS ✷,i horn are NP-complete under (Den,<,S), (Den,<,Non-S), (Dis,≤,Non-S), (Den,≤,S), and (Den,≤,Non-S) semantics.

The theorem shows that adding hybrid machinery to HS ✷horn has a price of moving from P-completeness to NPcompleteness, and thus sheds more light on the interplay between expressiveness and computational complexity of HS fragments. As future work I plan to:

• Investigate computational complexity of other HS fragments. For instance, one of the unsolved problems is determining computational complexity of HS ✷horn under (Dis,≤,S). At the moment it is not even known if it is decidable;
• Study expressiveness of HS fragments. The fragments are intensively scrutinized in terms of their computational complexity but there is hardly any research on their expressiveness;
• Search for application domains appropriate for HS fragments and their hybrid versions.

Acknowledgments

This work is supported by the NCN grant DEC2011/02/A/HS1/00395.