A model checker for interval temporal logic over nite structures?

Abstract

Model checking is the process of establishing whether a certain formula is satis ed by a given structure, and it is usually associated with point-based temporal logics. Recently, the question of how to correctly de ne and study the model checking problem for interval-based temporal logics has been raised. In this paper, we focus on a very natural nite version of the model checking problem for Halpern and Shoham's modal logic of time intervals, a.k.a. HS, for which an algorithm that behaves in a very e cient way (under certain conditions) can be designed. We present an implementation of such an algorithm and analyse its performance through a systematic series of tests.

-

Model checking is the problem of verifying whether a given logical formula is satis ed by a certain structure. It has been extensively studied in the area of formal methods and automated veri cation as a technique to establish the correctness of (hardware and software) reactive systems with respect to certain properties of interest. In most cases, the property to be veri ed is expressed in some point-based temporal logic, such as LTL [ 24 ], CTL [ 9 ], and CTL [ 12 ]. The main reason is that the behavior of a (reactive) system is usually captured by specifying how its states can possibly evolve during an execution, and thus it is naturally represented as a labeled directed graph, where vertices represent the states of the system, edges encode its transitions, and paths describe executions. Interesting properties predicate about points (states) along a timeline (execution), which makes point-based temporal logics a natural choice for the speci cation formalism.

In the last years, however, a certain interest is emerging towards model checking for temporal logics with an interval-based semantics, in particular for Halpern and Shoham's logic HS [ 13 ], which plays a prominent role in the literature about interval-based temporal logics, along with its fragments. HS can be viewed as the logic of Allen's relations [ 2 ]. While some of its theoretical properties, such as satis ability and expressiveness, have been already studied in a very systematic way (see, for instance, [ 1, 8 ]), its model checking problem has entered the research agenda only recently, despite it has several potential application domains, as shown in [ 22 ].

Model checking for full HS, interpreted over nite Kripke structures, according to the so-called state-based semantics [ 6 ], has been studied in [ 18, 23 ]. The authors showed that, under the homogeneity assumption [ 25 ], which constrains a proposition letter to hold over an interval if and only if it holds over each component state, the problem is non-elementarily decidable (EXPSPACE-hardness has been later shown in [ 5 ]). Since then, the attention has been brought to HS fragments, whose computational behavior is often much better [5, 7, 19{21]. The model checking problem for some HS fragments extended with epistemic operators has been investigated in [ 15, 16 ]. The semantic assumptions for these epistemic HS fragments di er from those of [5, 7, 18{21, 23] in two important respects, making it di cult to compare the two families of logics: formulas are interpreted over the unwinding of the Kripke structure (computation-tree-based semantics [ 6 ]) and interval labeling takes into account only the endpoints of intervals. The latter assumption has been later relaxed by allowing the use of regular expressions to de ne the labeling of proposition letters over intervals in terms of the component states [ 17 ]. An in-depth investigation of interval temporal logic model checking with regular expressions, under the homogeneity assumption, has been recently undertaken [ 3, 4 ].

In this paper, we focus our attention on the problem of model checking a single, nite path/interval. Unlike standard model checking, where logical speci cations are evaluated against temporal structures which are abstract ( nite) representations of the in nite set of nite/in nite computation paths of a system, we are interested in checking the truth of a formula against a concrete, nite interval model. In [ 22 ], it has been shown that such a problem has various interesting applications, such as, for instance, temporal query evaluation and temporal constraint checking in temporal databases [ 10, 14, 26, 27 ].

We describe an implementation of a model checker for HS formulas against concrete, nite interval models, and we report the outcomes of a series of systematic performance tests. Even though the proposed implementation is inspired by the well-known model checking algorithm for CTL formulas by Emerson and Clarke [ 11 ], devising an e cient procedure is not trivial at all and it requires a deep theoretical analysis as well as suitable choices in representing and searching the nite model, e.g., a symbolic representation is used when labeling intervals with special kinds of formulas (see [ 22 ] for a more detailed discussion). hAi hLi hBi hEi hDi hOi 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 :, and 6 existential modalities based on the following 6 Allen's relations: meets (modality hAi), begins (modality hBi), and ends (modality hEi), graphically depicted in Figure 1, and their transposes met-by (modality hAi), begun-by (modality hBi), and ended-by (modality hEi). Formulas of HS are de ned by the following grammar: ' ::= p j :' j ' ^ ' j ' _ ' j hAi' j hAi' j hBi' j hBi' j hEi' j hEi': The other Boolean connectives are de ned as usual, while the universal version of each existential modality hXi is denoted by [X] and de ned as [X] :hXi: . The language of HS allows for additional (existential) modalities corresponding to the other Allen's relations, namely, during (modality hDi), later (modality hLi), and overlaps (modality hOi), graphically depicted in Figure 1, and their transposes contains (modality hDi), before (modality hLi), and overlapped-by (modality hOi), which can be de ned as follows: hDi hLi hOi hBihEi , hAihAi , hEihBi , hDi hLi hOi hBihEi , hAihAi , hBihEi .

Hereafter, we denote by RX the Allen relation corresponding to modality hXi, e.g., we denote by RA the relation corresponding to modality hAi (see Figure 1).

Let D = hD; <i be a nite linearly ordered set. An interval over D is an ordered pair [x; y], where x; y 2 D and x < y (strict semantics). An interval of the type [x; x +1] is called unit (x+1 denotes the immediate successor of x in D). The semantics of HS is given in terms of interval models M = hI(D); V i, where I(D) is the set of all intervals over D and V : AP 7! 2I(D) is a valuation function that assigns to every p 2 AP the set of intervals V (p) over which p holds. Since every nite linear order is isomorphic to a pre x of the set N of the natural numbers, for every N 2 N we denote the linear order D = f0; 1; : : : ; N 1g by [N ]. The truth relation of an HS formula over a given interval [x; y] in an interval model M is de ned by structural induction on formulas as follows: { M; [x; y] p i [x; y] 2 V (p); { Boolean connectives are dealt with in the standard way; { M; [x; y] hAi' i there exists z > y such that M; [y; z] '; { M; [x; y] hAi' i there exists z < x such that M; [z; x] '; { M; [x; y] hBi' i there exists x < z < y such that M; [x; z] { M; [x; y] hBi' i there exists z > y such that M; [x; z] '; { M; [x; y] hEi' i there exists x < z < y such that M; [z; y] { M; [x; y] hEi' i there exists z < x such that M; [z; y] '. '; '; We say that an HS formula ' is satis able if and only if there exists a model M and an interval [x; y] such that M; [x; y] '. The satis ability problem for HS is the problem of nding a model and an interval that satis es a formula.

Given an interval model M = hI(D); V i over a nite linearly ordered set D = hD; <i, an interval [x; y] in M , and an HS formula ', the problem of checking ' against [x; y] in M ( nite (concrete) model checking, model checking for short) consists in establishing whether or not M; [x; y] '.

In the rest of the paper, we make use of the following two shortcuts: the global modality [U ] , that forces to hold everywhere in the model, and the strong intersect modality hSIi, that forces to hold on some interval [z; t], distinct from the current interval [x; y], such that at least one w 2 fz; : : : ; tg falls inside [x; y]. Their formal de nitions are given in Figure 1. 3

A model checking algorithm for HS

In this section, we present the algorithm for model checking HS formulas against (concrete) nite intervals/models [ 22 ].

Data structures for representing the input. The algorithm receives as input an instance of the model checking problem, that is, a pair consisting of an HS formula and an interval model.

An HS formula can be represented as a binary rooted decorated tree. A rooted tree is a triple G = (V; E; r), where (V; E) is a directed acyclic graph and r 2 V is a distinguished vertex, called root of G, such that there is exactly one incoming edge for each vertex except for the root, which has none, that is, f(u; r) j u 2 Eg = ; and jf(u; v) j u 2 Egj = 1, for each v 2 V n frg. Vertices of a tree are also called nodes. A rooted decorated tree is a rooted tree equipped with a function that associates a decoration with each node. A decoration is either a proposition letter or an operator, which, in turn, is either a Boolean or a modal input model conceptual representation

internal representation operator. For each edge (v; u) 2 E, we say that u is a child of v. We focus on binary trees, that is, trees in which each node has at most 2 children, which we refer to as its left and its right child. If a node has only one outgoing edge, then its right child is unde ned. Nodes without children are called leaves.

As a preliminary step, the algorithm transforms the input formula into an equivalent one belonging to the language generated by the grammar in Section 2, that is, a formula only containing negations, disjunctions, conjunctions, and existential modalities from the set fhAi; hBi; hEi; hAi; hBi; hEig, and, then, it stores the resulting formula into a tree-like structure.

An input model M is represented by a string carrying the following pieces of information: a number, that speci es the size (number of points) of the linear order, and, for each proposition letter, a list of intervals encoding the valuation function (Figure 2, top). Input models are stored in a linear array A of pointers (Figure 2, bottom), whose elements correspond to intervals, in ascending order with respect to their second coordinate and, if their values on the second coordinate is the same, with respect to their rst coordinate. In Figure 2, the rst (resp., second, third) element of A corresponds to the interval [0; 1] (resp., [0; 2], [1; 2]), and so on. This is a classic representation of an upper triangular matrix, that re ects the intrinsic structure of an interval model. At the beginning, each element of A contains (points to) those proposition letters that hold at the corresponding interval, that is, A represents the valuation function V of M . Then, the algorithm will associate with each element of A the set of pointers to the subtrees of the formula tree that `hold' in the corresponding interval.

Figure 2 shows a model, based on the linear order D = f0; 1; 2; 3; 4g, which features the set of proposition letters AP = fp; qg. At the top, the unstructured input model is given. Such an unstructured model corresponds to the conceptual one shown in the middle of the picture. The internal representation of the model is depicted at the bottom.

proc ModelCheck (A; T (')) >8for each T ( ) subtree of T (') <> foCrheeackch(T((0 ); Ai; i)N (N2 1) 1) >>:return (T (') 2 A[0]) proc Check (T ( ); A; i) 8if (Op(T ( )) 2 f:; _; ^g) >>> then >>>8if (Op(T ( )) = : and Left(T ( )) 2= A[i]) >>>>>>>>> then A[i] = A[i] [ fT ( )g >><>if (Op(T ( )) = ^ and Left(T ( )) 2 A[i] and Right(T ( )) 2 A[i]) <>>>>>>>ift(hOepn(TA([i])=)=A_[i]a[nfdT((Le)fgt(T ( )) 2 A[i] or Right(T ( )) 2 A[i])) >>>>>>>>:elstehen A[i] = A[i] [ fT ( )g >>>8for each (j 2 I(i; Op(T ( )); N)) >>>>>>:<: ift(hLeenftA(T[i(] =))A2[i]A[[jf])T ( )g

Execution. Following Clarke and Emerson's schema [ 9 ], model checking a given HS formula (represented as a binary tree) against a certain model (represented as an array of sets of pointers to trees) can be done by a simple procedure that executes a bottom-up visit of the formula tree.

Let ' be the formula to be checked and, for each subformula , let T ( ) be the corresponding subtree. Moreover, let M = h[N ]; V i be the model against which ' is to be checked. The size of the array A used to store M is equal to the number of intervals featured by M , namely, N (N2 1) . For each i 2 f0; : : : ; N (N2 1) 1g, let us denote by Int(i) the interval corresponding to the i-th position in A. As an example, we denote by Int(2) the interval [1; 2] (see Figure 2). For a binary tree T that represents a formula, we denote by Op(T ) the decoration of the root of T , and we denote by Lef t(T ) (resp., Right(T )) the subtree rooted in its left (resp., right) child.

We de ne a function I that, for any position i in A and any modality hXi, returns the set of positions corresponding to intervals [z; t] such that Int(i)RX [z; t]. Besides the position i and the modality hXi, I clearly depends on the size N of the underlying linear order:

I : N fA; B; E; A; B; Eg

N ! 2N.

As an example, with reference to the model depicted in Figure 2, where N = 5, we have that I(2; A; 5) = f5; 8g.

In Figure 3, we provide the pseudo-code of the model checking procedure, and then, in Figure 4, we show the result of checking the formula ' hAi(hBip ^ q) against the model in Figure 2.

Theoretical complexity and optimization. In [ 22 ], Della Monica et al. have shown that the problem of checking an HS formula against a nite (concrete) interval model can be solved by a deterministic algorithm that runs in polynop hBi ^ hAi q A : mial time in the size of the input. The execution time of our implementation of the model checking procedure is polynomial in the size of the representation of the input formula, but it is not necessarily polynomial in the size of the representation of the model (this is the case with some particular input models).

Classic model checking, e.g., LTL and CTL model checking, where in nite paths are nitely encoded in the input structure, is in nite in nature. In our setting, as shown in Figure 2, models can be compactly represented by specifying the size (number of points) of the underlying domain and then listing, for each proposition letter, the set of intervals over which it holds. The fundamental di erence between the two frameworks is that, in classic model checking, frame information, i.e., states and transitions, must be explicitly represented in the input, while, in our setting, frame information, i.e., intervals and their relations, is implicit in the size of the temporal domain, as the relations among intervals are induced by the underlying linear order. As a consequence, while the size of the representation of a Kripke structure is polynomial in the number of states and labels, the size of the representation of a nite interval model may be logarithmic in the number of intervals.

As an example, consider an interval model M = h[N ]; V i over AP = fpg, with V (p) = f[N 1; N ]g. Its representation consists of the number N , whose binary encoding takes space O(log(N )), and the mapping p 7! f[N 1; N ]g, which takes space O(log(N )) as well, as it su ces to represent two numbers. In [ 22 ], it has been shown that such degenerate instances can be reduced in polynomial time to non-degenerate, equivalent ones, making it possible to e ciently employ the proposed algorithm to model check any instance.

To improve the performance of the algorithm, we devised a non-trivial heuristics that exploits a suitable form of `lemma caching'. It makes use of a complex data structure, denoted here by S, which can be seen as a hash table (accessible in constant time) that, for each already-visited subtree T ( ), keeps track of the set of positions S(T ( )) in A corresponding to intervals where is true. e d i s t f e L t a o B e d i s t h g i R

By construction, S(T ( )) is unde ned if T ( ) has never been visited before. At each iteration, before checking a generic subtree T ( ), the procedure makes the following steps: 1. if = , that is, if and are two occurrences of the same sub-formula, for some such that S(T ( )) is de ned, then, for each index i, we add to A[i] a pointer to T ( ) if and only if i 2 S(T ( )); 2. otherwise, if Op(T ( )) is a modality and jS(Lef t(T ( )))j = 0, then no pointer to T ( ) is added to any cell of A.

Notice that whenever any of the above conditions applies, executing the entire check for T ( ) takes precisely one pass over A instead of two. 4

Experimental analysis

In this section, we describe the outcomes of a set of systematic experiments to test the e ectiveness of our implementation. To start with, we consider the well-known riddle wolf, goat, and cabbage, which can be described as follows. A farmer wants to cross a river and take with him a wolf, a goat, and a cabbage. There is a boat that can t himself plus either the wolf, the goat, or the cabbage, and the following constraints apply: if the wolf and the goat are alone on one shore, the wolf will eat the goat, and if the goat and the cabbage are alone on the shore, the goat will eat the cabbage. The problem asks to nd a plan so that the farmer can bring the wolf, the goat, and the cabbage safely across the river. This problem can be easily described in HS, using proposition letters that represent the localization (left hand side of the river, right hand side of the river, or the boat) of the farmer, the wolf, the goat, and the cabbage at each time. A model that solves the problem is represented in Figure 5.

To test our implementation, we designed a generalized version of the abovedescribed riddle with n characters (or elements) and m rivers. In this version, the (single) farmer must cross every element e1; : : : ; en from the left side of the i-th river to its right side using a boat that may host, at most, n 2 elements at the same time, plus the farmer. The main constraints of the system are: (i) for each j, ej \eats" ej+1 (if any), and (ii) the relation \eats" is not transitive. Clearly, to keep the meaning of the original riddle unchanged, the farmer must bring everyone across all rivers, sequentially (no river can be skipped). We give a formalization of this generalized version of the problem in HS, which makes use of the following proposition letters: { for i 2 f0; : : : ; mg; f i;S represents the situation where the farmer is on some river side: f 0;S means that the farmer is on the left side of the 1st river, f m;S means that the farmer is on the right side of the m-th river, and f i;S , with 1 i < m, means that the farmer is on the right side of the i-th river (and on the left side of the (i + 1)-th one); analogously, proposition letters eij;S , with i 2 f0; : : : ; mg and j 2 f1; : : : ; ng, represent the situation where the j-th element is on some river side; { for i 2 f1; : : : ; mg; f i;B represents the situation where the farmer is on a boat crossing the i-th river; analogously, proposition letters eij;B, with i 2 f1; : : : ; mg and j 2 f1; : : : ; ng, represent the situation where the j-th element is on a boat crossing the i-th river.

The problem can be encoded in HS as follows. First of all, we introduce a formula 'boat, which states that if anyone is on the boat, then the farmer must be as well, and a formula 'safe, which prevents two incompatible elements from being alone (unguarded) on the same side of a river: 'boat 'safe [U ] Vi;j (eij;B ! f i;B); [U ] Vi;j ((eij;S ^ eij;+S1 ^ :f i;S ) ! ?): Next, we need to force some obvious physical constraints: 'phy 8> [U ] Vi>0;j (eij;S ! (hLieij;B _ hAieij;B)); ><>>>>> [[UU ]] VVii;>j0(e(fij;Bi;S!!(h(LhLieifij i;1B;S__hhAAiifeiij;B1);)S;)); >>>>>>>: [[[UUU ]]] VVViii;;(jf;(if(;Bei;ij;!!!(hVLVii0i;f0;i0 0:1:h;SShSI_IifiheAi0ij;0i;f00)i):;1;S )); (i) (ii) (iii) (iv) (v) (vi) 1;200 1;000 . 800 s m n i e 600 m i T 400 200 0 0

Experiments Interpolating parabola three rivers four rivers ve rivers one river

two rivers 200 400 600 800 1;000 1;200 1;400 1;600 1;800 2;000

Input size

Formulas (i) and (ii) impose that the farmer, as well as any element, has been on the boat on the i-th river before being on the right hand side of that river. Similarly, formulas (iii) and (iv) state that the farmer, as well as any element, must have been on the left hand side of the i-th river before being on the boat across it. Furthermore, formulas (v) and (vi) constrain the model to be coherent: whenever any element or the farmer are somewhere, they are not anywhere else.

Finally, we add a formula 'riddle (the riddle constraint) which states that the capacity of the boat is limited (as in the original formulation of the riddle, it states that the boat cannot host all the elements together) and that everyone starts at the left hand side of the rst river and, eventually, ends up at the right hand side of the last one:

>8 f 0;S ^ e10;S ^ : : : ^ e0n;S ; 'riddle < [U ] Vj (Vi(ei1;B ^ : : : ^ eij;B1 ^ eij;+B1 ^ : : : ^ ein;B) ! ?); >: hLi(f m;S ^ e1m;S ^ : : : ^ enm;S ):

In Figure 7, we have reported the elapsed time for model checking the conjunction of the above formulas against a generalized version of the model in Figure 5. The size of the problem is expressed in bytes, and time in milliseconds. All experiments have been run on a CPU Intel(R) Core(TM) i7, with a clock of 2.60GHz and 8GB RAM. For each number of rivers, ranging from 1 to 5, we have tried to model check the conjunction of all speci cations for a number of elements ranging from 8 to 48 (with 4-unit steps).

As one may observe from Figure 7, the elapsed time grows quadratically, i.e., as a parabola, with the size of the input (size of the model plus size of the formula), as expected in a non-degenerate experiment. 5

Conclusions

Model checking is a fundamental problem in computational logic. In the recent past, it has been applied to a number of di erent contexts, ranging from program and protocol checking to system veri cation. Point-based temporal logics have been traditionally used for property speci cation in model checking. The interest for interval temporal logic model checking is much more recent.

We focused on the problem of model checking formulas of the interval temporal logic HS against (concrete) nite interval models, which comes into play in a number of applications di erent from automated system veri cation. As an example, constraint checking and query answering in temporal databases can be viewed as special instances of such a problem. The same holds for temporal rule extraction in data mining. A formalization of the problem, an analysis of its complexity, and a discussion of some possible applications can be found in [ 22 ].

Here, we proposed a rst implementation of the model checking procedure outlined in [ 22 ], and we reported the outcomes of its systematic testing against benchmarks obtained from the generalization of a known riddle and its solution.

References

1. L. Aceto , D. Della Monica , V. Goranko , A. Ingolfsdottir , A. Montanari , and G. Sciavicco . A complete classi cation of the expressiveness of interval logics of Allen's relations: The general and the dense cases . Acta Informatica , 53 ( 3 ): 207 { 246 , 2016 .

2. J. Allen . Maintaining knowledge about temporal intervals . Communications of the ACM , 26 ( 11 ): 832 { 843 , 1983 .

3. L. Bozzelli , A. Molinari , A. Montanari , and A. Peron. An in-Depth Investigation of Interval Temporal Logic Model Checking with Regular Expressions . In Proc. of the 15th SEFM , volume 10469 of LNCS , 2017 .

4. L. Bozzelli , A. Molinari , A. Montanari , and A. Peron . On the Complexity of Model Checking for Syntactically Maximal Fragments of the Interval Temporal Logic HS with Regular Expressions . In Proc. of the 8th GandALF , 2017 .

5. L. Bozzelli , A. Molinari , A. Montanari , A. Peron , and P. Sala . Interval temporal logic model checking: The border between good and bad HS fragments . In Proc. of the 8th IJCAR , volume 9706 of LNCS , pages 389 { 405 . Springer, 2016 .

6. L. Bozzelli , A. Molinari , A. Montanari , A. Peron , and P. Sala . Interval vs. point temporal logic model checking: an expressiveness comparison . In Proc. of the 36th FSTTCS , volume 65 of LIPIcs , pages 26 :1{ 26 : 14 , 2016 .

7. L. Bozzelli , A. Molinari , A. Montanari , A. Peron , and P. Sala . Model checking the logic of Allen's relations meets and started-by is PNP-complete . In Proc. of the 7th GandALF , volume 226 of EPTCS , pages 76 { 90 , 2016 .

8. D. Bresolin , D. Della Monica , A. Montanari , P. Sala , and G. Sciavicco . Interval temporal logics over strongly discrete linear orders: Expressiveness and complexity . Theoretical Computer Science , 560 : 269 { 291 , 2014 .

9. E.M. Clarke and E.A. Emerson . Design and synthesis of synchronization skeletons using branching-time temporal logic . In Logics of Programs , volume 131 of LNCS , pages 52 { 71 . Springer, 1981 .

10. C. Combi and A. Montanari . Data models with multiple temporal dimensions: Completing the picture . In Proc. of the 13th CAiSE , volume 2068 of LNCS , pages 187 { 202 . Springer, 2001 .

11. E.A. Emerson and J.Y. Halpern . Decision procedures and expressiveness in the temporal logic of branching time . Journal of Computer and System Sciences , 30 ( 1 ):1{ 24 , 1985 .

12. E.A. Emerson and J.Y. Halpern . \ Sometimes" and \Not Never" revisited: On branching versus linear time temporal logic . Journal of the ACM , 33 ( 1 ): 151 { 178 , 1986 .

13. J. Halpern and Y. Shoham . A propositional modal logic of time intervals . J. of the ACM , 38 ( 4 ): 935 { 962 , 1991 .

14. K. Kulkarni and J.E. Michels . Temporal features in SQL:2011 . ACM SIGMOD Record, 41 ( 3 ): 34 { 43 , 2012 .

15. A. Lomuscio and J. Michaliszyn . An epistemic Halpern-Shoham logic . In Proc. of the 23rd IJCAI , pages 1010 { 1016 , 2013 .

16. A. Lomuscio and J. Michaliszyn . Decidability of model checking multi-agent systems against a class of EHS speci cations . In Proc. of the 21st ECAI , volume 263 of Frontiers in Arti cial Intelligence and Applications , pages 543 { 548 , 2014 .

17. A. Lomuscio and J. Michaliszyn . Model checking multi-agent systems against epistemic HS speci cations with regular expressions . In Proc. of the 15th KR , pages 298 { 308 , 2016 .

18. A. Molinari , A. Montanari , A. Murano , G. Perelli, and A. Peron . Checking interval properties of computations . Acta Informatica , 53 ( 6-8 ): 587 { 619 , 2016 .

19. A. Molinari , A. Montanari , and A. Peron . Complexity of ITL model checking: Some well-behaved fragments of the interval logic HS . In Proc. of the 22nd TIME , pages 90 { 100 , 2015 .

20. A. Molinari , A. Montanari , and A. Peron . A model checking procedure for interval temporal logics based on track representatives . In Proc. of the 24th CSL , volume 41 of LIPIcs , pages 193 { 210 , 2015 .

21. A. Molinari , A. Montanari , A. Peron , and P. Sala . Model checking well-behaved fragments of HS: the (almost) nal picture . In Proc. of the 15th KR , pages 473 { 483 , 2016 .

22. 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. LIPIcs , 2017 .

23. A. Montanari , A. Murano , G. Perelli, and A. Peron . Checking interval properties of computations . In Proc. of the 21st TIME , pages 59 { 68 , 2014 .

24. A. Pnueli . The temporal logic of programs . In Proc. of the 18th FOCS , pages 46 { 57 , 1977 .

25. P. Roper . Intervals and tenses . Journal of Philosophical Logic , 9 ( 4 ): 451 { 469 , 1980 .

26. R.T. Snodgrass, editor. The TSQL2 Temporal Query Language . Kluwer, 1995 .

27. R.T. Snodgrass, I. Ahn, G. Ariav , D.S. Batory , J. Cli ord, C.E. Dyreson, R. Elmasri , F. Grandi , C.S. Jensen , W. Kafer, N. Kline , K. Kulkarni , T.Y.C. Leung , N. Lorentzos , J.F. Roddick , A. Segev , M.D. Soo , and S.M. Sripada . TSQL2 language speci cation . ACM Sigmod Record , 23 ( 1 ): 65 { 86 , 1994 .