Time Series Checking with Fuzzy Interval Temporal Logics?

Abstract

Model checking is a very well-known problem, with many practical applications. A possible variation of such a problem in the interval logic setting is the so-called nite model checking, that consists of verifying an interval temporal logic formula, typically of Halpern and Shoham's logic of Allen's relations HS, on a fully represented nite interval model. Multivariate time series are collections of temporally ordered sets of values, and they allow to describe a variety of situations, such as the medical history of an hospitalized patient or the sensor values during a plane ight. In this paper we argue how the recently introduced fuzzy generalization of interval temporal logic is a suitable language in which interesting properties of a multivariate time series can be expressed and checked, and we de ne, solve, and discuss the complexity of the multivariate time series fuzzy interval logic checking problem.

Keywords

• Model checking Time series Fuzzy logic

-

A temporal variable is a variable whose value changes over time. A time series is a set of temporal variables. They can be univariate, if only one temporal variable is involved, or multivariate, otherwise. Each variable of a multivariate time series is an ordered collection of n numeric values, instead of a single value. Multivariate time (or temporal) series emerge in many application contexts: the temporal history of some hospitalized patients can be described by the time series of the values of their temperature, blood pressure, and oxygenation; the pronunciation of a word in sign language can be described by the time series of the relative and absolute positions of the ten ngers w.r.t. some reference point; di erent sport activities can be distinguished by the time series of some relevant physical quantities; all active sensors during a ight give time-changing values that form a time series. A repository of time series extracted from real-world data can be found in [ 3 ].

In its original formulation, model checking (MC) is the problem of verifying if a given formula is satis ed by a given model [ 12 ]. Usually, the model is the abstract representation of a system, in which the relevant properties become propositional letters, where the formula is written in a temporal logic and represents an interesting property. The prevailing adopted ontology for both the model and the logic is point-based: systems are represented in such a way that each state is a vertex on a Kripke model, atomic properties are descriptions of states, and the underlying logic is a point-based temporal logic, often LTL or CTL [ 32,33 ]. As interval-based temporal logics emerged as a possible alternative to point-based ones, the concept of interval temporal logic model checking (IMC) emerged with them. Halpern and Shoham's interval temporal logic HS [ 18 ], which features one modality for each Allen relation [ 2 ], is the most representative interval-based temporal logic, and its model checking problem is the one that received the most attention. The problem of model checking HS formul has been formulated in two ways. On the one side, model checking for full HS, interpreted over nite Kripke structures according to a state-based semantics has been studied in [ 24,28 ]. The authors showed that, under the homogeneity assumption, 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 (EXPSPACEhardness has been later shown in [ 5 ]). Since then, the attention was brought to HS fragments, which are often computationally much better [ 5,6,25,26,27 ]. Also, the model checking problem for some HS fragments extended with epistemic operators has been investigated in [ 20,21 ]. The semantic assumptions for these epistemic HS fragments di er from those of [ 24,28 ] in two important respects, making it di cult to compare the two families of logics: formul are interpreted over the unwinding of the Kripke structure (computation-tree-based semantics) and interval labeling takes into account only the endpoints of intervals. The latter assumption has been later relaxed by making it possible to use regular expressions to de ne the labeling of proposition letters over intervals in terms of the component states [ 22 ]. On the other side, the problem of checking nite, linear, and fully represented interval models (FIMC problem) against HS formul was formulated in [ 14 ], and its in nite, periodical generalization was presented in [ 15 ] for a fragment of HS.

These interval model checking strategies share the following elements: rst, the object to be checked is abstracted in some way, and, second, the underlying temporal logic is a crisp (i.e., non-fuzzy) logic. We de ne multivariate time series model checking as the problem of checking if an interval temporal logic formula is satis ed by a nite multivariate time series. Time series are represented without abstraction, and we capture the intrinsic uncertainty carried by real-world data by checking formul of the fuzzy generalization of HS (FHS) [ 13 ], e ectively introducing the fuzzy interval logic multivariate time series checking problem (TFIMC). On the one hand, fuzzy model checking has received very little attention in the literature, having been attempted in [ 16,31 ] for fuzzy generalizations of CTL; however, these frameworks are not directly comparable with the one we present here. On the other hand, our approach could be associated with the concept of probabilistic model checking (PMC) on Markov models, which has a large recent history in the literature (see [ 19 ], and references within); however: (i) fuzzy logics generalize probabilistic logics by having non-crisp both accessibility relations and atomic properties, (ii) probabilistic model checking is point-based, and (iii) Markov models are, as Kripke models, abstractions of the underlying systems. The TFIMC problem is the fuzzy, time series generalization of the FIMC problem. The major obstacle in solving the latter lies in the representation of the model, which may be exponentially succinct w.r.t. the size of the input (i.e., the pair model+formula). In [ 14 ] it has been proved that FIMC is polynomial, but the necessary pre-processing of the model has an impact on the overall complexity. Such an obstacle does not present itself in solving TFIMC, as time series cannot be succinctly represented, and, as a consequence, its complexity is lower than FIMC; however, the problem itself is conceptually not easier (in fact, it is slightly more di cult), and such a di erence is hidden, so to say, in the representation of the model. 2

Preliminaries: Fuzzy Interval Temporal Logic Crisp interval temporal logic. Let D = hD; i be a linearly ordered set. An interval over D is an ordered pair [x; y], where x; y 2 D and x < y. While in the original approach to interval temporal logic intervals with coincident endpoints were included in the semantics, in the recent literature they tend to be excluded except, for instance, in [ 4 ] where a two-sorted approach has been studied. If we exclude the identity relation, there are 12 di erent relations between two intervals in a linear order, often called Allen's relations [ 2 ]: the six relations RA (adjacent to, or meets), RL (later than), RB (begins), RE (ends), RD (during), and RO (overlaps), depicted in Figure 1, together with their inverses RX = (RX ) 1, for each X 2 fA; L; B; E; D; Og. We interpret interval structures as Kripke structures, with Allen's relations playing the role of the accessibility relations. Thus, we associate a universal modality [X] and an existential modality hXi with each Allen's relation RX . For each X 2 fA; L; B; E; D; Og, the inverse of the modalities [X] and hXi are the modalities [X] and hXi, corresponding to the inverse relation RX of RX . Halpern and Shoham's logic, denoted HS [ 18 ], is a

HS hAi hLi hBi hEi hDi hOi

Allen's relations [x; y]RA[x0; y0] , y = x0 [x; y]RL[x0; y0] , y < x0 [x; y]RB[x0; y0] , x = x0; y0 < y [x; y]RE[x0; y0] , y = y0; x < x0 [x; y]RD[x0; y0] , x < x0; y0 < y [x; y]RO[x0; y0] , x < x0 < y < y0

Graphical representation x y x0

y0 x0

y0 multi-modal logic with formul built from a nite, non-empty set AP of atomic propositions (also referred to as propositional letters), the classical propositional connectives, and a modal operator for each Allen's relation, as follows: ' ::= ? j p j :' j ' _ ' j hXi': In the above grammar, p 2 AP and X 2 fA; L; B; E; D; O; A; L; B; E; D; Og. The other propositional connectives and constants (e.g., !, and >), as well as the dual modalities, can be de ned in the standard way (e.g., [A]' :hAi:'). Given a formula of HS, its inverse formula is obtained by substituting every operator hXi with its inverse one hXi, and the other way around, for X 2 fA; L; B; E; D; Og, while its symmetric is obtained by substituting every operator hXi with its inverse one hXi, and the other way around, for X 2 fA; L; Og, and every hBi (resp., hBi) with hEi (resp., hEi), and the other way around.

The semantics of HS is given in terms of interval models of the type:

M = hI(D); V i; where D is a linear order, I(D) is the set of all intervals over D, and V is a valuation function V : AP 7! 2I(D), which assigns to each atomic proposition p 2 AP the set of intervals V (p) on which p holds. In this work, we are interested in nite structures and thus we restrict our attention to linear orders over nite domains. A nite domain of length n will be denoted [n]. The truth of a formula ' on a given interval [x; y] in an interval model M is de ned by structural induction on formul as follows:

M; [x; y] M; [x; y] M; [x; y] M; [x; y] p :

_ hXi if [x; y] 2 V (p); for p 2 AP ; if M; [x; y] 6 ; if M; [x; y] or M; [x; y] ; if M; [z; t] for [z; t] s.t. [x; y]RX [z; t]; for X 2 fA; L; B; E; D; O; A; L; B; E; D; Og:

During the past decades, several computational problems related to the logic HS have been studied, including the satis ability problem, analyzed for the full logic in the original work by Halpern and Shoham [ 18 ], in which the authors prove that it is undecidable when the logic is interpreted in virtually all interesting classes of linearly ordered sets, and for various fragments (with di erent computational behaviours) in, among others, [ 1,8,9,10,23,29,30 ], the model checking problem, in [ 21,24,14 ], and, more recently, di erent knowledge extraction problems, in [ 7,11 ].

Fuzzy interval temporal logic. Fuzzy HS was introduced in [ 13 ], where its satis ability problem, along with certain expressive power problems, were studied. A formula of a fuzzy modal logic is usually evaluated in a Heyting Algebra. A Heyting Algebra is a structure:

H = (H; ^; _; !; 0; 1); that is, a bounded distributive lattice with (non-empty) domain H, with internal operations ^ (meet6) and _ (join), both commutative, associative, and connected by the absorption law, in which a partial order can be de ned as: , ^ = , _ = : The symbols 0 and 1 denote, respectively, least and the greatest elements of H. In a Heyting algebra, the relative pseudo-complement of w.r.t. (aka Heyting implication), usually denoted as ! , is de ned as: _ f j ^ g; and it exists for every and [ 17 ]. A Heyting algebra is said to be complete if for every subset S H, both its least upper bound W S and its greatest lower bound V S exist. Typical realizations of Heyting algebras include the twoelement Boolean algebra and the closed interval [0; 1] in R. Given a complete Heyting algebra H with domain H, the fuzzy generalization of HS is de ned starting with a domain D enriched with two functions: <e ; =e : D

D ! H;

De = hD; <e ; =e i and de ning the structure: as a fuzzy linearly ordered set if it holds, for every x; y; and z: 1. =e (x; y) = 1 , x = y (re exivity of =);

e 2. =e (x; y) = =e (y; x) (symmetry of =);

e 3. <e (x; x) = 0 (irre exivity of <e ); 6 This is the classical nomenclature in lattice theory, and it should not be confused with Allen's relation meets, used in this paper. 4. <e (x; z) <e (x; y) ^ <e (y; z) (transitivity of <e ); 5. <e (x; y) 0 &<e (y; z) 0 ) <e (x; z) 0 (transfer of <e ); 6. <e (x; y) = 0 &<e (y; x) = 0 ) =e (y; x) = 1 (weak totality); 7. =e (x; y) 0 ) <e (x; y) 1 (non-contradiction of <e over =e ).

Observe that in the above formul we have used a meta-language with f&; ) ; ,g in order to avoid confusion. Given a set of propositional letters AP and a complete Heyting algebra H, a well-formed fuzzy interval temporal logic (FHS, for short) formula is obtained by the following grammar: ' ::=

j p j ' _ ' j ' ^ ' j ' ! ' j hXi' j [X]'; where 2 H, p 2 AP , and, as in the crisp case, X 2 fA; L; B; E; D; O; A; L; B; E; D; Og. We use :' to denote the formula ' ! 0.

Given a fuzzy linearly ordered set, we can now de ne the set of fuzzy (strict) intervals in De:

I(De) = f[x; y] j <e (x; y) 0g: Generalizing classical Boolean evaluation, propositional letters are directly evaluated in the underlying algebra, by de ning a fuzzy valuation function Ve : AP I(De) ! H that generalizes the crisp function V . Similarly, Allen's relations now have a fuzzy behaviour, which is obtained by generalizing the original, crisp de nition, and substituting every = with =e and every < with <e : ReA([x; y]; [z; t]) = =e (y; z); ReL([x; y]; [z; t]) = <e (y; z); ReB([x; y]; [z; t]) = =e (x; z) ^ <e (t; y); ReE ([x; y]; [z; t]) = <e (x; z) ^ =e (y; t); ReD([x; y]; [z; t]) = <e (x; z) ^ <e (t; y);

ReO([x; y]; [z; t]) = <e (x; z) ^ <e (z; y) ^ <e (y; t): Now, we say that an H-valued interval model (or fuzzy interval model) is a tuple of the type:

Mf = hI(De); Ve i; where De is a fuzzy linearly ordered set that respects properties 1-7, and Ve is a fuzzy valuation function. We interpret an FHS formula in a fuzzy interval model Mf and an interval [x; y] by extending the valuation Ve of propositional letters as follows, where X 2 fA; L; B; E; D; O; A; L; B; E; D; Og and [z; t] varies in I(De):

[z;t] We say that a formula ' of FHS is -satis ed at an interval [x; y] in a fuzzy interval model Mf = hI(De); Ve i, denoted Mf; [x; y] ', if Ve ('; [x; y]) . The formula ' is -satis able if and only if there exists a fuzzy interval model and an interval in that model where it is -satis ed. A formula is satis able if it is -satis able for some 2 H, 6= 0. A formula is -valid if it is -satis ed at every interval in every model, and valid if it is 1-valid. Observe that since a Heyting algebra, in general, does not encompass classical negation, and since our de nition of satis ability is graded, rather than absolute, the usual duality between satis ability and validity does not hold anymore. 3

Fuzzy Time Series Checking

Multivariate time series. A temporal variable is a variable whose value changes over time. A time series is a set of temporal variables. They can be univariate, if only one temporal variable is involved, or multivariate, otherwise. In data science, a time series de ned over a set of temporal variables (or temporal attributes) A = fA1; : : : ; Amg is usually represented as an n m matrix: 0a1;1 a1;2 : : : a1;m 1 T = BB@a:2:;:1 a:2:;:2 :: :: :: a:2:; m: CCA :

an;1 an;2 : : : an;m We denote the domain of an attribute A, that is, the set in which A takes values, by dom(A). We assume that each variable Ai that forms a multivariate series T has n values, and that there are no missing values, or that missing values are symbolized by placeholders; so, the length of a multivariate time series n is well-de ned, as well as its width m. By A(t), we denote the value of variable A at point t. An example of time series with m = 2 and n = 8 can be found in Figure 2; in this example, the variable A1 (circles) represents the evolution of a patient's temperature during the observed period, while the variable A2 (stars) represents his/her blood pressure during the same period.

Problem de nition. Let T be a time series of length n de ned over a set of variables A = fA1; : : : ; Amg. We de ne a set of decisions S as:

S = fA ./ a j A 2 A; a 2 dom(A); ./ 2 f ; <; =; >; gg; 120 42 115 41 110 40 ? 105 39 100 38 95 37 90 36 1 ? 2 ? 3 ? 4 ? 5 ? 6 ? 7 ? 8 and we set S as our set of propositional letters. Now, consider a time series T with n distinct points, and the nite domain [n]+ 1] obtained by adding a point 0 at the beginning of the series with unde ned values a0;i, for each i. After having xed two concrete relations = and <e , we can form the set of intervals I([n ^+1]), e and de ne a function f to give truth values to decisions: By means of f , we allow a decision to be H-valuated on an interval. Interpreting a formula of FHS on a time series T simply consists of de ning a H-valued interval model: f : S

I([n ^+1]) ! H:

Te = hI([n ^+1]); Ve ; f i; and of imposing that decisions are evaluated through f :

Ve (Ai ./ a; [x; y]) = f (Ai ./ a; [x; y]): Since the variables Ai are all unde ned on 0, we may assume that f is unde ned on every interval of the type [0; y] as well. Given a time series T , an algebra H, a value 2 H, and a formula ' of FHS, the fuzzy interval logic multivariate time series checking problem (TFIMC) is the problem of establishing if it holds: Te; [0; 1] ': In a way, we can say that the function f implicitly de nes the domain of the algebra on which Te is de ned.

Concretizing a model: an example. Given a time series T , there are many ways to produce a concrete temporal model; some of them are more intuitive than others. In this example, we assume H to be the closed interval [0; 1] in R equipped with the relation minimum (as meets) and maximum (as join), and we describe a concretization of f . The function f can be thought as a black-box function representing the domain-expert knowledge. In the example in Figure 2, for instance, one has to decide when temperature can be considered, say, over 38 degrees. One possible way is to de ne f , for a generic variable A, relation ./, value a, and interval [x; y], as the ratio between the number of points x t y that satisfy A ./ a and y x+1. Similarly, we have to describe a concretization of =e and <e . Among the many ways that exist to do so, we x a positive parameter h 2 N (which can be thought of as an horizon), and de ne two parametric versions for =e and <e as follows: =e h(x; y) is always 0, except when jx yj < h, in which case it is h jhx yj ; instead, <e h(x; y) is 1 when y x > h, it is 0 when y < x, and it is y hx when 0 y x h. It is immediate to see that they satisfy axioms 1-7. Moreover, if h = 1 our de nition immediately reduces to the crisp de nitions of = and <. Consider, again, the time series from Figure 2 and its corresponding model Te obtained with the above fuzzy equality and ordering relations, and in which we assume, for the purpose of this example, h = 4. A possibly interesting property to be evaluated on this time series is starting from day two, it is never true that blood pressure is low while temperature is high. We can translate such a property as starting from day two, there is no interval in which blood pressure is low (i.e., less than or equal to 100) and temperature is high (i.e., greater than or equal to 38). The existence of such an interval is translated to FHS as: 100 ^ A1 38): Among all witnesses of such a condition in Te, we nd the interval [5; 6]: <e (1; 5) = 44 , f (A1 38; [5; 6]) = 22 , and f (A2 100; [5; 6]) = 22 , so that Ve (hLi(A2 100 ^ A1 38); [0; 1]) = 1.

Algorithm. We are ready to formalize the fuzzy time series checking algorithm. Let Te = hI([^n+ 1]); Ve ; f i be a model based on some complete algebra H, ' a formula of FHS, and 2 H. Algorithm 1 is the adaptation of Emerson and Clarke's classical CTL algorithm to the interval, fuzzy case, and it returns true if and only if the value of ' on the (auxiliary) interval [0; 1] is greater than or equal to in Te. In Algorithm 1, we use the symbol 2 f_; ^; !g to denote a logical symbol, and the symbol to denote its algebraic corresponding one. Unlike the crisp case, every sub-formula must be checked on every interval, because, in the fuzzy case, any two intervals [x; y] and [z; t] may be related by any relation RX . e The auxiliary data structure L can be thought of as a hash table indexed by three elements, namely ; x; y, that is, a sub-formula, and two points. Accessing L may be considered to have constant time complexity. Formul , classically represented as binary trees, can be pre-processed in order to identify repeating sub-formul , so that the main cycle of Algorithm 1 can be implemented in an e cient way. It is worth observing that such a solution implicitly assumes that n is a reasonably low value; for very high values of n, a di erent solution should be designed for the dimension of L to be manageable.

Complexity. Let Te = hI([^n+ 1]); Ve ; f i be a model based on m temporal attributes, each with n distinct points, and let k be the length of the input formula '. Since the length of the time series grows as time passes, while its width remains unchanged as well as the property to check, we can assume that m; k = o(n), 1: function Check(Te; '; ) 2: L = ; 3: for 4: if Algorithm 1 Fuzzy interval logic multivariate time series checking algorithm. if if if if 2 sub(') in increasing length order do

= , with 2 H then for [x; y] 2 I([n^+ 1]) do

L( ; [x; y]) = = A ./ a then for [x; y] 2 I([n^+ 1]) do

L( ; [x; y]) = f (A ./ a; [x; y]) = then for [x; y] 2 I([n^+ 1]) do

L( ; [x; y]) = L( ; [x; y]) L( ; [x; y]) = hXi then for [x; y] 2 I([n^+ 1]) do s = 0 for [z; t] 2 I([n^+ 1]) do

s s _ (RXe ([x; y]; [z; t]) ^ L( ; [z; t]))

L( ; [x; y]) = s = [X] then for [x; y] 2 I([n^+ 1]) do s = 1 for [z; t] 2 I([n^+ 1]) do

s s ^ (RXe ([x; y]; [z; t]) ! L( ; [z; t]))

L( ; [x; y]) = s return L('; [0; 1]) that is, that there are much less temporal variables and much less sub-formul than there are distinct points. Thus, we can express the size of the input as O(n). Also, we can assume that the join (_), meet (^), and Heyting implication (!) operations take constant time in n, and that each call to f takes time O(n) (in the worst case scenario, in fact, each call to f requires exploring an interval with n points). The most external cycle is executed O(n) times. In the worstcase scenario, during each execution is a modal formula. Since there are O(n2) intervals in Te, the complexity of the modal case is O(n4). Therefore, the entire algorithm runs in O(n5).

Theorem 1. The TFIMC problem can be solved in polynomial time by a deterministic algorithm. 4

Conclusions

In this paper we rst de ned, and then solved, the multivariate time series fuzzy interval logic checking problem. Despite its simplicity, the interest in this problems lies in the fact that multivariate time series are ubiquitous in certain areas of data science and learning, but they have never before been linked to the classical model checking problem. Yet, we believe that many interesting properties can be formulated, and therefore checked, on a time series, and that the recently introduced fuzzy interval temporal logic FHS is a suitable language to do so. As future work, our intention is to design and test an e cient implementation of our algorithm, and to explore further interactions between model checking and learning, speci cally, symbolic learning of FHS formul over time series.

References

1. Aceto , L. , Della Monica , D. , Goranko , V. , Ingolfsdottir , A. , Montanari , A. , Sciavicco , G.: 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. Allen , J.F. : Maintaining knowledge about temporal intervals . Communications of the ACM 26 ( 11 ), 832 { 843 ( 1983 )

3. Bagnall , A.J. , Dau , H.A. , Lines , J. , Flynn , M. , Large , J. , Bostrom , A. , Southam , P. , Keogh , E.J. : The UEA multivariate time series classi cation archive , 2018 . CoRR abs/ 1811 .00075 ( 2018 ), http://arxiv.org/abs/ 1811 .00075

4. Balbiani , P. , Goranko , V. , Sciavicco , G.: Two sorted point-interval temporal logic . In: Proc. of the 7th Workshop on Methods for Modalities (M4M) . ENTCS , vol. 278 , pp. 31 { 45 ( 2011 )

5. Bozzelli , L. , Molinari , A. , Montanari , A. , Peron , A. , Sala , P. : Interval temporal logic model checking: The border between good and bad HS fragments . In: Proc. of the 8th International Joint Conference on Automated Reasoning (IJCAR) . LNCS , vol. 9706 , pp. 389 { 405 . Springer ( 2016 )

6. Bozzelli , L. , Molinari , A. , Montanari , A. , Peron , A. , Sala , P. : Model checking the logic of allen's relations meets and started-by is PNP-complete . In: Proc. of the 7th International Symposium on Games , Automata, Logics and Formal Veri cation (GandALF) . EPTCS , vol. 226 , pp. 76 { 90 ( 2016 )

7. Bresolin , D. , Cominato , E. , Gnani , S. , Mun~oz- Velasco , E. , Sciavicco , G.: Extracting interval temporal logic rules: A rst approach . In: Proc. of the 25th International Symposium on Temporal Representation and Reasoning (TIME). LIPIcs , vol. 120 , pp. 7 : 1 {7: 15 ( 2018 )

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

9. Bresolin , D. , Della Monica , D. , Montanari , A. , Sciavicco , G. : The light side of interval temporal logic: the Bernays-Schon nkel fragment of CDT . Annals of Mathematics and Arti cial Intelligence 71 ( 1-3 ), 11 { 39 ( 2014 )

10. Bresolin , D. , Kurucz , A. , Mun~oz- Velasco , E. , Ryzhikov , V. , Sciavicco , G. , Zakharyaschev , M. : Horn fragments of the Halpern-Shoham interval temporal logic . ACM Transactions on Computational Logic 18 ( 3 ), 22 :1{ 22 : 39 ( 2017 )

11. Brunello , A. , Sciavicco , G. , Stan , I. : Interval temporal logic decision tree learning . In: Proc. of the 16th European Conference on Logics in Arti cial Intelligence (JELIA) . LNCS , vol. 11468 , pp. 778 { 793 ( 2019 )

12. Clarke , E.M. , Grumberg , O. , Peled , D. : Model Checking. MIT Press ( 2002 )

13. Conradie , W. , Della Monica , D. , Mun~oz- Velasco , E. , Sciavicco , G. : An approach to fuzzy modal logic of time intervals . In: Proc. of the 24th European Conference on Arti cial Intelligence (ECAI) ( 2020 ), in press

14. Della Monica , D., de Frutos-Escrig, D. , Montanari , A. , Murano , A. , Sciavicco , G. : Evaluation of temporal datasets via interval temporal logic model checking . In: Proc. of the 24th International Symposium on Temporal Representation and Reasoning (TIME). LIPIcs , vol. 90 , pp. 11 : 1 { 11 : 18 ( 2017 )

15. Della Monica , D. , Montanari , A. , Murano , A. , Sciavicco , G.: Ultimately-periodic interval model checking for temporal dataset evaluation . In: Proc. of the 5th Global Conference on Arti cial Intelligence (GCAI) . EPiC Series in Computing , vol. 65 , pp. 28 { 41 ( 2019 )

16. Ebrahimi , M. , Sotudeh , G. , Movaghar , A. : Symbolic checking of fuzzy CTL on fuzzy program graph . Acta Inf . 56 ( 1 ), 1 { 33 ( 2019 )

17. Galatos , N. , Jipsen , P. , Kowalski , T. , Ono , H.: Residuated lattices: an algebraic glimpse at substructural logics . Elsevier ( 2007 )

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

19. Katoen , J.: The probabilistic model checking landscape . In: Proc. of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) . pp. 31 { 45 . ACM ( 2016 )

20. Lomuscio , A. , Michaliszyn , J.: An epistemic halpern-shoham logic . In: Proc. of the 23rd International Joint Conference on Arti cial Intelligence (IJCAI) . pp. 1010 { 1016 ( 2013 )

21. Lomuscio , A. , Michaliszyn , J.: Decidability of model checking multi-agent systems against a class of EHS speci cations . In: Proc. of the 21st European Conference on Arti cial Intelligence (ECAI) . pp. 543 { 548 ( 2014 )

22. Lomuscio , A. , Michaliszyn , J.: Model checking multi-agent systems against epistemic HS speci cations with regular expressions . In: Proc. of the 15th International Conference on Principles of Knowledge Representation and Reasoning (KR) . pp. 298 { 308 ( 2016 )

23. Marcinkowski , J. , Michaliszyn , J.: The undecidability of the logic of subintervals . Fundamenta Informaticae 131 ( 2 ), 217 { 240 ( 2014 )

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

25. Molinari , A. , Montanari , A. , Peron , A. : Complexity of ITL model checking: Some well-behaved fragments of the interval logic HS . In: Proc. of the 22nd International Symposium on Temporal Representation and Reasoning (TIME) . pp. 90 { 100 ( 2015 )

26. Molinari , A. , Montanari , A. , Peron , A. : A model checking procedure for interval temporal logics based on track representatives . In: Proc. of the 24th EACSL Annual Conference on Computer Science Logic (CSL) . LIPIcs , vol. 41 , pp. 193 { 210 ( 2015 )

27. Molinari , A. , Montanari , A. , Peron , A. , Sala , P. : Model checking well-behaved fragments of HS: the (almost) nal picture . In: Proc. of the 15th International Conference on Principles of Knowledge Representation and Reasoning (KR) . pp. 473 { 483 ( 2016 )

28. Montanari , A. , Murano , A. , Perelli , G. , Peron , A. : Checking interval properties of computations . In: Proc. of the 21st International Symposium on Temporal Representation and Reasoning (TIME) . pp. 59 { 68 . IEEE Computer Society ( 2014 )

29. Montanari , A. , Pratt-Hartmann , I. , Sala , P. : Decidability of the logics of the reexive sub-interval and super-interval relations over nite linear orders . In: Proc. of the 17th International Symposium on Temporal Representation and Reasoning (TIME) . pp. 27 { 34 ( 2010 )

30. Montanari , A. , Sciavicco , G. , Vitacolonna , N.: Decidability of interval temporal logics over split-frames via granularity . In: Proc. of the 8th European Conference on Logics in Arti cial Intelligence (JELIA) . LNAI , vol. 2424 , pp. 259 { 270 . Springer ( 2002 )

31. Pan , H. , Li , Y. , Cao , Y. , Ma , Z. : Model checking fuzzy computation tree logic . Fuzzy Sets Syst . 262 , 60 { 77 ( 2015 )

32. Pnueli , A. : The temporal logic of programs . In: Proc. of the 18th Annual Symposium on Foundations of Computer Science (FOCS) . pp. 46 { 57 ( 1977 )

33. Pnueli , A. : The temporal semantics of concurrent programs . Theoretical Computer Science 13 ( 1 ), 45 { 60 ( 1981 )