Time Series Checking with Fuzzy Interval Temporal Logics? Willem Conradie1[0000−0001−9906−4132] , Dario Della Monica2[0000−0001−9743−665X] , Emilio Muñoz-Velasco3[0000−0002−0117−4219] , Guido Sciavicco4[0000−0002−9221−879X] , and Ionel Eduard Stan4,5[0000−0001−9260−102X] 1 School of Math., Wits University, South Africa willem.conradie@wits.ac.za 2 Dept. of Math., Comp. Sci., and Phys., University of Udine, Italy dario.dellamonica@uniud.it 3 Dept. of App. Math., University of Málaga, Spain ejmunoz@uma.es 4 Dept. of Math. and Comp. Sci., University of Ferrara, Italy {guido.sciavicco|ioneleduard.stan}@unife.it 5 Dept. of Math., Phys., and Comp. Sci., University of Parma, Italy Abstract. Model checking is a very well-known problem, with many practical applications. A possible variation of such a problem in the in- terval logic setting is the so-called finite 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 finite inter- val 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 flight. 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 define, solve, and discuss the complexity of the multi- variate time series fuzzy interval logic checking problem. Keywords: Model checking · Time series · Fuzzy logic. 1 Introduction 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 ? Copyright c 2020 for this paper by its authors. Use permitted under Creative Com- mons License Attribution 4.0 International (CC BY 4.0). The authors acknowl- edge the partial support by the Italian INDAM-GNCS project Strategic Reasoning and Automated Synthesis of Multi-Agent Systems, by the National Spanish project PGC2018-095869-B-I00 Fuzzy, Logic-based, and Algebraic tools for Information Re- sources, and by the Andalucia Region project UMA2018-FEDERJA-001 Mathemat- ics for the Imperfect Information. 2 W. Conradie et al. 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 fingers w.r.t. some reference point; different sport activities can be distinguished by the time series of some relevant physical quantities; all active sensors during a flight 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 satisfied by a given model [12]. Usually, the model is the ab- stract representation of a system, in which the relevant properties become propo- sitional 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 formu- lated in two ways. On the one side, model checking for full HS, interpreted over finite 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 (EXPSPACE- hardness 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 differ from those of [24,28] in two important respects, making it difficult 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 define the labeling of proposition letters over intervals in terms of the component states [22]. On the other side, the problem of checking finite, lin- ear, and fully represented interval models (FIMC problem) against HS formulæ was formulated in [14], and its infinite, periodical generalization was presented in [15] for a fragment of HS. Time Series Checking 3 These interval model checking strategies share the following elements: first, 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 define multivariate time series model checking as the problem of checking if an interval temporal logic formula is satisfied by a finite 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], effectively introducing the fuzzy interval logic multivariate time series checking problem (TFIMC). On the one hand, fuzzy model checking has received very little atten- tion 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); how- ever: (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 general- ization 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 im- pact 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 difficult), and such a difference 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 ∈ 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 different 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 ∈ {A, L, B, E, D, O}. 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 ∈ {A, L, B, E, D, O}, 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 4 W. Conradie et al. HS Allen’s relations Graphical representation x y x0 y0 hAi [x, y]RA [x0 , y 0 ] ⇔ y = x0 x0 y0 hLi [x, y]RL [x0 , y 0 ] ⇔ y < x0 x0 y0 hBi [x, y]RB [x0 , y 0 ] ⇔ x = x0 , y 0 < y x0 y0 hEi [x, y]RE [x0 , y 0 ] ⇔ y = y 0 , x < x0 x0 y0 hDi [x, y]RD [x0 , y 0 ] ⇔ x < x0 , y 0 < y x0 y0 hOi [x, y]RO [x0 , y 0 ] ⇔ x < x0 < y < y 0 Fig. 1. Allen’s interval relations and HS modalities. multi-modal logic with formulæ built from a finite, 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: ϕ ::= ⊥ | p | ¬ϕ | ϕ ∨ ϕ | hXiϕ. In the above grammar, p ∈ AP and X ∈ {A, L, B, E, D, O, A, L, B, E, D, O}. The other propositional connectives and constants (e.g., →, and >), as well as the dual modalities, can be defined in the standard way (e.g., [A]ϕ ≡ ¬hAi¬ϕ). Given a formula of HS, its inverse formula is obtained by substituting ev- ery operator hXi with its inverse one hXi, and the other way around, for X ∈ {A, L, B, E, D, O}, while its symmetric is obtained by substituting every op- erator hXi with its inverse one hXi, and the other way around, for X ∈ {A, L, O}, and every hBi (resp., hB̄i) with hEi (resp., hĒi), 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 ∈ AP the set of intervals V (p) on which p holds. In this work, we are interested in finite structures and thus we restrict our attention to linear orders over finite domains. A finite 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 defined by structural induction on formulæ as follows: M, [x, y] p if [x, y] ∈ V (p), for p ∈ AP ; M, [x, y] ¬ψ if M, [x, y] 6 ψ; M, [x, y] ψ ∨ ξ if M, [x, y] ψ or M, [x, y] ξ; M, [x, y] hXiψ if M, [z, t] ψ for [z, t] s.t. [x, y]RX [z, t], for X ∈ {A, L, B, E, D, O, A, L, B, E, D, O}. Time Series Checking 5 During the past decades, several computational problems related to the logic HS have been studied, including the satisfiability 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 inter- esting classes of linearly ordered sets, and for various fragments (with differ- ent computational behaviours) in, among others, [1,8,9,10,23,29,30], the model checking problem, in [21,24,14], and, more recently, different knowledge extrac- tion problems, in [7,11]. Fuzzy interval temporal logic. Fuzzy HS was introduced in [13], where its satisfiability problem, along with certain expressive power problems, were stud- ied. 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 defined 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 defined as: _ {γ | α ∧ γ  β}, and it exists for every α and β [17]. A Heyting algebra isWsaid to be complete if for every subset V S ⊆ H, both its least upper bound S and its greatest lower bound S exist. Typical realizations of Heyting algebras include the two- element 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 defined starting with a domain D enriched with two functions: <, e =e : D × D → H, and defining the structure: e = hD, <, D e =i e as a fuzzy linearly ordered set if it holds, for every x, y, and z: 1. =(x, e y) = 1 ⇔ x = y (reflexivity of =); e 2. =(x, e y) = =(y, e x) (symmetry of =); e 3. <(x, e x) = 0 (irreflexivity 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. 6 W. Conradie et al. 4. <(x, e z)  <(x, e y) ∧ <(y, e z) (transitivity of <); e 5. <(x, e y)  0 &<(y, e z)  0 ⇒ <(x,e z)  0 (transfer of <); e 6. <(x, y) = 0 &<(y, x) = 0 ⇒ =(y, e e e x) = 1 (weak totality); 7. =(x, e y)  0 ⇒ <(x, e y) ≺ 1 (non-contradiction of < e over =). e Observe that in the above formulæ we have used a meta-language with {&, ⇒ , ⇔} 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: ϕ ::= α | p | ϕ ∨ ϕ | ϕ ∧ ϕ | ϕ → ϕ | hXiϕ | [X]ϕ, where α ∈ H, p ∈ AP , and, as in the crisp case, X ∈ {A, L, B, E, D, O, A, L, B, E, D, O}. We use ¬ϕ to denote the formula ϕ → 0. Given a fuzzy linearly ordered set, we can now define the set of fuzzy (strict) intervals in D: e e = {[x, y] | <(x, I(D) e y)  0}. Generalizing classical Boolean evaluation, propositional letters are directly eval- uated in the underlying algebra, by defining a fuzzy valuation function Ve : AP × I(D)e → H that generalizes the crisp function V . Similarly, Allen’s rela- tions now have a fuzzy behaviour, which is obtained by generalizing the original, crisp definition, and substituting every = with = e and every < with <: e R eA ([x, y], [z, t]) = =(y, e z); R eL ([x, y], [z, t]) = <(y, e z); R eB ([x, y], [z, t]) = =(x, e z) ∧ <(t, e y); RE ([x, y], [z, t]) = <(x, e e z) ∧ =(y, e t); R eD ([x, y], [z, t]) = <(x, e z) ∧ <(t, e y); RO ([x, y], [z, t]) = <(x, z) ∧ <(z, e e e y) ∧ <(y, e t). Now, we say that an H-valued interval model (or fuzzy interval model) is a tuple of the type: f = hI(D), M e 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 M f and an interval [x, y] by extending the valuation Ve of propositional letters as follows, where X ∈ {A, L, B, E, D, O, A, L, B, E, D, O} and [z, t] varies in I(D): e Time Series Checking 7 Ve (α, [x, y]) = α; Ve (ψ ∧ ξ, [x, y]) = Ve (ψ, [x, y]) ∧ Ve (ξ, [x, y]); Ve (ψ ∨ ξ, [x, y]) = Ve (ψ, [x, y]) ∨ Ve (ξ, [x, y]); Ve (ψ → ξ, [x, y]) = V _(ψ, [x, y]) → V (ξ, [x, y]); e e V (hXiψ, [x, y]) = {RX ([x, y], [z, t]) ∧ Ve (ψ, [z, t])}; e e [z,t] ^ Ve ([X]ψ, [x, y]) = {R eX ([x, y], [z, t]) → Ve (ψ, [z, t])}. [z,t] We say that a formula ϕ of FHS is α-satisfied at an interval [x, y] in a fuzzy interval model M f = hI(D), e Ve i, denoted M f, [x, y] α ϕ, if Ve (ϕ, [x, y])  α. The formula ϕ is α-satisfiable if and only if there exists a fuzzy interval model and an interval in that model where it is α-satisfied. A formula is satisfiable if it is α-satisfiable for some α ∈ H, α 6= 0. A formula is α-valid if it is α-satisfied 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 definition of satisfiability is graded, rather than absolute, the usual duality between satisfiability 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 defined over a set of temporal variables (or temporal attributes) A = {A1 , . . . , Am } is usually represented as an n × m matrix:   a1,1 a1,2 . . . a1,m  a2,1 a2,2 . . . a2,m  T =  ... ... ... ... .  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-defined, 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 definition. Let T be a time series of length n defined over a set of variables A = {A1 , . . . , Am }. We define a set of decisions S as: S = {A ./ a | A ∈ A, a ∈ dom(A), ./ ∈ {≤, <, =, >, ≥}}, 8 W. Conradie et al. 120 42 115 41 • • 110 40 ? ? • ? 105 39 ? ? • 100 38 • ? 95 37 • • 90 36 • ? ? 1 2 3 4 5 6 7 8 Fig. 2. A multivariate time series with two variables. and we set S as our set of propositional letters. Now, consider a time series T with n distinct points, and the finite domain [n] + 1] obtained by adding a point 0 at the beginning of the series with undefined values a0,i , for each i. After having fixed two concrete relations = e and <,e we can form the set of intervals I([n^ + 1]), and define a function f to give truth values to decisions: f : S × I([n^ + 1]) → H. 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 defining a H-valued interval model: 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 undefined on 0, we may assume that f is undefined on every interval of the type [0, y] as well. Given a time series T , an algebra H, a value α ∈ 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 defines the domain of the algebra on which Te is defined. 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 define f , for a generic variable A, relation ./, Time Series Checking 9 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 fix a positive parameter h ∈ N (which can be thought of as an horizon), and define two parametric versions for =e and h, it is 0 when < y−x y < x, and it is h when 0 ≤ y − x ≤ h. It is immediate to see that they satisfy axioms 1-7. Moreover, if h = 1 our definition immediately reduces to the crisp definitions 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: hLi(A2 ≤ 100 ∧ A1 ≥ 38). Among all witnesses of such a condition in Te, we find the interval [5, 6]: <(1, e 5) = 4 2 2 4 , f (A 1 ≥ 38, [5, 6]) = 2 , and f (A 2 ≤ 100, [5, 6]) = 2 , so that Ve (hLi(A 2 ≤ 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 α ∈ 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 ◦ ∈ {∨, ∧, →} 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 RXe . 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 efficient 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 different 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 at- tributes, 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), 10 W. Conradie et al. Algorithm 1 Fuzzy interval logic multivariate time series checking algorithm. 1: function Check(Te, ϕ, α) 2: L=∅ 3: for ψ ∈ sub(ϕ) in increasing length order do 4: if ψ = β, with β ∈ H then 5: for [x, y] ∈ I([n^ + 1]) do 6: L(ψ, [x, y]) = β 7: if ψ = A ./ a then 8: for [x, y] ∈ I([n^ + 1]) do 9: L(ψ, [x, y]) = f (A ./ a, [x, y]) 10: if ψ = τ ◦ ξ then 11: ^ for [x, y] ∈ I([n + 1]) do 12: L(ψ, [x, y]) = L(τ, [x, y]) • L(ξ, [x, y]) 13: if ψ = hXiτ then 14: ^ for [x, y] ∈ I([n + 1]) do 15: s=0 16: ^ for [z, t] ∈ I([n + 1]) do 17: s ← s ∨ (RXe ([x, y], [z, t]) ∧ L(τ, [z, t])) 18: L(ψ, [x, y]) = s 19: if ψ = [X]τ then 20: ^ for [x, y] ∈ I([n + 1]) do 21: s=1 22: ^ for [z, t] ∈ I([n + 1]) do 23: s ← s ∧ (RXe ([x, y], [z, t]) → L(τ, [z, t])) 24: L(ψ, [x, y]) = s 25: 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 worst- case 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 deter- ministic algorithm. 4 Conclusions In this paper we first defined, and then solved, the multivariate time series fuzzy interval logic checking problem. Despite its simplicity, the interest in this prob- Time Series Checking 11 lems 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 clas- sical 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 efficient implementation of our algorithm, and to explore further interactions between model checking and learning, specifically, symbolic learning of FHS formulæ over time series. References 1. Aceto, L., Della Monica, D., Goranko, V., Ingólfsdóttir, A., Montanari, A., Sciav- icco, G.: A complete classification 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 classification 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 Verification (GandALF). EPTCS, vol. 226, pp. 76–90 (2016) 7. Bresolin, D., Cominato, E., Gnani, S., Muñoz-Velasco, E., Sciavicco, G.: Extracting interval temporal logic rules: A first 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 in- terval temporal logic: the Bernays-Schönfinkel fragment of CDT. Annals of Math- ematics and Artificial Intelligence 71(1-3), 11–39 (2014) 10. Bresolin, D., Kurucz, A., Muñoz-Velasco, E., Ryzhikov, V., Sciavicco, G., Za- kharyaschev, 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 learn- ing. In: Proc. of the 16th European Conference on Logics in Artificial Intelligence (JELIA). LNCS, vol. 11468, pp. 778–793 (2019) 12. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press (2002) 12 W. Conradie et al. 13. Conradie, W., Della Monica, D., Muñoz-Velasco, E., Sciavicco, G.: An approach to fuzzy modal logic of time intervals. In: Proc. of the 24th European Conference on Artificial 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 Artificial 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 An- nual 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 Artificial Intelligence (IJCAI). pp. 1010– 1016 (2013) 21. Lomuscio, A., Michaliszyn, J.: Decidability of model checking multi-agent systems against a class of EHS specifications. In: Proc. of the 21st European Conference on Artificial Intelligence (ECAI). pp. 543–548 (2014) 22. Lomuscio, A., Michaliszyn, J.: Model checking multi-agent systems against epis- temic HS specifications 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 Interna- tional 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) final 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 Repre- sentation and Reasoning (TIME). pp. 59–68. IEEE Computer Society (2014) 29. Montanari, A., Pratt-Hartmann, I., Sala, P.: Decidability of the logics of the re- flexive sub-interval and super-interval relations over finite linear orders. In: Proc. Time Series Checking 13 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 Artificial 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 Sympo- sium 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)