=Paper=
{{Paper
|id=Vol-2785/paper2
|storemode=property
|title=A Note on Ultimately-Periodic Finite   Interval Temporal Logic Model Checking
|pdfUrl=https://ceur-ws.org/Vol-2785/paper2.pdf
|volume=Vol-2785
|authors=Dario Della Monica,Angelo Montanari,Guido Sciavicco,Ionel Eduard Stan
|dblpUrl=https://dblp.org/rec/conf/overlay/MonicaMSS20
}}
==A Note on Ultimately-Periodic Finite   Interval Temporal Logic Model Checking==
<pdf width="1500px">https://ceur-ws.org/Vol-2785/paper2.pdf</pdf>
<pre>
                                                   Proceedings of the
      2nd Workshop on Artificial Intelligence and Formal Verification, Logics, Automata and Synthesis (OVERLAY),
                                                   September 25, 2020




               A Note on Ultimately-Periodic Finite
             Interval Temporal Logic Model Checking∗

    Dario Della Monica1 , Angelo Montanari2 , Guido Sciavicco3 , and Ionel Eduard Stan4
                                         1
                                       University of Udine, Italy
                                         2
                                       University of Udine, Italy
                                     3
                                       University of Ferrara, Italy
                       4
                         University of Ferrara and University of Parma, Italy
                                        1
                                         dario.dellamonica@uniud.it
                                         2
                                           angelo.montanari@uniud.it
                                          3
                                            guido.sciavicco@unife.it
                                         4
                                           ioneleduard.stan@unife.it



                                                     Abstract


                In this paper, we deal with the ultimately-periodic finite interval temporal logic
            model checking problem. The problem has been shown to be in PTIME for full
            Halpern and Shoham’s interval temporal logic (HS for short) over finite models,
            as well as for the HS fragment featuring a modality for Allen relation meets and
            metric constraints over non-sparse ultimately-periodic (finite) models, that is, over
            ultimately-periodic models whose representation is polynomial in their size. Here,
            we generalize the latter result to the case of sparse ultimately-periodic models.


1     Introduction
In its standard formulation, model checking (MC) is the problem of verifying if a formula is satisfied by a
given model [10]. Usually, the model is the abstract representation of a system, whose basic properties are
expressed by proposition letters, and the formula specifies a complex property of the system to be checked
and is written in a temporal logic. The most commonly adopted ontology for both the model and the
logic is point-based: systems are represented as Kripke structures, whose vertices are the states of the
system, atomic properties are descriptions of states, and the underlying logic is a point-based temporal
logic, such as LTL, CTL, and the like [9, 19].
    As interval-based temporal logics emerged as a possible alternative to point-based ones, the concept of
interval temporal logic model checking (IMC) came into play. Halpern and Shoham’s interval temporal logic
HS [13], which features one modality for each Allen relation [1], is the most representative interval-based
temporal logic, and its model checking problem is the one that received the most attention.
    The model checking problem for full HS over finite Kripke structures, under the homogeneity assumption,
has been addressed in [17]. A systematic investigation of the problem for a number of HS fragments has
   ∗ The authors acknowledge the partial support by the Italian INdAM-GNCS project Ragionamento Strategico e Sintesi

Automatica di Sistemi Multi-Agente.
                 Copyright © 2020 for this paper by its authors.
                 Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
12                                                      D. Della Monica, A. Montanari, G. Sciavicco, I.E. Stan


                                                                    x               y
                                                                                    z       t
                            hAi   [x, y]RA [z, t] ⇔ y = z
                                                                                        z       t
                            hLi   [x, y]RL [z, t] ⇔ y < z
                                                                    z t
                            hBi   [x, y]RB [z, t] ⇔ x = z, t < y
                                                                                z t
                            hEi   [x, y]RE [z, t] ⇔ y = t, x < z
                                                                        z       t
                            hDi   [x, y]RD [z, t] ⇔ x < z, t < y
                                                                            z               t
                            hOi   [x, y]RO [z, t] ⇔ x < z < y < t


                   Table 1: Allen’s interval relations and corresponding HS modalities.


been pursued in a series of subsequent contributions [2, 3, 4, 5, 18]. Moreover, the model checking problem
for some HS fragments extended with epistemic operators has been studied in [14, 15, 16].
    In this paper, we focus on the problem of model checking an interval temporal logic formula against a
single (finite) model. The problem of checking a finite, linear (and fully represented) interval model against
HS formulas (FIMC problem) was originally formulated in [11]. Its generalization to infinite, periodical
models was proposed in [12] for a meaningful fragment of HS. The latter problem, called ultimately-
periodic finite interval model checking problem (UP-FIMC problem), takes Metric Right Propositional
Neighborhood Logic (MRPNL for short) as its specification languages. MRPNL is a fragment of HS that
only encompasses a modality for Allen relation meets and some metric constraints (definable in HS) [6].
    The most relevant technical problem with FIMC and UP-FIMC is related to the so-called sparsity of
finite models. In both FIMC and UP-FIMC, an interval model is assumed to be fully represented, but its
representation may turn out to be logarithmic in the size of the model (unlike the classical MC problem,
where Kripke or Kripke-like models are always represented polynomially in their size). While such an
issue has been successfully solved for full HS and finite (non-periodic) models [11] (the FIMC problem has
been proved to be in PTIME even for sparse models), the UP-FIMC problem for MRPNL has been shown
to be in PTIME [12] only for non-sparse ultimately-periodic models. Here, we show that such a restriction
can be removed, proving that the UP-FIMC problem for MRPNL is in PTIME for sparse models as well.


2     HS and MRPNL
Let D = hD, <i be a linearly ordered set. An interval over D is an ordered pair [x, y], where x, y ∈ D
and x < y. Let I(D) be the set of all intervals over D. Excluding equality, there are 12 possible relations
between two intervals in a linear order, often called Allen’s relations [1]: the 6 relations depicted in
Table 1 and their inverses. By treating sets of intervals as Kripke structures, with Allen’s relations as their
accessibility relations, we can associate a modality hXi with each Allen relation RX . For each modality
hXi, its transpose hXi corresponds to the inverse RX of RX , i.e., RX = (RX )−1 . HS is a multi-modal
logic with formulas built over a set AP of proposition letters, the Boolean connectives ∧ and ¬, and the
set of modalities for Allen’s relations. With each subset of Allen’s relations {RX1 , . . . , RXk }, we associate
the HS fragment X1 X2 . . . Xk , whose formulas are defined by the grammar:

                                  ϕ ::= p | ¬ϕ | ϕ ∧ ϕ | hX1 iϕ | . . . | hXk iϕ.
where p ∈ AP. The other Boolean connectives, e.g., ∨ and →, and the dual modalities [X] are defined as
usual, e.g., [A]ϕ ≡ ¬hAi¬ϕ.
    An interval model is a pair M = hI(D), V i, where D is a linearly ordered set (domain of M ) and
V : AP → 2I(D) is a valuation function, that assigns to each proposition letter p ∈ AP the set of intervals
V (p) on which it holds. Let M be an interval model. We denote by DM (resp., VM ) its domain (resp.,
valuation function). We define the size, or cardinality, of M as the cardinality of DM , and denote it by NM
(subscripts are omitted when clear from the context). Even if interval temporal logics have been studied
over several classes of linearly ordered sets, we assume here every domain D to be either N (infinite case)
Interval Temporal Logic Finite Model Checking                                                                    13


or a prefix of it (finite case, that is, D = {0, 1, . . . , |D| − 1}). With a little abuse of notation, we sometimes
use M to refer to the set of its intervals, i.e., we write [x, y] ∈ M for [x, y] ∈ I(D). The semantics of HS
formulas is given in terms of interval models, that is, the truth of a formula ϕ on an interval [x, y] of an
interval model M is defined by structural induction on formulas:

                      M, [x, y]   p        iff [x, y] ∈ V (p), for p ∈ AP,
                      M, [x, y]   ¬ψ       iff M, [x, y] 6 ψ,
                      M, [x, y]   ψ∧γ      iff M, [x, y] ψ and M, [x, y] γ,
                      M, [x, y]   hXiψ     iff ∃[z, t] s.t. [x, y]RX [z, t] and M, [z, t]   ψ.
We write M      ϕ for M, [0, 1]    ϕ.
    Among the many fragments of HS, a particularly significant one is Propositional Neighborhood Logic
(PNL, for short). PNL has only two modalities hAi and hAi corresponding to Allen’s relations meets
and met by, respectively, and its satisfiability problem, unlike that of HS and of most of its fragments, is
decidable [7]. Moreover, its syntax can be easily extended with metric capabilities without losing its good
computational properties. The resulting logic, known as Metric Propositional Neighborhood Logic (MPNL),
features modalities hAi and hAi, and, for each natural number k, a pre-interpreted modal constant len<k ,
called length constraint [6]. In [8], it has been shown that MPNL is a fragment of HS, as length constraints
can be defined, in polynomial space, by means of modality hBi (or modality hEi). The future fragment of
MPNL, called MRPNL, consists of the formulas generated by the following grammar:

                                        ϕ ::= len<k | p | ¬ϕ | ϕ ∧ ϕ | hAiϕ,
where p ∈ AP and k ∈ N. The other Boolean connectives and the logical constants, as well as the universal
modality [A], are defined in the standard way. Hereafter, given an MRPNL formula ϕ, we denote by ξϕ
(or, simply, ξ) the greatest constant k that occurs in a length constraint len<k in ϕ. MRPNL is interpreted
on discrete interval models by enriching the HS satisfaction relation with the following clause:

                                          M, [x, y]   len<k iff y − x < k.


3     Finite and ultimately-periodic model checking
Definition 1 (FIMC [11]). Given a pair (M, ϕ), where M is a finite interval model and ϕ is an HS
formula, the finite interval model checking problem (FIMC) consists in deciding whether M, [0, 1] ϕ.

    It is quite straightforward to devise a simple algorithm for FIMC whose running time is polynomial in
the cardinality N of the model M (and in the size of the formula). Thus, if we can guarantee that the size
of the representation of the model is at least linear in its cardinality, then we can conclude that FIMC
is in PTIME. However, this is not in the case in general. As an example, consider the class of models
M = h{0, 1, . . . , N − 1}, V i, for N ∈ N, and where V (p) = {[N − 2, N − 1]} and p is the only proposition
letter. The representation of each model M requires space logarithmic in the cardinality N of M , in order
to represent the cardinality N , in binary, and to capture the valuation of the only proposition letter p,
which holds over the interval [N − 2, N − 1] only. In order to check, e.g., the formula hAihAip against a
model M in the above-defined class, the aforementioned simple algorithm would require labeling with
hAip all intervals [x, N − 1], with 1 ≤ x < N − 2, whose number is linear in N , and thus exponential in
the size of the representation of M .
    The cornerstone of the above argument is that not all the points of a model are explicitly represented:
a point x such that, for all y, none of the intervals [x, y] and [y, x] satisfies any proposition letter is not
explicitly represented. We call these points useless. On the contrary, points that are explicitly represented
are called useful. Since the domain of a finite model is a prefix of N, a representation of one such model
consists of an integer, expressed in binary, representing its cardinality, and, for each proposition letter, a
list of intervals where the proposition holds true. Thus, the size of the representation of a finite model
is logarithmic in its cardinality and polynomial in the number of useful points. A class of models is
non-sparse if, for every model, the number of useful points is at least linear in the cardinality; otherwise,
14                                                 D. Della Monica, A. Montanari, G. Sciavicco, I.E. Stan


the class is said to be sparse. As we have already pointed out, it is easy to devise a straightforward
algorithm solving FIMC in polynomial time when we restrict to a non-sparse class of models. However,
the class of models defined above is sparse, as the number of useful points is constant, and therefore the
algorithm runs in exponential time.
    In [11], the authors show that every instance (M, ϕ) of FIMC, with M ranging over a sparse class of
models, can be turned into a new one, (M 0 , ϕ), where M 0 ranges over a non-sparse class of models and such
that M, [0, 1] ϕ if and only M 0 , [0, 1] ϕ [11, Lemma 2]. Intuitively, this is done by first establishing a
suitable upper bound to the size of gaps, i.e., maximal blocks of adjacent useless points, occurring in a
model. Such an upper bound provides a maximum to the ratio between the number of useless and useful
points or, equivalently, establishes a linear correspondence between the number of useful points and the
cardinality of a model, thus identifying a non-sparse class of models. Then, a transformation is defined
that makes it possible to shrink the gaps so to keep their size below the upper bound. In other words, if
a model contains a gap that exceeds the upper bound, it can be turned into a new one whose gaps are
small enough. Finally, it is shown that the transformation always produces a model that is bisimilar to
the original one (and thus the two models satisfy the same set of formulas) [11, Lemma 1]. Since the
transformation can be done in polynomial time, FIMC can be solved in polynomial time by applying the
aforementioned straightforward model checking algorithm.
Theorem 1 ([11]). FIMC is in PTIME.
    The finite interval MC problem only deals with finite interval models, which can be seen as finite,
complete pieces of information. However, a finite model can also be thought of as an incomplete object,
e.g., a prefix of an infinite model. The notion of ultimately-periodic model aims at formalizing this idea:
an ultimately-periodic model is an infinite model that is finitely represented as a finite model that embeds
a period; by repeating the period an infinite number of times, the finite model is extended into an infinite
one. Thus, we can generalize the notion of MC to the case of ultimately-periodic models. However, due
to several technicalities related with the periodicity, at the moment we are only able to deal with the
fragment MRPNL of HS.
Definition 2 (UP-FIMC [12]). Given a pair (M, ϕ), where M is a finite interval model and ϕ is a
formula of MRPNL, the ultimately-periodic interval model checking problem (UP-FIMC) is the problem
of enumerating the natural numbers P such that M can be extended, by repeating an infinite number of
times its suffix of length P , into an infinite ultimately-periodic M that satisfies ϕ, i.e., M, [0, 1] ϕ.
     The UP-FIMC problem has been addressed in [12] for non-sparse classes of models.
Theorem 2 ([12]). UP-FIMC over non-sparse classes of models is in PTIME.
    In order to generalize Theorem 2 to sparse classes of models, it is possible to use an argument similar
to the one used in [11]. The additional difficulties are given by the finite input model being conceptually
divided into a prefix and a period. This basically means that (i) we need to be careful to only shrink gaps
contained in either the prefix or the period (i.e., avoid shrinking gaps spanning both prefix and period)
and (ii) when shrinking a gap in the period, we obtain an infinite ultimately-periodic model whose period
has also been shrunk. In order to properly deal with the former issue, it is enough to double the upper
bound for gaps used in [11]: indeed, if a gap of size at least 2B exists, then we are sure that a gap of
size at least B exists that is contained either in the prefix or in the period. As for the latter issue, we
need to introduce a stronger notion of equivalence than the bisimilarity exploited in [11]; more precisely,
given an instance (M, ϕ) of UP-FIMC, with M ranging over a sparse class of models, we produce a new
instance (M 0 , ϕ), where M 0 ranges over a non-sparse class of models, along with an invertible function
f : N → N, such that if M can be extended, by repeating an infinite number of times its suffix of length P ,
into an infinite ultimately-periodic M that satisfies ϕ, then M 0 can be extended, by repeating an infinite
number of times its suffix of length f (P ), into an infinite ultimately-periodic M0 that satisfies ϕ. Since f
is invertible, we can transform the instance (M, ϕ) into (M 0 , ϕ), run the algorithm from [12] over (M 0 , ϕ),
and then apply the inverse f −1 of f to the output to obtain, in polynomial time, a solution to the original
instance (M, ϕ), as stated in the following theorem.
Theorem 3. UP-FIMC is in PTIME.
Interval Temporal Logic Finite Model Checking                                                          15


References
 [1] J. F. Allen. Maintaining knowledge about temporal intervals. Comm. of the ACM, 26(11):832–843,
     1983.
 [2] L. Bozzelli, A. Molinari, A. Montanari, and A. Peron. Model checking interval temporal logics with
     regular expressions. Inf. Comput., 272:104498, 2020.
 [3] L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. Satisfiability and model checking for
     the logic of sub-intervals under the homogeneity assumption. In Proc. of the 44th ICALP, volume 80
     of LIPIcs, pages 120:1–120:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
 [4] L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. Model checking for fragments of
     the interval temporal logic HS at the low levels of the polynomial time hierarchy. Inf. Comput.,
     262(Part):241–264, 2018.
 [5] L. Bozzelli, A. Molinari, A. Montanari, A. Peron, and P. Sala. Which fragments of the interval
     temporal logic HS are tractable in model checking? Theor. Comput. Sci., 764:125–144, 2019.
 [6] D. Bresolin, D. Della Monica, V. Goranko, A. Montanari, and G. Sciavicco. Metric propositional
     neighborhood logics on natural numbers. Soft. and Sys. Mod., 12(2):245–264, 2013.
 [7] D. Bresolin, D. Della Monica, A. Montanari, P. Sala, and G. Sciavicco. Interval temporal logics over
     strongly discrete linear orders: Expressiveness and complexity. Theor. Comp. Sci., 560:269–291, 2014.
 [8] D. Bresolin, P. Sala, and G. Sciavicco. On begins, meets, and before. Int. J. Found. Comp. Sci.,
     23(3):559–583, 2012.
 [9] E. M. Clarke and E. A. Emerson. Design and synthesis of synchronization skeletons using branching-
     time temporal logic. In Proc. of the 1981 Workshop on Logics of Programs, volume 131 of LNCS,
     pages 52–71, 1981.
[10] E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT Press, 2002.
[11] D. Della Monica, D. de Frutos-Escrig, A. Montanari, A. Murano, and G. Sciavicco. Evaluation of
     temporal datasets via interval temporal logic model checking. In Proc. of the 24th TIME, pages
     11:1–11:18, 2017.
[12] D. Della Monica, A. Montanari, A. Murano, and G. Sciavicco. Ultimately-periodic interval model
     checking for temporal dataset evaluation. In Proc. of the 5th Global Conference on Artificial
     Intelligence (GCAI), volume 65 of EPiC Series in Computing, pages 28–41, 2019.
[13] J. Halpern and Y. Shoham. A propositional modal logic of time intervals. J. ACM, 38(4):935–962,
     1991.
[14] A. Lomuscio and J. Michaliszyn. An epistemic Halpern-Shoham logic. In Proc. of the 23rd IJCAI,
     pages 1010–1016, 2013.
[15] A. Lomuscio and J. Michaliszyn. Decidability of model checking multi-agent systems against a class
     of EHS specifications. In Proc. of the 21st ECAI, pages 543–548, 2014.
[16] A. Lomuscio and J. Michaliszyn. Model checking multi-agent systems against epistemic HS specifica-
     tions with regular expressions. In Proc. of the 15th KR, pages 298–308, 2016.
[17] A. Molinari, A. Montanari, A. Murano, G. Perelli, and A. Peron. Checking interval properties of
     computations. Acta Inf., 53(6-8):587–619, 2016.
[18] A. Molinari, A. Montanari, and A. Peron. Model checking for fragments of Halpern and Shoham’s
     interval temporal logic based on track representatives. Inf. Comput., 259(3):412–443, 2018.
[19] A. Pnueli. The temporal logic of programs. In Proc. of the 18th FOCS, pages 46–57, 1977.

</pre>