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

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.

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 hAi [x, y]RA[z, t] ⇔ y = z hLi

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

t t t 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 ultimatelyperiodic 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 X1X2 . . . Xk, whose formulas are defined by the grammar:

ϕ ::= p | ¬ϕ | ϕ ∧ ϕ | hX1iϕ | . . . | hXkiϕ. 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) 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] M, [x, y] M, [x, y] M, [x, y] p iff [x, y] ∈ V (p), for p ∈ AP, ¬ψ iff M, [x, y] 6 ψ, ψ ∧ γ iff M, [x, y] ψ and 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, 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.

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 branchingtime 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 specifications 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 .