Implementation of a tableau-based satis ability checker for HS3 ?

Abstract

Although there exist several decidable fragments of Halpern and Shoham's interval temporal logic HS, the computational complexity of their satis ability problem tend to be generally high. Recently, the fragment HS3 of HS, based on coarser-than-Allen's relations, has been introduced, and it has been proven to be not only decidable, but also relatively e cient. In this paper we describe an implementation of a tableau-based satis ability checker for HS3 interpreted in the class of all nite linear orders.

Introduction

Interval Temporal Logics (ITLs) consider time intervals as the primitive ontological entities. This represents an advantage when dealing with some relevant application domains, such as planning and synthesis of controllers, which are characterized by advanced features that are neglected or dealt with in an unsatisfactory way by point-based formalisms. ITLs have been applied in several elds, such as hardware and real-time system veri cation, language processing, constraint satisfaction and planning, among others [ 2, 15, 25, 27 ]. Moreover, due to the fact that temporal logics are considered as the natural basis for temporal extensions of Description Logics [ 5 ], several attempts have been made to design interval-based extensions of such formalisms, as in [ 3, 4, 7, 28 ]. ITLs can be also considered as the temporal counterpart of TSQL, that is, the temporal extension to the language SQL for databases, included in the standard SQL:2011 [ 32 ]. Halpern and Shoham's Modal Logic of Allen's Relations (HS), introduced in [ 20 ], is the most prominent representative interval temporal logic, but its satis ability problem is undecidable when interpreted in almost every interesting class of linearly ordered sets. Various strategies have been considered in the literature to de ne fragments or variants of HS with a better computational behaviour, including constraining the underlying temporal structure [ 24 ], restricting the set of modal operators [ 1,13 ], softening the semantics to a re exive one [ 23 ], restricting the nesting of modal operators [ 10 ], and restricting the propositional power of the languages [ 12,14 ]. The underlying idea in [ 26 ] is substituting Allen's Interval Algebra (IA) [ 2 ] as the backbone of HS (modal operators in the HS repository can be mapped one-by-one over Allen's interval relations) with a set of jointly exhaustive, mutually exclusive, but coarser, interval relations, originally proposed in Golumbic and Shamir's work [ 17 ]. In particular, the coarser algebra IA3 involves three relations: the original before and after, plus a relation (intersects) that can be viewed as the disjunction of all the remaining ones (and therefore is the inverse of itself and includes equality). We call the corresponding modal logic HS3: in [ 26 ] its nite satis ability problem has been shown to be PSpace-complete by providing a suitable small model theorem.

In this paper we describe the implementation of a satis ability checker for HS3 interpreted in nite linear orders. The nite satis ability problem is usually emblematic for the entire range of (discrete) satis ability problems in interval temporal logics, and so is our tableau-based procedure. On the other hand, checking the ( nite) satis ability of an interval temporal logic formula is essentially di erent from the same problem for a point-based temporal formula due to the absence of the Until operator and the fact that ITLs are not generally susceptible of being treated via xed-point techniques. This means that most of the work done for (variants of) LTL, including [ 18, 29, 31 ] cannot be simply reused, nor compared with this one. Tableau-based procedures for interval temporal logics are not common in the literature. Among the few exceptions, a procedure for the fragment A of HS has been implemented in [ 9, 22 ]; the former is an experimental implementation not devoted to computational e ciency, and the latter is an attempt to use an automatic tableaux generator introduced in [ 30 ]. The only previous attempt to apply a generic theorem prover to an interval temporal logic can be found in [ 11 ], where a tableau-based decision procedure for the fragment D, interpreted over dense linear orders, was developed in LoTREC [ 16 ]. Finally, in [ 8 ] the authors designed an implementation for a tableau-based procedure for a ITL with the chop operator, which is interval-based but employs a semantic strategy, called locality, that reduces the truth of a propositional letter over an interval to that of the initial point of that interval. 2

The logic HS and its fragment HS3

Let D = hD; <i be a strict (i.e., irre exive) linearly ordered set. A strict interval (resp., non-strict interval) over D is an ordered pair [x; y], where x; y 2 D and x < y (resp., x y). In the recent literature, the strict semantics, where only strict intervals are considered, is usually adopted. This conforms to the de nition of interval adopted by Allen in [ 2 ], but di ers from the one given by Halpern and Shoham in [ 20 ]. 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), RL (later than), RB (begins), RE (ends), RD (during), and RO (overlaps), depicted in Fig. 1, and their inverses, that is, hAi hLi hBi hEi hDi hOi HS3/HS7 hAOi hDBEi hIi

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

Semantics hAOi hDBEi hIi hAi _ hOi

hDi _ hBi _ hEi hAOi _ hAOi _ hDBEi _ hDBEi

Graphical representation x y x0

y0 x0

y0 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 relation RX . For each X 2 fA; L; B; E; D; Og, the transposes 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 HS [ 20 ] is a multi-modal logic with formulas built from a nite, non-empty set AP of atomic propositions (also referred to as proposition letters), the classical propositional connectives, and a pair of modalities for each Allen relation: ' ::= ? j p j : j _ j ^ j hXi j hXi ; (1) where p 2 AP and X 2 fA; L; B; E; D; Og. The other propositional connectives and constants (e.g., !, and >), as well as the dual modalities (e.g., [A]' :hAi:'), can be derived in the standard way. In general, given any subset S fY; Y j Y 2 fA; L; B; E; D; Ogg, one can de ne the relation: RS = _ RX :

X2S The corresponding modal operator can be denoted by simply juxtaposing the original symbols to obtain a string, so that, for example, the modal operator that is the disjunction of Allen's relations overlaps and during would be denoted by hODi. In some cases, such as the relation intersect, we introduce a shorthand for the sake of readability, so that I = AABBEEOODD3. Well-formed HS3 formulae can be obtained from (1) when X 2 fL; Ig; for the sake of completeness, a ner version of HS3 can be de ned, called HS7, under the restriction that X 2 fL; AO; DBEg, but in [ 26 ] it has been proved that its computational behaviour is the same as the entire HS.

The semantics of HS and HS3 is given in terms of interval models M = hI(D); V i, where D is a linear order, I(D) is the set of all (strict) 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. The truth of a formula ' on a given interval [x; y] in an interval model M is de ned by structural induction on formulae, as follows: { M; [x; y] { M; [x; y] { M; [x; y] { M; [x; y] { M; [x; y] { M; [x; y] p 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; [x; y] and M; [x; y] ; hXi if there exists [z; t] such that [x; y]RX [z; t] and M; [z; t] hXi if there exists [z; t] such that [x; y]RX [z; t] and M; [z; t] ; .

Formulas of HS, and therefore of HS3, can be interpreted over several different classes of interval models. Their frame properties sometimes in uence the computational complexity of the satis ability problem, as witnessed by the recent series of results [ 1, 13 ]. Notable classes of linear orders include the class of all linear orders, the class of all nite linear orders, containing all and only those 3 This notation should not be confused with the standard notation for fragments of HS, indicated by the set of its modal operators, e.g., ABBA, which includes four modal operators, namely, hAi; hAi; hBi, and hBi. linear orders with nitely many points, and the classes of interval models that can be built over notable sets such as N; Z; Q, and R. Beside notable exceptions (such as the fragment ABBA), fragments of HS tend to behave in a similar way in all nite/discrete cases. Not only is solving in an e cient way the nite satisability problem a necessary step towards tackling the satis ability problem for other, sometimes more interesting, classes of linearly ordered sets, but it is also an important problem on its own. For example, temporal databases use intervals to describe time, and the interval logic HS is their ideal logical counterpart, especially when interpreted in nite domains. Temporal queries, as well as temporal constraints, can be easily expressed in HS, and the problem of establishing whether a query or a constraint is semantically correct is, essentially, a nite satis ability problem. The latter is undecidable in HS; although HS3 is less expressive than HS, some interesting queries and constraints can be expressed in the former [ 26 ], and, thus, checked. 3

A tableau-based satis ability checker for HS3

In [ 26 ], a small model theorem for HS3 interpreted in the class of all nite linear orders has been proved, that is, that a formula ' is nitely satis able if and only if it has a model with less than

2j'j (log(4 j'j+1)+log(j'j)+j'j) distinct points; let us call this number L('). Building on it, it has been possible to prove that the nite satis ability problem for HS3 is PSpace-complete. This result, in particular, is obtained by showing the correctness and completeness of a PSpace (non-deterministic) algorithm based on the maximal dimension of a satisfying model for a given formula '. Such an algorithm is ine cient in nature (although theoretically optimal); in this section, we describe an e cient (but not theoretically optimal) imperative, deterministic implementation of a tableau-based procedure for checking the nite satis ability of formulas of HS3; the ow diagram of the entire procedure is depicted in Fig. 2. We have chosen to develop a semantic tableau-based satis ability checker for HS3. Algebraically speaking, both the tableau and the formula to be checked are represented as rooted decorated trees. A rooted directed tree is a graph G = (V; E; r), where V is nonempty, E V V , jEj = jV j 1, and r 2 V is its root; every element of V is called a node. A rooted decorated tree [ 19 ] is a rooted directed tree such that there exists a function that associates every node with its decoration, which can be thought of as the information carried by that node; when we represent formulae, a decoration is a propositional letter or an operator, and when we represent semantic tableaux, a decoration is the collection of all information needed to expand the tableau or to close it. In any (rooted decorated) tree, nodes without successors are called leaves, and every nite path from the root to a leaf is called a branch.

Representation. Formulas and tableaux are represented as rooted decorated trees. Focusing on formulas, which correspond to binary trees, each node of Climb up the branch Select leaf

No Model?

Yes

Satis able Throw away the leaf

Yes

Contradictory? Yes

Other leaves?

No Unsatis able No

Expand the tree contains a code that identi es the operator (Boolean or modal, distinguishing between universal and existential), of which a propositional letter is a special case; nodes with a single child have a left child only. A formula is read and contextually transformed by a tree; a simple recursive procedure eliminates all implications and pushes all negations in front of propositional letters, obtaining an equivalent formula in negated normal form. Moreover, since nite satis ability can be reduced to nite initial satis ability, that is, satis ability over the initial interval [0; 1], before checking its satis ability our procedure transforms a formula ' into the formula

' _ hLi' _ hIi'; whose initial satis ability is checked. Indeed, if ' is satis ed on a model M at some interval [x; y] 6= [0; 1], then either y > 1 and therefore hLi' is satis ed at [0; 1], or y 1, and therefore hIi' is satis ed at [0; 1].

A tableau is represented as a k-ary tree in form of left-child right-sibling. Each node of this tree contains a pointer to the node in the formula tree that represents the sub-formula under analysis, the interval over which it holds, an active/inactive ag, a leaf/internal ag, and the pointers to the left child, the right sibling, and the parent. Domains are represented as totally ordered sets of oating point numbers, so that an interval is a pair of oating point numbers. This has a very speci c purpose: whenever a new point must be added in between a pair of already existing ones, it can be created by simply computing their arithmetic average; nevertheless, a model is always nite by construction. Some tableau nodes are leaves during the construction of the tableau; they (temporally) represent their branch, so that they also store domain information, plus other data that help us choosing the next branch depending on the expansion policy. In addition to the two trees (a formula tree and a tableau tree - the former is xed during the satis ability checking process of a given formula, the latter evolves), there are additional data structures used within the tableau expansion. In particular, the collection of all current leaves is stored in a linked list. Each element of such a list points to the tableau node that represents that leaf (and therefore a branch) which may be chosen in the next expansion step. A non-trivial adaptation of a generic tree visit algorithm has been implemented in order to correctly identify, given a tableau node, the set of all and only leaves that belong to the sub-tree rooted at it (see Fig. 3). Finally, a dynamic data structure is built (and destroyed) before each expansion step that allows us to examine the branch on which the to-be-expanded tableau node lies in order to establish if the branch is closed (because it is contradictory), or it represents a model (in which case the procedure stops and returns that the given formula is satis able). Such a structure may be thought of as a hash (unordered) set with an e cient (constant time) lookup method, that contains the intervals and the formulas that are (currently) true on them.

Initial tableau and main procedure. The initial tableau for a formula ' whose initial satis ability must be checked is a tableau tree composed by a single

Branch checking. Given a branch B, we check, at the same time, whether it is closed or it is a model, and, during this operation, a structure (H; S; n) is produced; both H (i.e., the current labeled interval structure) and S (i.e., the set of all formulas that should appear somewhere due to some universal modality) are unordered heaps of pairs (node, interval), while n is a node on the branch B. By means of this structure we are able to check if: (i) it presents a contradiction, or (ii) it is a model. The branch B is closed if one of the following two conditions holds: a propositional contradiction is found on it, that is, there exist two nodes in B such that their decorations show (p; [x; y]) and (:p; [x; y]), respectively, or the domain in the decoration of its leaf is greater than L('). Notice that when B is contradictory, it may be the case that it presents more than one contradiction. Let (m1; m01); (m2; m02); : : : be the set of all pairs of contradictory nodes in B in increasing order of distance (i.e., number of edges) from the root; the structure (H; S; n) is built in such a way that n points precisely to m01. In this way, we can eliminate from the list of leaves all those that identify a branch B0 that share the contradiction (m1; m01) with B (there may be more than one such branch). If all leaves are eliminated, the formula is found unsatis able. If B is not contradictory, we check whether all active universal modalities on B have already been expanded in all possible intervals: if that is the case, and if, in B, the only active nodes are universal modalities, then we can conclude that B is a model. If B is not a model but it is not contradictory, then n points to the node that is closest to the root and active.

Branch expansion. Expansion rules are described in Tab. 1. Boolean rules are standard, while the rules for modal operators are designed as follows. Let D be the set of all nite domains, and let I be the set of all intervals in any domain in D. For a given existential operator hXi, we de ne a function: e;X : I

D ! N that for a given pair ([x; y]; D) returns the number of di erent intervals in the relation RX with [x; y] plus the number of new intervals that should be created in the relation RX in order to explore all qualitatively distinct possibilities (see [ 19 ] for a similar approach for a simpler interval temporal logic); for example, e;L([0; 1]; f0 < 1 < 2g) is 5: indeed, if hLi holds on [0; 1] and the current domain is f0 < 1 < 2g, then may hold on some interval [1:25; 1:75]; [1:5; 2]; [2; 2:5]; [3; 4]; or [1:5; 2:5]; notice that, for example, [1:25; 1:75] is a necessary possibility as it represents a new interval completely between existing points; the same holds for [3; 4]. In this way, given hXi holding on [x; y] in the nite domain D, the parametric function(s): ie;;IX : I

D ! I ; ie;;DX : I

D ! D return, respectively, the i-th interval on which holds and the corresponding ith domain (not necessarily di erent from D) in no particular order; following up with the above example, e1;;LI([0; 1]; f0 < 1 < 2g) = [1:25; 1:75], e1;;LD([0; 1]; f0 < 1 < 2g) = f0 < 1 < 1:25 < 1:75 < 2g. Because we are restricting ourselves to initial satis ability, these functions never return new points between 0 and 1, nor smaller than 0. In this way for each existential operator hXi we have an existential disjunctive rule that creates enough branches to search for every possible location for . Dually, for universal operators, we have functions u;X and iu;X to return all intervals seen from [x; y] via RX ; in this case, domains do not change.

Given the node in B to be expanded, the correct rule is chosen for its expansion, and the result of such a step is applied to all leaves in the sub-tree rooted at the chosen node. Potentially, each application of the expansion rules gives rise to new nodes to be attached to such leaves; they are placed all the same level as new leaves in disjunctive rules (i.e., _; hXi), or in sequence (with no particular order) in conjunctive rules (i.e., ^; [X]). While the application of Boolean rules is completely standard, non-Boolean ones are subject to the following conditions:(i) if the hXi rule is applied to the node n with the decoration (hXi ; [x; y]), and B already contains a pair ( ; [z; t]) where [x; y]RX [z; t], then n is deactivated without any expansion; (ii) similarly, if the [X] rule is applied to the node n with the decoration ([X] ; [x; y]), then, for each pair ( ; [z; t]) where [x; y]RX [z; t] is already present in B, this pair is not added to the set of nodes that is the result of the expansion. The protocol for active/inactive nodes is designed in such a way that nodes are deactivated after being expanded; in case of universal nodes, they are copied at the end of the branch with the active ag at 1.

Soundness, completeness. We want to argue that our tableau-based procedure is sound and complete; calculating its complexity in the worst-case scenario is not really informative (it is, in fact, doubly exponential in time) considering that the interest in tableau-based methods roots in their e ciency in the average case, as well as their several possible optimizations.

In order to argue that the presented method is complete we need to introduce the following notion. Consider a node n on a tableau for a formula ', and let S(n) be the set of all decorations on nodes between n and the root; we say that S(n) is satis ed on an extension of D(n), where D(n) is the domain in the decoration of n, if there exists a model M based on some extension of D(n) such that, for each ( ; [x; y]) 2 S(n) it is the case that M; [x; y] . We now show that for every nitely satis able formula of HS3 the presented method terminates and returns `Satis able', that is, contra-positively, whenever the procedure closes all branches, the starting formula ' is not nitely satis able, by proving, by induction, a stronger claim: for any node n at height h on a tableau for ', if every branch that contains n is closed, then S(n) is not satis ed on any extension D0 of D(n) such that jD0j L('); notice that, when n is the root, this is to say that ' is not nitely satis able. Now, if h = 0, the only branch that contains n also contains two nodes with decorations (p; [x; y]) and (:p; [x; y]), and therefore S(n) is simply not satis able, or the number of points ever named in the decorations of its nodes is more than L('), for which S(n) can never be satis ed on any extension of D(n). If h > 0, then n has been expanded by some rule, some nodes n1; n2; : : : exist that are descendants of n, and the inductive hypothesis applies to all of them. If the rule that has been applied is Boolean, than the claim follows immediately. If it is the universal rule, then suppose that ([X] ; [x; y]) is in the decoration of n. Every branch that contains n also contains all nodes that are the result of its expansion, and, in particular, some node n0 with decoration ( ; [z; t]) for some interval [z; t] such that [x; y]RX [z; t]; if S(n) were satis able on some extension of D(n), then, in particular, S(n) [ f( ; [z; t])g = S(n0) would be too, but this is in contradiction with the inductive hypothesis. Finally, if it is the existential rule, then suppose that (hXi ; [x; y]) is in the decoration of n. If S(n) were satis able on some extension of D(n), then there would be a model whose domain extends D(n) such that it satis es hXi on [x; y] and on some [z; t] such that [x; y]RX [z; t]. By construction, there must be some successor n0 of n that contains the decoration ( ; [z; t]), independently of z; t being already in D(n). This means that S(n0) would be satis able on some extension of D(n0), which is in contradiction with the inductive hypothesis.

To conclude, we must argue that our method is also sound, that is, for every formula ' of HS3 for which it returns `Satis able', there exists a model M such that M; [0; 1] '. Consider a branch B such that it is not contradictory, all its active nodes are universal, and every node with universal decoration has been already expanded on every possible interval of the domain D of the branch. Now, let M be a model based on D, and whose valuation function is de ned as follows: for each interval [x; y] and each propositional letter p, [x; y] 2 V (p) if and only if (p; [x; y]) decorates some node on B. We want to prove, by structural induction, that, for each node n in B with decoration ( ; [x; y]), M; [x; y] . If is a propositional letter or its negation, we have the result immediately. If is a composite formula, two cases arise: either it is a universal formula, or it is not. In the latter case, the fact that B is not closed implies that n has been expanded, and such expansion has been applied to all branches that contain n: if is a conjunction, then both conjuncts have been included as decorations in nodes of B, if it is a disjunction then at least one disjunct has been included as decoration in some node of B, and, if it is = hXi , then at least one node in B must be decorated with ( ; [z; t]), for some [z; t] such that [x; y]RX [z; t]; in all cases, the inductive hypothesis applies, so that M must satisfy on [x; y]. In the former case, if = [X] , since B cannot be further extended, it must be the case that a node n0 with decoration ( ; [z; t]) occurs in B for each [z; t] such that z; t 2 D and that [x; y]RX [z; t], and again, the inductive hypothesis applies. Theorem 1. A formula ' of HS3 is nitely satis able if and only if the tableaubased method described in Fig. 2, with the rules in Tab. 1, returns `Satis able'. Policies. Our procedure is programmed fully object-oriented in C++ standard language with threads capabilities. Threads are run in (virtual) parallel, and carry a speci c policy for choosing the next leaf to be examined. Each policy is fair, that is every branch is eventually examined; the advantage of using di erent policies is the improved execution time, especially for satis able formulae. We have taken into account two key aspects: domain cardinality and branch sparseness. The sparseness degree allows us to estimate how many intervals already existing in the domain are actually used; to compute such an estimation, we calculate the average of positive propositional letters assigned to some interval, and de ned the sparseness of the branch as the variance of the (ideal) binomial probabilistic variable associated to assigning positive propositions to intervals. We implemented the following policies: (i) branches with smaller domain and less sparse rst (SBF); (ii) branches with longer domain and more sparse rst (LBF); (iii) branches taken in First-In-First-Out order (FIFO) - that is, the tableau tree is explored depth- rst. In our experiments (see next section) we used all such policies; establishing which one of them, if any, is clearly better than the others is an open problem. 4

Experimental results

Because tableau-based (and, in general, decision and semi-decision) procedures for interval temporal logics are not common in the literature, there are no available benchmarks. We have designed a scalable experiment to generate a sequence of (arbitrary) nitely satis able formulae, shown in Tab. 2, which are systematically generated for k = 1; 3; 5; : : :, so that their length can be put in relation with the time that our method takes to establish its satis ability; formulae are generated inductively, and to generate 'k, we use 'k 2[+2], that is, 'k 2 where each propositional letter pi has been replaced by pi+2. We have followed the general guidelines for generating a systematic benchmark for modal logics [ 6 ] taking

Finitely satis able formulas k formula into account, in particular: (i) length of the formulas, in terms of the number of symbols, and (ii) modal depth of the formulas. The results of this experiment (carried out on an Intel(R) Core(TM) i7-6700HQ, with a clock of 2.60Ghz, four cores, and 16GB RAM), are shown in Fig. 4; as it can be observed, satis able formulae have been successfully checked up to 3167 symbols (and modal depth of 63) in less than 17 minutes.

In order to generate a similar benchmark for unsatis able formulae, we used a rather straightforward method: we considered an arbitrary set of propositional and modal tautologies (of HS3), and we systematically applied universal substitution to generate longer and longer tautologies; we then tested their negation for satis ability. It turns out that the elapsed time for testing a satis able formula grows proportionally to the length and the modal depth of formulae, while for unsatis able ones they di er; therefore there is a single plot in the rst case, and two di erent plots in the second one. The apparent erratic behaviour for unsatis able formulas is probably due to the absence of speci c optimization policies for this case: therefore, the time needed to establish that a formula is not satis able depends too much on the depth at which a contradiction is found. 5

Conclusions

In this paper we have described an e cient implementation of a tableau-based reasoner for the interval temporal logic HS3, whose nite satis ability problem

1;400 ) 1;200 s nd 1;000 o sce 800 i(n 600 em 400 i T 200 0 20 40 60 100 120 140

160 80

Length of ' had been shown to be PSpace-complete in [ 26 ]. The experiments showed that we are able to check the satis ability of relatively long formulas with a relatively high modal depth. There are several considerations that can be drawn from our experiments. Tableau-based satis ability checkers are notoriously not very e cient with formulas with a very relevant propositional component. In the case of unsatis able formulas, branch pruning is the main strategy to improve the performance of the reasoner. Our implementation allows for experimenting with rules for branch pruning thanks to the e cient representation of the branch information; since the underlying problem is PSpace, we expect our implementation to be very susceptible to optimizations. On the other hand, for satis able formulas, the main problem relies in branch selection: being able to choose the most promising branch is one of the most important optimizations tools for a tableau-based procedure. As far as branch selection is concerned, our policies can be seen as a rst step in this direction, but, as future work, we plan to experiment in innovative and much more aggressive strategies for branch selection. In particular, we are looking into describing this problem as a machine learning problem, and designing an intelligent system that is able to quickly select the most promising branch based on previous experience on the same problem, improving in this way the performance on satis able formulas.

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. F. Allen . Maintaining knowledge about temporal intervals . Communications of the ACM , 26 ( 11 ): 832 { 843 , 1983 .

3. A. Artale , D. Bresolin , A. Montanari , V. Ryzhikov , and G. Sciavicco. DL-lite and interval temporal logics: A marriage proposal . In Proc. of the 21st European Conference of Arti cial Intelligence (ECAI) , pages 957 { 958 , 2014 .

4. A. Artale and E. Franconi . A temporal Description Logic for reasoning about actions and plans . Journal of Arti cial Intelligence Reasoning , 9 : 463 { 506 , 1998 .

5. A. Artale , V. Ryzhikov , R. Kontchakov , and M. Zakharyaschev . A cookbook for temporal conceptual data modelling with Description Logics . ACM Transaction on Computational Logic , 15 ( 3 ):1{ 50 , 2014 .

6. P. Balsiger , A. Heuerding , and S. Schwendimann . A benchmark method for the propositional modal logics K, KT, S4 . Journal of Automated Reasoning , 24 ( 3 ): 297 { 317 , 2000 .

7. C. Bettini . Time-dependent concepts: Representation and reasoning using temporal description logics . Data Knowedge Engeneering , 22 ( 1 ):1{ 38 , 1997 .

8. H. Bowman and S. J. Thompson . A tableau method for interval temporal logic with projection . In Proc. of the Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX) , volume 1397 of LNCS , pages 108 { 123 , 1998 .

9. D. Bresolin , D. Della Monica , A. Montanari , and G. Sciavicco . A tableau system for Right Propositional Neighborhood Logic over nite linear orders: an implementation . In Proc. of the 22th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX) , volume 8123 of LNCS , pages 74 { 80 , 2013 .

10. D. Bresolin , D. Della Monica , A. Montanari , and G. Sciavicco. 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 .

11. D. Bresolin , V. Goranko , A. Montanari , and P. Sala . Tableaux for logics of subinterval structures over dense orderings . Journal of Logic and Computation , 20 ( 1 ): 133 { 166 , 2010 .

12. D. Bresolin , A. Kurucz , E. Mun~oz- Velasco , V. Ryzhikov , G. Sciavicco, and M. Zakharyaschev . Horn fragments of the Halpern-Shoham interval temporal logic . ACM Transactions on Computational Logic (TOCL) , Accepted , 2017 .

13. 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 .

14. D. Bresolin , E. Mun~oz- Velasco , and G. Sciavicco . Sub-propositional fragments of the interval temporal logic of Allen's relations . In Proc. of the 14th European Conference on Logics in Arti cial Intelligence (JELIA) , volume 8761 of LNCS , pages 122 { 136 , 2014 .

15. Z. Chaochen and M. R. Hansen . Duration Calculus: A Formal Approach to RealTime Systems . EATCS: Monographs in Theoretical Computer Science. Springer, 2004 .

16. L. Farin~as del Cerro , D. Fauthoux , O. Gasquet , A. Herzig , D. Longin , and F. Massacci . Lotrec : The generic tableau prover for modal and description logics . In Proc. of the 1st International Joint Conference on Automated Reasoning (IJCAR) , pages 453 { 458 , 2001 .

17. M.C. Golumbic and R. Shamir . Complexity and algorithms for reasoning about time: A graph-theoretic approach . Journal of the ACM , 40 ( 5 ): 1108 { 1133 , 1993 .

18. V. Goranko , A. Kyrilov , and D. Shkatov . Tableau tool for testing satis ability in LTL: Implementation and experimental analysis . Electr. Notes Theor. Comput. Sci. , 262 : 113 { 125 , 2010 .

19. V. Goranko , A. Montanari , and G. Sciavicco . Propositional interval neighborhood temporal logics . Journal of Universal Computer Science , 9 ( 9 ): 1137 { 1167 , 2003 .

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

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

22. D. Della Monica , A. Montanari , G. Sciavicco, and D. Tishkovsky . First steps towards automated synthesis of tableau systems for interval temporal logics . In Proc. of the 5th International Conference on Computational Logics , Algebras, Programming, Tools, and Benchmarking ( COMPUTATION TOOLS) , pages 32 { 37 , 2014 .

23. A. Montanari , I. Pratt-Hartmann, and P. Sala . Decidability of the logics of the re exive sub-interval and super-interval relations over nite linear orders . In Proc. of the 17th International Symposium on Temporal Representation and Reasoning (TIME) , pages 27 { 34 . IEEE Computer Society, 2010 .

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

25. B. Moszkowski . Reasoning about digital circuits . PhD thesis , Dept. of Computer Science, Stanford University, Stanford, CA, 1983 .

26. E. Mun ~oz- Velasco , M. Pelegr n-Garc a , P. Sala, and G. Sciavicco . On coarser interval temporal logics and their satis ability problem . In Proc. of the 16th Conference of the Spanish Association for Arti cial Intelligence (CAEPIA 2015 ), volume 9422 of LNAI , pages 1 { 11 , 2015 .

27. I. Pratt-Hartmann . Temporal prepositions and their logic . Arti cial Intelligence , 166 ( 1 {2):1{ 36 , 2005 .

28. A. Schmiedel . Temporal terminological logic . In Proc. of the 8th National Conference on Arti cial Intelligence (AAAI) , pages 640 { 645 . AAAI Press, 1990 .

29. S. Schwendimann . A new one-pass tableau calculus for PLTL . In Proc. of the 4th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods , pages 277 { 291 . Springer, 1998 .

30. D. Tishkovsky , R.A. Schmidt , and M. Khodadadi . The tableau prover generator MetTeL2 . In Proc. of the 13th European Conference on Logics in Arti cial Intelligence (JELIA) , pages 492 { 495 , 2012 .

31. M.Y. Vardi and P. Wolper . Automata theoretic techniques for modal logics of programs (extended abstract) . In Proc. of the 16th Annual ACM Symposium on Theory of Computing (STOC 1984 ), pages 446 { 456 , 1984 .

32. F. Zemke . What's new in SQL:2011 . SIGMOD Record, 41 ( 1 ): 67 { 73 , 2012 .