A central goal of language theory is to compare formalisms by understanding both their expressive overlaps and their relative expressive power. One particularly challenging question in this direction is the problem of determining the common fragment of two formalisms F₁ and F₂, that is, effectively characterise the class F₁∩ F₂ of properties that can be expressed in both formalisms. This question can be equally phrased as a decision problem: given a property expressed in F₁ or F₂, decide whether the same property can be also expressed in F₁∩ F₂. A question closely related to this is the membership problem, denoted F₁ ↦ F₂, which asks whether a property expressed in F₁ can be also expressed in F₂. These problems become particularly difficult when branching-time formalisms are involved, in general due to the lack of equivalent algebraic characterizations. In this work, we prove that LTL ∩ PCTL is decidable, where PCTL denotes CTL extended with past operators. We do this by showing that both membership problems, LTL ↦ PCTL and PCTL ↦ LTL, are decidable. The direction PCTL ↦ LTL follows from suitable combinations of known results. The converse direction, LTL ↦ PCTL, requires an automata-theoretic characterisation of PCTL. Specifically, we introduce a new class of automata, called counter-free hesitant weak tree automata (HWT_cf) that capture precisely the expressiveness of PCTL, and that are obtained by combining two orthogonal restrictions on alternating parity tree automata, namely, counter-free hesitancy and weakness. We then prove that, for every word language L defined by an LTL formula, the associated tree language △[L] is recognisable by an HWT_cf if and only if L is recognized by a deterministic Büchi word automaton. Since the latter recognisability problem is known to be decidable, so is the former. This result advances the longstanding open problem of deciding LTL ∩ CTL. Indeed, that problem can now be reduced to PCTL ↦ CTL, that is, the question of when past operators can be eliminated.

In this paper, we study the finite satisfiability problem for the logic BE under the homogeneity assumption. BE is the cornerstone of Halpern and Shoham’s interval temporal logic, and features modal operators corresponding to the prefix (a.k.a. "Begins") and suffix (a.k.a. "Ends") relations on intervals. In terms of complexity, BE lies in between the "Chop" logic C, whose satisfiability problem is known to be non-elementary, and the PSpace-complete interval logic D of the sub-interval (a.k.a. "During") relation. BE was shown to be ExpSpace-hard, and the only known satisfiability procedure is primitive recursive, but not elementary. Our contribution consists of tightening the complexity bounds of the satisfiability problem for BE, by proving it to be ExpSpace-complete. We do so by devising an equi-satisfiable normal form with boundedly many nested modalities. The normalization technique resembles Scott’s quantifier elimination, but it turns out to be much more involved due to the limitations enforced by the homogeneity assumption.

Hintikka and Sandu originally proposed Independence Friendly Logic (IF) as a first-order logic of imperfect information to describe game-theoretic phenomena underlying the semantics of natural language.The logic allows for expressing independence constraints among quantified variables, in a similar vein to Henkin quantifiers, and has a nice game-theoretic semantics in terms of imperfect information games.However, the IF semantics exhibits some limitations, at least from a purely logical perspective.It treats the players asymmetrically, considering only one of the two players as having imperfect information when evaluating truth, resp., falsity, of a sentence.In addition, truth and falsity of sentences coincide with the existence of a uniform winning strategy for one of the two players in the semantic imperfect information game.As a consequence, IF does admit undetermined sentences, which are neither true nor false, thus failing the law of excluded middle.These idiosyncrasies limit its expressive power to the existential fragment of Second Order Logic (Sol).In this paper, we investigate an extension of IF, called Alternating Dependence/Independence Friendly Logic (ADIF), tailored to overcome these limitations.To this end, we introduce a novel compositional semantics, generalising the one based on trumps proposed by Hodges for IF.The new semantics (i) allows for meaningfully restricting both players at the same time, (ii) enjoys the property of game-theoretic determinacy, (iii) recovers the law of excluded middle for sentences, and (iv) grants ADIF the full descriptive power of Sol.We also provide an equivalent Herbrand-Skolem semantics and a gametheoretic semantics for the prenex fragment of ADIF, the latter being defined in terms of a determined infinite-duration game that precisely captures the other two semantics on finite structures.

An extension of QPTL is considered where functional dependencies among the quantified variables can be restricted in such a way that their current values are independent of the future values of the other variables. This restriction is tightly connected to the notion of behavioral strategies in game-theory and allows the resulting logic to naturally express game-theoretic concepts. Inspired by the work on logics of dependence and independence, we provide a new compositional semantics for QPTL that allows for expressing such functional dependencies among variables. The fragment where only restricted quantifications are considered, called behavioral quantifications , allows for linear-time properties that are satisfiable if and only if they are realisable in the Pnueli-Rosner sense. This fragment can be decided, for both model checking and satisfiability , in 2 Exp Time and is expressively equivalent to QPTL , though significantly less succinct.

Temporal reasoning based on intervals is nowadays ubiquitous in artificial intelligence, and the most representative interval temporal logic, called HS, was introduced by Halpern and Shoham in the eighties. There has been a great effort in the past in studying the expressive power and computational properties of the satisfiability problem for HS and its fragments, but only recently HS has been proposed as a suitable formalism for artificial intelligence applications. Such applications highlighted some of the intrinsic limits of HS: Sometimes, when dealing with real-life data one is not able to express temporal relations and propositional labels in a definite, crisp way. In this paper, following the seminal ideas of Fitting and Zadeh, among others, we present a fuzzy generalization of HS that partially solves such problems of expressive power, and we prove that, as in the crisp case, its satisfiability problem is generally undecidable.

The timeline-based approach to automated planning was originally developed in the context of space missions. In this approach, problem domains are expressed as systems consisting of independent but interacting components whose behaviors over time, the timelines, are governed by a set of temporal constraints, called synchronization rules. Although timeline-based system descriptions have been successfully used in practice for decades, the research on the theoretical aspects only started recently. In the last few years, some interesting results have been shown concerning both its expressive power and the computational complexity of the related planning problem. In particular, the general problem has been proved to be EXPSPACE-complete. Given the applicability of the approach in many practical scenarios, it is thus natural to ask whether computationally simpler but still expressive fragments can be identified. In this paper, we study the timeline-based planning problem with the restriction that only qualitative synchronization rules, i.e., rules without explicit time bounds in the constraints, are allowed. We show that the problem becomes PSPACE-complete.

Within the timeline-based framework, planning problems are modeled as sets of independent, but interacting, components whose behavior over time is described by a set of temporal constraints. Timeline-based planning is being used successfully in a number of complex tasks, but its theoretical properties are not so well studied. In particular, while it is known that Linear Temporal Logic (LTL) can capture classical action-based planning, a similar logical characterization was not available for timeline-based planning formalisms. This paper shows that timeline-based planning with bounded temporal constraints can be captured by a bounded version of Timed Propositional Temporal Logic, augmented with past operators, which is an extension of LTL originally designed for the verification of real-time systems. As a byproduct, we get that the proposed logic is expressive enough to capture temporal action-based planning problems.

The problem of temporal dataset evaluation consists in establishing to what extent a set of temporal data (histories) complies with a given temporal condition. It presents a strong resemblance with the problem of model checking enhanced with the ability of rating the compliance degree of a model against a formula. In this paper, we solve the temporal dataset evaluation problem by suitably combining the outcomes of model checking an interval temporal logic formula against sets of histories (finite interval models), possibly taking into account domain-dependent measures/criteria, like, for instance, sensitivity, specificity, and accuracy. From a technical point of view, the main contribution of the paper is a (deterministic) polynomial time algorithm for interval temporal logic model checking over finite interval models. To the best of our knowledge, this is the first application of a (truly) interval temporal logic model checking in the area of temporal databases and data mining rather than in the formal verification setting.

Interval temporal logics are temporal logics that take time intervals, instead of time instants, as their primitive temporal entities. One of the most studied interval temporal logics is Halpern and Shoham's modal logic of time intervals (HS), which has a distinct modality for each binary relation between intervals over a linear order. As HS turns out to be undecidable over most classes of linear orders, the study of HS fragments, featuring a proper subset of HS modalities, is a major item in the research agenda for interval temporal logics. A characterization of HS fragments in terms of their relative expressive power has been given for the class of all linear orders. Unfortunately, there is no easy way to directly transfer such a result to other meaningful classes of linear orders. In this paper, we provide a complete classification of the expressiveness of HS fragments over the class of (all) dense linear orders.

We compare the expressiveness of the fragments of Halpern and Shoham’s interval logic (HS), i.e., of all interval logics with modal operators associated with Allen’s relations between intervals in linear orders. We establish a complete set of interdefinability equations between these modal operators, and thus obtain a complete classification of the family of 2^12 fragments of HS with respect to their expressiveness. Using that result and a computer program, we have found that there are 1347 expressively different such interval logics over the class of all linear orders.

Unlike the Moon, the dark side of interval temporal logics is the one we usually see: their ubiquitous undesirability. Identifying minimal undecidable interval logics is thus a natural and important issue in the research agenda in the area. The decidability status of a logic often depends on the class of models (in our case, the class of interval structures)in which it is interpreted. In this paper, we have identified several new minimal undecidable logics amongst the fragments of Halpern-Shoham logic HS, including the logic of the overlaps relation, over the classes of all and finite linear orders, as well as the logic of the meet and subinterval relations, over the class of dense linear orders. Together with previous undecid ability results, this work contributes to delineate the border of the dark side of interval temporal logics quite sharply.

Decidability and complexity of the satisfiability problem for the logics of time intervals have been extensively studied in the last years. Even though most interval logics turnout to be undecidable, meaningful exceptions exist, such as the logics of temporal neighborhood and (some of) the logics of the subinterval relation. In this paper, we explore a different path to decidability: instead of restricting the set of modalities or imposing suitable semantic restrictions, we take the most expressive interval temporal logic studied so far, namely, Venema's CDT, and we suitably limit the nesting degree of modalities. The decidability of the satisfiability problem for the resulting CDT fragment is proved by embedding it into a well-known decidable prefix quantifier class of first-order logic, namely, the Bernays-Schonfinkel's class. In addition, we show that such a fragment is in fact NP-complete (theBernays-Schonfinkel's class is NEXPTIME-complete), and that any natural extension of it is undecidable.

Interval temporal logics formalize reasoning about interval structures over (usually) linearly ordered domains, where time intervals are the primitive ontological entities and truth of formulae is defined relative to time intervals, rather than time points. In this paper, we introduce and study Metric Propositional Neighborhood Logic (MPNL) over natural numbers. MPNL features two modalities referring, respectively, to an interval that is “met by” the current one and to an interval that “meets” the current one, plus an infinite set of length constraints, regarded as atomic propositions, to constrain the lengths of intervals. We argue that MPNL can be successfully used in different areas of artificial intelligence to combine qualitative and quantitative interval temporal reasoning, thus providing a viable alternative to well-established logical frameworks such as Duration Calculus. We show that MPNL is decidable in double exponential time and expressively complete with respect to a well-defined subfragment of the two-variable fragment FO2[N, =, <, s] of first-order logic for linear orders with successor function, interpreted over natural numbers. Moreover, we show that MPNL can be extended in a natural way to cover full FO2[N, =, <, s], but, unexpectedly, the latter (and hence the former) turns out to be undecidable.

Temporal reasoning plays an important role in artificial intelligence. Temporal logics provide a natural framework for its formalization and implementation. A standard way of enhancing the expressive power of temporal logics is to replace their unidimensional domain by a multidimensional one. In particular, such a dimensional increase can be exploited to obtain spatial counterparts of temporal logics. Unfortunately, it often involves a blow up in complexity, possibly losing decidability. In this paper, we propose a spatial generalization of the decidable metric interval temporal logic RPNL+INT, called Directional Area Calculus (DAC). DAC features two modalities, that respectively capture (possibly empty) rectangles to the north and to the east of the current one, and metric operators, to constrain the size of the current rectangle. We prove the decidability of the satisfiability problem for DAC, when interpreted over frames built on natural numbers, and we analyze its complexity. In addition, we consider a weakened version of DAC, called WDAC, which is expressive enough to capture meaningful qualitative and quantitative spatial properties and computationally better.

We investigate fragments of Halpern-Shoham's interval logic HS involving the modal operators for the relations of left or right overlap of intervals. We prove that most of these fragments are undecidable, by employing a non-trivial reduction from the octant tiling problem.