Due to its expressiveness and unambiguous nature, First-Order Logic (FOL) is a powerful formalism for representing concepts expressed in natural language (NL). This is useful, e.g., for specifying and verifying desired system properties. While translating FOL into human-readable English is relatively straightforward, the inverse problem, converting NL to FOL (NL-FOL translation), has remained a longstanding challenge, for both humans and machines. Although the emergence of Large Language Models (LLMs) promised a breakthrough, recent literature provides contrasting results on their ability to perform NL-FOL translation. In this work, we provide a threefold contribution. First, we critically examine existing datasets and protocols for evaluating NL-FOL translation performance, revealing key limitations that may cause a misrepresentation of LLMs' actual capabilities. Second, to overcome these shortcomings, we propose a novel evaluation protocol explicitly designed to distinguish genuine semantic-level logical understanding from superficial pattern recognition, memorization, and dataset contamination. Third, using this new approach, we show that state-of-the-art, dialogue-oriented LLMs demonstrate strong NL-FOL translation skills and a genuine grasp of sentence-level logic, whereas embedding-centric models perform markedly worse.

In runtime verification, monitoring consists of analyzing the current execution of a system and determining, on the basis of the observed finite trace, whether all its possible continuations satisfy or violate a given specification. This is typically done by synthesizing a monitor–often a Deterministic Finite State Automaton (DFA)–from logical specifications expressed in Linear Temporal Logic (LTL) or in its finite-word variant (LTLf). Unfortunately, the size of the resulting DFA may incur a doubly exponential blow-up in the size of the formula. In this paper, we identify some conditions under which monitoring can be done without constructing such a DFA. We build on the notion of intentionally safe and cosafe formulas to show that monitoring of these formulas can be carried out through trace-checking, that is, by directly evaluating them on the current system trace, with a polynomial complexity in the size of both the trace and the formula. In addition, we investigate the complexity of recognizing intentionally safe and cosafe formulas for the safety and cosafety fragments of LTL and LTLf. As for LTLf, we show that all formulas in these fragments are intentionally safe and cosafe, thus removing the need for the check. As for LTL, we prove that the problem is in PSPACE, significantly improving over the EXPSPACE complexity of full LTL.

We investigate a fragment of Linear Temporal Logic (LTL) comprising the tomorrow (X) and eventually (F) modalities, and present a singly exponential time algorithm for the pastification problem within this fragment. The pastification problem consists of constructing, for a given LTL formula, an equivalent formula that exclusively employs past temporal operators. While the best known algorithms for this task in full LTL–and in the fragment under consideration–exhibit triply exponential time complexity, our approach achieves optimal complexity for this fragment. The proposed algorithm proceeds in two main stages: (i) the input formula is first translated into a tailored normal form, and then (ii) a pure past formula is synthesized from a tree-like structure derived from the normalized formula. With minor adaptations, the algorithm extends to handle the fragment of LTL featuring the tomorrow and globally modalities. We provide an implementation of the algorithm in the temporal reasoning tool BLACK, and report on an experimental evaluation of its performance.1

Monitoring is a runtime verification technique that allows one to check whether an ongoing computation of a system (partial trace) satisfies a given formula. It does not need a complete model of the system, but it typically requires the construction of a deterministic automaton doubly exponential in the size of the formula (in the worst case), which limits its practicality. In this paper, we show that, when considering finite, discrete traces, monitoring of pure past (co)safety fragments of Signal Temporal Logic (STL) can be reduced to trace checking, that is, evaluation of a formula over a trace, that can be performed in time polynomial in the size of the formula and the length of the trace. By exploiting such a result, we develop a GPU-accelerated framework for interpretable early failure detection based on vectorized trace checking, that employs genetic programming to learn temporal properties from historical trace data. The framework shows a 2–10% net improvement in key performance metrics compared to the state-of-the-art methods.

Krohn-Rhodes theory encompasses the techniques for the study of finite automata and their decomposition into elementary automata. The famous result of Krohn and Rhodes roughly states that each finite automaton can be decomposed into elementary components which correspond to permutation and reset automata connected by a cascade product. However, this outcome is not easy to access for the working computer scientist. This paper provides a short introduction into Krohn-Rhodes theory based on the valuable work of Ginzburg.

Linear Temporal Logic over finite traces ( LTL f ) has proved itself to be an important and effective formalism in formal verification as well as in artificial intelligence. Pure past LTL f ( pLTL ) is the variant of LTL f featuring only past temporal modalities, and is naturally interpreted at the end of a finite trace. It is known that each property definable in LTL f is also definable in pLTL , and vice versa (they are expressively equivalent). The same goes for the safety and cosafety fragments of Linear Temporal Logic over infinite traces ( LTL ), when compared to G ( pLTL ) and F ( pLTL ) formulas, respectively, that is, pLTL formulas prefixed by a globally and an eventually modality. However, despite being extensively used in practice, to the best of our knowledge, there is no systematic study of their succinctness. Moreover, when considering (co)safety fragments of LTL devoid of binary temporal modalities, there are no known characterizations based on pLTL . In this paper, we investigate succinctness issues for LTL f and (co)safety fragments of LTL when compared with their pure past counterparts. First, we provide a pure past characterization of the (co)safety fragments of LTL devoid of binary temporal modalities. Then, we prove that the (co)safety fragments of LTL have pure past counterparts that can be exponentially more succinct. Finally, we show that the same holds for LTL f with respect to pLTL , and viceversa: LTL f and pLTL are incomparable when succinctness is concerned.

Abstract This paper focuses on succinctness results for fragments of Linear Temporal Logic with Past ( $$\textsf{LTL}$$ LTL ) devoid of binary temporal operators like until, and provides methods to establish them. We prove that there is a family of cosafety languages $$(\mathcal {L}_n)_{n \ge 1}$$ ( L n ) n ≥ 1 such that $$\mathcal {L}_n$$ L n can be expressed with a pure future formula of size $$\mathcal {O}(n)$$ O ( n ) , but it requires formulae of size $$2^{\varOmega (n)}$$ 2 Ω ( n ) to be captured with past formulae. As a by-product, such a succinctness result shows the optimality of the pastification algorithm proposed in [Artale et al., KR, 2023]. We show that, in the considered case, succinctness cannot be proven by relying on the classical automata-based method introduced in [Markey, Bull. EATCS, 2003]. In place of this method, we devise and apply a combinatorial proof system whose deduction trees represent $$\textsf{LTL}$$ LTL formulae. The system can be seen as a proof-centric (one-player) view on the games used by Adler and Immerman to study the succinctness of $$\textsf{CTL}$$ CTL .

Abstract Linear temporal logic( $$\textsf{LTL}\,$$ LTL ) and its variant interpreted onfinite traces( $$\textsf{LTL}_{\textsf{f}\,}$$ LTLf ) are among the most popular specification languages in the fields of formal verification, artificial intelligence, and others. In this paper, we focus on the satisfiability problem for $$\textsf{LTL}\,$$ LTL and $$\textsf{LTL}_{\textsf{f}\,}$$ LTLf formulas, for which many techniques have been devised during the last decades. Among these aretableau systems, of which the most recent is Reynolds’ tree-shaped tableau. We provide a SAT-based algorithm for $$\textsf{LTL}\,$$ LTL and $$\textsf{LTL}_{\textsf{f}\,}$$ LTLf satisfiability checking based on Reynolds’ tableau, proving its correctness and discussing experimental results obtained through its implementation in the BLACK satisfiability checker.

In the timeline-based approach to planning, the evolution over time of a set of state variables (the timelines) is governed by a set of temporal constraints. Traditional timeline-based planning systems excel at the integration of planning with execution by handling temporal uncertainty. In order to handle general nondeterminism as well, the concept of timeline-based games has been recently introduced. It has been proved that finding whether a winning strategy exists for such games is 2EXPTIME-complete. However, a concrete approach to synthesize controllers implementing such strategies is missing. This paper fills this gap, by providing an effective and computationally optimal approach to controller synthesis for timeline-based games.

A classic result by Stockmeyer gives a non-elementary lower bound to the emptiness problem for star-free generalized regular expressions. This result is intimately connected to the satisfiability problem for interval temporal logic, notably for formulas that make use of the so-called chop operator. Such an operator can indeed be interpreted as the inverse of the concatenation operation on regular languages, and this correspondence enables reductions between non-emptiness of star-free generalized regular expressions and satisfiability of formulas of the interval temporal logic of chop under the homogeneity assumption. In this paper, we study the complexity of the satisfiability problem for suitable weakenings of the chop interval temporal logic, that can be equivalently viewed as fragments of Halpern and Shoham interval logic. We first consider the logic $\mathsf{BD}_{hom}$ featuring modalities $B$, for \emph{begins}, corresponding to the prefix relation on pairs of intervals, and $D$, for \emph{during}, corresponding to the infix relation. The homogeneous models of $\mathsf{BD}_{hom}$ naturally correspond to languages defined by restricted forms of regular expressions, that use union, complementation, and the inverses of the prefix and infix relations. Such a fragment has been recently shown to be PSPACE-complete . In this paper, we study the extension $\mathsf{BD}_{hom}$ with the temporal neighborhood modality $A$ (corresponding to the Allen relation \emph{Meets}), and prove that it increases both its expressiveness and complexity. In particular, we show that the resulting logic $\mathsf{BDA}_{hom}$ is EXPSPACE-complete.

Abstract Realizability and reactive synthesis from temporal logics are fundamental problems in formal verification. The complexity of these problems for linear temporal logic with past ( ) led to the identification of fragments with lower complexities and simpler algorithms. Recently, the logic of extended bounded response ( $$\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} $$ LTLEBR+P for short) has been introduced. It allows one to express safety languages definable in and it is provided with an efficient, fully symbolic algorithm for reactive synthesis. This paper features four related contributions. First, we introduce - , an extension of $$\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} $$ LTLEBR+P with fairness conditions, assumptions, and guarantees that, on the one hand, allows one to express properties beyond the safety fragment and, on the other, it retains the efficiency of $$\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} $$ LTLEBR+P in practice. Second, we the expressiveness of - starting from the expressiveness of its fragments. In particular, we prove that: (1) $$\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} $$ LTLEBR+P is expressively complete with respect to the safety fragment of , (2) the removal of past operators from $$\textsf {LTL} _{\textsf {EBR} }\textsf {{+}P} $$ LTLEBR+P results into a loss of expressive power, and (3) - is expressively equivalent to the logic of Bloem et al. Third, we provide a fully symbolic algorithm for the realizability problem from - specifications, that reduces it to a number of safety subproblems. Fourth, to ensure soundness and completeness of the algorithm, we propose and exploit a general framework for safety reductions in the context of realizability of (fragments of) . The experimental evaluation shows promising results.

Linear Temporal Logic (LTL) is the de-facto standard temporal logic for system specification, whose foundational properties have been studied for over five decades. Safety and cosafety properties of LTL define notable fragments of LTL, where a prefix of a trace suffices to establish whether a formula is true or not over that trace. In this paper, we study the complexity of the problems of satisfiability, validity, and realizability over infinite and finite traces for the safety and cosafety fragments of LTL. As for satisfiability and validity over infinite traces, we prove that the majority of the fragments have the same complexity as full LTL, that is, they are PSPACE-complete. The picture is radically different for realizability: we find fragments with the same expressive power whose complexity varies from 2EXPTIME-complete (as full LTL) to EXPTIME-complete. Notably, for all cosafety fragments, the complexity of the three problems does not change passing from infinite to finite traces, while for all safety fragments the complexity of satisfiability (resp., realizability) over finite traces drops to NP-complete (resp., Πᴾ₂- complete).

Confronting the past can be hard. This is true even in Linear Temporal Logic (LTL), interpreted on either infinite or finite traces, when faced with the problem of transforming a temporally future formula into an equivalent one that contains past temporal modalities only. To our knowledge, the best among the available pastification procedures for full LTL, as well as for expressive enough fragments of it (that is, containing at least one temporal modality other than tomorrow), are triply exponential in the size of the input. In this paper, we focus on the fragment of LTL that features the tomorrow and eventually modalities, and provide a singly exponential pastification algorithm for it. The transformation is based on a normalisation procedure that requires a non-trivial complexity analysis, and on the subsequent generation of a pure past formula from suitably-defined dependency tree structures. Moreover, leveraging its purely syntactic nature, we present an implementation of our procedure in a temporal satisfiability checking tool that deals with both future and past modalities.

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.

Fingerprinting is a common localisation approach that often estimates a device's position by comparing an observed vector to a set of prior vectors labelled with a ground truth location, typically using methods like k-NN. In Wi-Fi fingerprinting, these vectors represent visible access points and their signal strength. Thus, the choice of metric to compare the fingerprints is crucial. In this work, we discuss our main findings regarding the extent to which metrics in the fingerprint vector space preserve relationships among locations in the 2D/3D geometric/real world. In summary, traditional metrics are not optimal on their own, and while combining them into a learned meta-metric offers slight improvements, deep metric learning, i.e., learning similarities in an end-to-end fashion with deep neural networks, appears much more effective. However, this approach has its challenges given that in the literature the problem has only been formulated for binary similarities rather than continuous ones.

In a world increasingly pervaded by mobile and IoT devices, position-related information is gaining more and more importance. Highly accurate and standardized positioning techniques are not yet available for indoor scenarios, unlike for the outdoor case. The most commonly used method for indoor positioning is WiFi fingerprinting, which, despite its well-recognized advantages, still suffers from some notable limitations. Recently, approaches relying on deep learning showed promising results even though their lack of interpretability is still a significant drawback. In this paper, for the first time, we propose a domain-specific concept of interpretability, based on identifying the access points that are most relevant to a position estimate. The goal is to enhance the positioning process by gaining novel scientific knowledge and operational insights, without worsening the performance of the task. We show how it is possible to practically achieve both a local and a global notion of interpretability by means of a deep learning model equipped with an attention module, applied to a ranking based fingerprint representation. Since off-the-shelf application of attention does not guarantee to achieve a faithful nor plausible interpretation, we verified through a series of thoroughly designed quantitative and qualitative clustering based experiments the existence of a strong relationship between the obtained interpretations and the positioning domain. Finally, as by-product, we showed an example of how the new knowledge can be used in principle to improve positioning performance.

In this paper, we prove Pspace-completeness of the finite satisfiability and model checking problems for the fragment of Halpern and Shoham interval logic with modality , for the “suffix” relation on pairs of intervals, and modality , for the “sub-interval” relation, under the homogeneity assumption. The result significantly improves the Expspace upper bound recently established for the same fragment, and proves the rather surprising fact that the complexity of the considered problems does not change when we add either the modality for suffixes () or, symmetrically, the modality for prefixes () to the logic of sub-intervals (featuring only ).

Linear Temporal Logic (LTL) is one of the most popular temporal logics, that comes into play in a variety of branches of computer science. Among the various reasons of its widespread use there are its strong foundational properties: LTL is equivalent to counter-free omega-automata, to star-free omega-regular expressions, and (by Kamp's theorem) to the First-Order Theory of Linear Orders (FO-TLO). Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not belong or belongs to the language, respectively, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis for LTL. SafetyLTL (resp., coSafetyLTL) is a fragment of LTL where only universal (resp., existential) temporal modalities are allowed, that recognises safety (resp., co-safety) languages only. The main contribution of this paper is the introduction of a fragment of FO-TLO, called SafetyFO, and of its dual coSafetyFO, which are expressively complete with respect to the LTL-definable safety and co-safety languages. We prove that they exactly characterize SafetyLTL and coSafetyLTL, respectively, a result that joins Kamp's theorem, and provides a clearer view of the characterization of (fragments of) LTL in terms of first-order languages. In addition, it gives a direct, compact, and self-contained proof that any safety language definable in LTL is definable in SafetyLTL as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow operator of SafetyLTL, interpreted over finite and infinite words. Moreover, we prove that, when interpreted over finite words, SafetyLTL (resp. coSafetyLTL) devoid of the tomorrow (resp., weak tomorrow) operator captures the safety (resp., co-safety) fragment of LTL over finite words.

In this article, we introduce and investigate an extension of Halpern and Shoham’s interval temporal logic HS for the specification and verification of branching-time context-free requirements of pushdown systems under a state-based semantics over Kripke structures enforcing visibility of the pushdown operations. The proposed logic, called nested BHS , supports branching-time both in the past and in the future and is able to express non-regular properties of linear and branching behaviours of procedural contexts in a natural way. It strictly subsumes well-known linear time context-free extensions of LTL such as CaRet [ 4 ] and NWTL [ 2 ]. The main result is the decidability of the visibly pushdown model-checking problem against nested BHS . The proof exploits a non-trivial automata-theoretic construction.

Abstract Linear Temporal Logic ( $$\mathsf {LTL}$$ LTL ) is one of the most popular temporal logics, that comes into play in a variety of branches of computer science. Its widespread use is also due to its strong foundational properties. One of them is Kamp’s theorem, showing that $$\mathsf {LTL}$$ LTL and the first-order theory of one successor ( $$\mathsf {S1S}[\mathsf {FO}]$$ S 1 S [ FO ] ) are expressively equivalent. Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not or does belong to the language, respectively, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis for $$\mathsf {LTL}$$ LTL . $$\mathsf {Safety\text {-} \mathsf {LTL}}$$ Safety - LTL (resp., $$\mathsf {coSafety\text {-} \mathsf {LTL}}$$ coSafety - LTL ) is a fragment of $$\mathsf {LTL}$$ LTL where only universal (resp., existential) temporal modalities are allowed, that recognises safety (resp., co-safety) languages only. In this paper, we introduce a fragment of $$\mathsf {S1S}[\mathsf {FO}]$$ S 1 S [ FO ] , called $$\mathsf {Safety\text {-} FO}$$ Safety - FO , and its dual $$\mathsf {coSafety\text {-} FO}$$ coSafety - FO , which are expressively complete with regards to the $$\mathsf {LTL}$$ LTL -definable safety languages. In particular, we prove that they respectively characterise exactly $$\mathsf {Safety\text {-} \mathsf {LTL}}$$ Safety - LTL and $$\mathsf {coSafety\text {-} \mathsf {LTL}}$$ coSafety - LTL , a result that joins Kamp’s theorem, and provides a clearer view of the charactisations of (fragments of) $$\mathsf {LTL}$$ LTL in terms of first-order languages. In addition, it gives a direct, compact, and self-contained proof that any safety language definable in $$\mathsf {LTL}$$ LTL is definable in $$\mathsf {Safety\text {-} \mathsf {LTL}}$$ Safety - LTL as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow operator of $$\mathsf {Safety\text {-} \mathsf {LTL}}$$ Safety - LTL interpreted over finite and infinite traces.

In this paper, we study the computational complexity of action-based temporal planning interpreted over dense time. When time is assumed to be discrete, the problem is known to be EXPSPACE-complete. However, the official PDDL 2.1 semantics and many implementations interpret time as a dense domain. This work provides several results about the complexity of the problem, focusing on some particularly interesting cases: whether a minimum amount ε of separation between mutually exclusive events is given, in contrast to the separation being simply required to be non-zero, and whether or not actions are allowed to overlap already running instances of themselves. We prove the problem to be PSPACE-complete when self-overlap is forbidden, whereas, when it is allowed, it becomes EXPSPACE-complete with ε-separation and even undecidable with non-zero separation. These results clarify the computational consequences of different choices in the definition at the core of the PDDL 2.1 semantics, which have been vague until now.1

The expressive power of interval temporal logics (ITLs) makes them one of the most natural choices in a number of application domains, ranging from the specification and verification of complex reactive systems to automated planning. However, for a long time, because of their high computational complexity, they were considered not suitable for practical purposes. The recent discovery of several computationally well-behaved ITLs has finally changed the scenario. In this paper, we investigate the finite satisfiability and model checking problems for the ITL D, that has a single modality for the sub-interval relation, under the homogeneity assumption (that constrains a proposition letter to hold over an interval if and only if it holds over all its points). We first prove that the satisfiability problem for D, over finite linear orders, is PSPACE-complete, and then we show that the same holds for its model checking problem, over finite Kripke structures. In such a way, we enrich the set of tractable interval temporal logics with a new meaningful representative.

In this paper, we establish Pspace-completeness of the finite satisfiability and model checking problems for the fragment of Halpern and Shoham interval logic with modality ⟨E⟩, for the "suffix" relation on pairs of intervals, and modality ⟨D⟩, for the "sub-interval" relation, under the homogeneity assumption. The result significantly improves the Expspace upper bound recently established for the same fragment, and proves the rather surprising fact that the complexity of the considered problems does not change when we add either the modality for suffixes (⟨E⟩) or, symmetrically, the modality for prefixes (⟨B⟩) to the logic of sub-intervals (featuring only ⟨D⟩).

LTL+Past is the extension of Linear Temporal Logic (LTL) supporting past temporal operators. The addition of the past does not add expressive power, but does increase the usability of the language both in formal verification and in artificial intelligence, e.g., in the context of multi-agent systems. In this paper, we add the support of past operators to BLACK, a satisfiability checker for LTL based on a SAT encoding of a tree-shaped tableau system. We implement two ways of supporting the past in the tool. The first one is an equisatisfiable translation that removes the past operators, obtaining a future-only formula that can be solved with the original LTL engine. The second one extends the SAT encoding of the underlying tableau to directly support the tableau rules that deal with past operators. We describe both approaches and experimentally compare the two between themselves and with the νXmv model checker, obtaining promising results.

This paper studies the computational complexity of temporal planning, as represented by PDDL 2.1, interpreted over dense time. When time is considered discrete, the problem is known to be EXPSPACE-complete. However, the official PDDL 2.1 semantics, and many implementations, interpret time as a dense domain. This work provides several results about the complexity of the problem, studying a few interesting cases: whether a minimum amount ϵ of separation between mutually exclusive events is given, in contrast to the separation being simply required to be non-zero, and whether or not actions are allowed to overlap already running instances of themselves. We prove the problem to be PSPACE-complete when self-overlap is forbidden, whereas, when allowed, it becomes EXPSPACE-complete with ϵ-separation and undecidable with non-zero separation. These results clarify the computational consequences of different choices in the definition of the PDDL 2.1 semantics, which were vague until now.

Reactive synthesis is a key technique for the design of correct-by-construction systems and has been thoroughly investigated in the last decades.It consists in the synthesis of a controller that reacts to environment's inputs satisfying a given temporal logic specification.Common approaches are based on the explicit construction of automata and on their determinization, which limit their scalability.In this paper, we introduce a new fragment of Linear Temporal Logic, called Extended Bounded Response LTL (LTL EBR ), that allows one to combine bounded and universal unbounded temporal operators (thus covering a large set of practical cases), and we show that reactive synthesis from LTL EBR specifications can be reduced to solving a safety game over a deterministic symbolic automaton built directly from the specification.We prove the correctness of the proposed approach and we successfully evaluate it on various benchmarks.

The ability of determining and dealing with the trajectories followed by an object in a given (concrete or abstract) space turns out to be quite useful in a variety of contexts. This is the case, in particular, in positioning, where it can be exploited, for instance, for traffic control and user profiling. A key step in trajectory management is the evaluation of trajectory similarity. In many positioning applications, trajectories are built from Global Navigation Satellite System (GNSS) readings; however, in various scenarios, these coordinates are not available. In this paper, we focus on fingerprint positioning systems characterised by a low sampling frequency and a high heterogeneity of the observations. We start with a comprehensive analysis of well-known GNSS-based trajectory similarity measures, and show how some of them can actually be adapted to the fingerprinting setting. Then, we outline a novel approach that exploits multiple information, including both spatial and cellular identifiers with received signal strength. Finally, we make an extensive, experimental comparative evaluation of the various measures (adapted and novel ones) over a real-world fingerprint dataset.

A classic result by Stockmeyer [Stockmeyer, 1974] gives a non-elementary lower bound to the emptiness problem for star-free generalized regular expressions. This result is intimately connected to the satisfiability problem for interval temporal logic, notably for formulas that make use of the so-called chop operator. Such an operator can indeed be interpreted as the inverse of the concatenation operation on regular languages, and this correspondence enables reductions between non-emptiness of star-free generalized regular expressions and satisfiability of formulas of the interval temporal logic of the chop operator under the homogeneity assumption [Halpern et al., 1983]. In this paper, we study the complexity of the satisfiability problem for a suitable weakening of the chop interval temporal logic, that can be equivalently viewed as a fragment of Halpern and Shoham interval logic featuring the operators B, for "begins", corresponding to the prefix relation on pairs of intervals, and D, for "during", corresponding to the infix relation. The homogeneous models of the considered logic naturally correspond to languages defined by restricted forms of regular expressions, that use union, complementation, and the inverses of the prefix and infix relations.

Positioning is a key task in many different contexts. In the last decades, it has considerably evolved, but, while there are a lot of systems that offer a quite good performance in outdoor scenarios, the indoor realm is still under exploration. Among existing technologies and techniques for indoor positioning, the most popular one makes use of WiFi fingerprints. Such an approach has many advantages; however, its adoption as a standard for everyday life is limited due to issues like the (time) costly radio map construction, and radio signal strength fluctuations in indoor environments. In this paper, we present a novel solution for indoor positioning based on deep learning, that ignores as much as possible signal strengths, in order to reduce the adverse effects associated with their usage. It exploits signal strength only to generate a ranking-based representation of the access points associated with a fingerprint. By developing and testing two recurrent neural network models, we show that the proposed approach is able to achieve a positioning performance, based on access point ranking, comparable to the one achieved by state-of-the-art algorithms on multiple publicly available indoor datasets. As additional benefits, compared to existing ones, the developed solution is considerably more robust to signal fluctuations and simpler in terms of the considered data.

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.

The problem of timeline-based planning (TP) over dense temporal domains is known to be undecidable. In this paper, we introduce two semantic variants of TP, called strong minimal and weak minimal semantics, which allow to express meaningful properties. Both semantics are based on the minimality in the time distances of the existentially-quantified time events from the universally-quantified reference event, but the weak minimal variant distinguishes minimality in the past from minimality in the future. Surprisingly, we show that, despite the (apparently) small difference in the two semantics, for the strong minimal one, the TP problem is still undecidable, while for the weak minimal one, the TP problem is just PSPACE-complete. Membership in PSPACE is determined by exploiting a strictly more expressive extension (ECA^+) of the well-known robust class of Event-Clock Automata (ECA) that allows to encode the weak minimal TP problem and to reduce it to non-emptiness of Timed Automata (TA). Finally, an extension of ECA^+ (ECA^{++}) is considered, proving that its non-emptiness problem is undecidable. We believe that the two extensions of ECA (ECA^+ and ECA^{++}), introduced for technical reasons, are actually valuable per sé in the field of TA.

The model-checking (MC) problem of Halpern and Shoham Interval Temporal Logic (HS) has been recently investigated in some papers and is known to be decidable. An intriguing open question concerns the exact complexity of the problem for full HS: it is at least EXPSPACE-hard, while the only known upper bound is non-elementary and is obtained by exploiting an abstract representation of Kripke structure paths called descriptors. In this paper we generalize the approach by providing a uniform framework for model-checking full HS and meaningful (almost maximal) fragments, where a specialized type of descriptor is defined for each fragment. We then devise a general MC alternating algorithm parameterized by the type of descriptor which has a polynomially bounded number of alternations and whose running time is bounded by the length of minimal representatives of descriptors (certificates). We analyze the time complexity of the algorithm and give, by non-trivial arguments, tight bounds on the length of certificates. For two types of descriptors, we obtain exponential upper and lower bounds which lead to an elementary MC algorithm for the related HS fragments. For the other types of descriptors, we provide non-elementary lower bounds. This last result addresses a question left open in some papers regarding the possibility of fixing an elementary upper bound on the size of the descriptors for full HS.

Linear temporal logic (LTL) is commonly used in model checking tasks; moreover, it is well-suited for the formalization of technical requirements. However, the correct specification and interpretation of temporal logic formulas require a strong mathematical background and can hardly be done by domain experts, who, instead, tend to rely on a natural language description of the intended system behaviour. In such situations, a system that is able to automatically translate English sentences into LTL formulas, and vice versa, would be of great help. While the task of rendering an LTL formula into a more readable English sentence may be carried out in a relatively easy way by properly parsing the formula, the converse is still an open problem, due to the inherent difficulty of interpreting free, natural language texts. Although several partial solutions have been proposed in the past, the literature still lacks a critical assessment of the work done. We address such a shortcoming, presenting the current state of the art for what concerns the English-to-LTL translation problem, and outlining some possible research directions.

Abstract In this work, a data set describing phone interactions arising in a multichannel and multiskill contact centre is considered with the aim of classifying inbound sessions into those that will be eventually managed by an agent and those that, instead, will be abandoned before. More precisely, the goal of the work is to extract interpretable pieces of information that allow us to predict whether a user will or will not abandon a call, which may turn out to be very useful for the purpose of contact centre managing. To this end, the performance of two well‐known, state‐of‐the‐art evolutionary algorithms for feature selection (evolutionary nondominated radial slots based algorithm and nondominated sorted genetic algorithm) is compared for the task of feature selection, under the criteria of accuracy and cardinality of the selection, as well as for the task of fuzzy rule extraction, under the criteria of interpretability, accuracy, and hypervolume test. The best obtained fuzzy classifier, chosen after a decision making process, is validated and interpreted by domain experts.

In recent years, model checking with interval temporal logics is emerging as a viable alternative to model checking with standard point-based temporal logics, such as LTL, CTL, CTL*, and the like. The behavior of the system is modeled by means of (finite) Kripke structures, as usual. However, while temporal logics which are interpreted “point-wise” describe how the system evolves state-by-state, and predicate properties of system states, those which are interpreted “interval-wise” express properties of computation stretches, spanning a sequence of states. A proposition letter is assumed to hold over a computation stretch (interval) if and only if it holds over each component state (homogeneity assumption). A natural question arises: is there any advantage in replacing points by intervals as the primary temporal entities, or is it just a matter of taste? In this article, we study the expressiveness of Halpern and Shoham’s interval temporal logic (HS) in model checking, in comparison with those of LTL, CTL, and CTL*. To this end, we consider three semantic variants of HS: the state-based one, introduced by Montanari et al. in [30, 34], that allows time to branch both in the past and in the future, the computation-tree-based one, that allows time to branch in the future only, and the trace-based variant, that disallows time to branch. These variants are compared among themselves and to the aforementioned standard logics, getting a complete picture. In particular, we show that HS with trace-based semantics is equivalent to LTL (but at least exponentially more succinct), HS with computation-tree-based semantics is equivalent to finitary CTL*, and HS with state-based semantics is incomparable with all of them (LTL, CTL, and CTL*).

In timeline-based planning, domains are described as sets of independent, but interacting, components, whose behaviour over time (the set of timelines) is governed by a set of temporal constraints. A distinguishing feature of timeline-based planning systems is the ability to integrate planning with execution by synthesising control strategies for flexible plans. However, flexible plans can only represent temporal uncertainty, while more complex forms of nondeterminism are needed to deal with a wider range of realistic problems. In this paper, we propose a novel game-theoretic approach to timeline-based planning problems, generalising the state of the art while uniformly handling temporal uncertainty and nondeterminism. We define a general concept of timeline-based game and we show that the notion of winning strategy for these games is strictly more general than that of control strategy for dynamically controllable flexible plans. Moreover, we show that the problem of establishing the existence of such winning strategies is decidable using a doubly exponential amount of space.

In this paper, we investigate the finite satisfiability and model checking problems for the logic D of the sub-interval relation under the homogeneity assumption, that constrains a proposition letter to hold over an interval if and only if it holds over all its points. First, we prove that the satisfiability problem for D, over finite linear orders, is PSPACE-complete; then, we show that its model checking problem, over finite Kripke structures, is PSPACE-complete as well.

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.

Linear Temporal Logic (LTL) is a de-facto standard formalism for expressing properties of systems and temporal constraints in formal verification, artificial intelligence, and other areas of computer science. The problem of LTL satisfiability is thus prominently important to check the consistency of these temporal specifications. Although adding past operators to LTL does not increase its expressive power, recently the interest for explicitly handling the past in temporal logics has increased because of the clarity and succinctness that those operators provide. In this work, a recently proposed one-pass tree-shaped tableau system for LTL is extended to support past operators. The modularity of the required changes provides evidence for the claimed ease of extensibility of this tableau system.

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.

In the last years, model checking with interval temporal logics is emerging as a viable alternative to model checking with standard point-based temporal logics, such as LTL, CTL, CTL*, and the like. The behavior of the system is modeled by means of (finite) Kripke structures, as usual. However, while temporal logics which are interpreted "point-wise" describe how the system evolves state-by-state, and predicate properties of system states, those which are interpreted "interval-wise" express properties of computation stretches, spanning a sequence of states. A proposition letter is assumed to hold over a computation stretch (interval) if and only if it holds over each component state (homogeneity assumption). A natural question arises: is there any advantage in replacing points by intervals as the primary temporal entities, or is it just a matter of taste? In this paper, we study the expressiveness of Halpern and Shoham's interval temporal logic (HS) in model checking, in comparison with those of LTL, CTL, and CTL*. To this end, we consider three semantic variants of HS: the state-based one, introduced by Montanari et al., that allows time to branch both in the past and in the future, the computation-tree-based one, that allows time to branch in the future only, and the trace-based variant, that disallows time to branch. These variants are compared among themselves and to the aforementioned standard logics, getting a complete picture. In particular, we show that HS with trace-based semantics is equivalent to LTL (but at least exponentially more succinct), HS with computation-tree-based semantics is equivalent to finitary CTL*, and HS with state-based semantics is incomparable with all of them (LTL, CTL, and CTL*).

Planning prblems are usually expressed by specifying which actions can be performed to obtain a given goal. In temporal planning problems, actions come with a time duration and can overlap in time, which noticeably increase the complexity of the reasoning process. Action-based temporal planning has been thoroughly studied from the complexity-theoretic point of view, and it has been proved to be EXPSPACE-complete in its general formulation. Conversely, timeline-based planning problems are represented as a collection of variables whose time-varying behavior is governed by a set of temporal constraints, called synchronization rules. Timelines provide a unified framework to reason about planning and execution under uncertainty. Timeline-based systems are being successfully employed in real-world complex tasks, but, in contrast to action-based planning, little is known on their computational complexity and expressiveness. In particular, a comparison of the expressiveness of the action-and timeline-based formalisms is still missing. This paper contributes a first step in this direction by proving that timelines are expressive enough to capture action-based temporal planning, showing as a byproduct the EXPSPACE-completeness of timeline-based planning with no temporal horizon and bounded temporal relations only.

Model checking is a successful technique widely used in formal verification. Given a model of a system and a formula specifying a desired property of it, one can verify whether the system satisfies the property by checking the formula against the model. Distinctive features of model checking are: (i) it is a fully automatic process, (ii) it exaustively checks all the possible behaviours of the system, and (iii) it produces a counterexample, in case the property is violated. Systems are usually modeled as (finite) Kripke structures, that is, state-transition systems, and their properties are specified by formulas of point-based temporal logics, such as LTL, CTL, and the like. These logics allow one to express requirements on computation states and their relationships; however, they are not well suited to specify conditions on computation stretches, which come into play when dealing with, for instance, actions with duration, accomplishments, and temporal aggregations. To overcome the limitations of point-based logics, one can resort to interval temporal logics (ITLs), that assume time intervals,instead of time points, as their primitive entities. The most well-known ITL is Halpern and Shoham's modal logic of time intervals HS [4], which features one modality for each possible ordering relation between a pair of intervals, apart from equality. The satisfiability problem for HS has been studied in [4], and it turns out to be highly undecidable forall relevant (classes of) linear orders. The same holds for most fragments of it [2]; luckily, some meaningful exceptions exist, including the logic of temporal neighbourhood and the temporal logic of sub-intervals.

Model checking is commonly recognized as one of the most effective tool in system verification. While it has been systematically investigated in the context of classical, point-based temporal logics, it is still largely unexplored in the interval logic setting. Recently, a non-elementary model checking algorithm for Halpern and Shoham's modal logic of time intervals HS, interpreted over finite Kripke structures, has been proposed, together with a proof of the EXPSPACE-hardness of the problem. In this paper, we devise an EXPSPACE model checking procedure for two meaningful HS fragments. It exploits a suitable contraction technique, that allows one to replace long enough tracks of a Kripke structure by equivalent shorter ones.

Model checking has been successfully used in many computer science fields, including artificial intelligence, theoretical computer science, and databases. Most of the proposed solutions make use of classical, point-based temporal logics, while little work has been done in the interval temporal logic setting. Recently, a non-elementary model checking algorithm for Halpern and Shoham's modal logic of time intervals HS over finite Kripke structures (under the homogeneity assumption) and an EXPSPACE model checking procedure for two meaningful fragments of it have been proposed. In this paper, we show that more efficient model checking procedures can be developed for some expressive enough fragments of HS.

The chop operator C is a binary modality that plays an important role in interval temporal logics. Such an operator, which is not definable in Halpern and Shoham's modal logic of time intervals HS, allows one to split an interval into two parts and to specify what is true over them. C appears both in Moszkowski's PITL (that pairs it with a modal constant Pi which is true on all and only the intervals with coincident endpoints) and in Venema's CDT (that also features the binary modalities D and T, and Pi). Without the so-called locality principle, which restricts the semantics of proposition letters, the satisfiability problem for both PITL and CDT turns out to be undecidable over all meaningful classes of linear orders. The problem has been shown to be undecidable also for the fragment C, that is, PITL without Pi, over infinite linear orders. In this paper, we prove that the same holds for C over finite linear orders. To this end, we exploit the close relation between C and the reflexive version of the HS fragment BE, whose modalities correspond to Allen's relations starts and finishes: we prove that the satisfiability problem for reflexive BE is undecidable, undecidability of the same problem for C comes as a corollary.

Description logics of the DL-Lite family are widely used in knowledge representation because of their low computational complexity and rather good expressivity sufficient to capture important conceptual modelling constructs and the OWL2 QL profile of the Ontology Web Language (OWL). Recently, various point-based temporal extensions of DL-Lite have been investigated. Here, we propose to extend DL-Lite with fragments of Halpern and Shoham's interval logic of Allen's relations (ℋ𝒮). We formally define such extensions and show how they can be successfully used in knowledge representation. In the quest for a decidable logic, we discuss the challanges in combining decidable fragments of ℋ𝒮 with DL-Lite.

Model checking is a powerful method widely explored in formal verification. Given a model of a system, e.g. A Kripke structure, and a formula specifying its expected behavior, one can verify whether the system meets the behavior by checking the formula against the model. Classically, system behavior is given as a formula of a temporal logic, such as LTL and the like. These logics are "point-wise" interpreted, as they describe how the system evolves state-by-state. However, there are relevant properties, such as those involving temporal aggregations, which are inherently "interval-based", and thus asking for an interval temporal logic. In this paper, we give a formalization of the model checking problem in an interval logic setting. First, we provide an interpretation of formulas of Halpern and Shoham's interval temporal logic HS over Kripke structures, which allows one to check interval properties of computations. Then, we prove that the model checking problem for HS against Kripke structures is decidable by a suitable small model theorem, and we outline a PSpace decision procedure for the meaningful fragments AAbarBBbar and AAbarEEbar.

The propositional interval logic of temporal neighborhood (PNL for short) features two modalities that make it possible to access intervals adjacent to the right (modality xAy) and to the left (modality xAy) of the current interval. PNL stands at a central position in the realm of interval temporal logics, as it is expressive enough to encode meaningful temporal conditions and decidable (undecidability rules over interval temporal logics, while PNL is NEXPTIME-complete). Moreover, it is expressively complete with respect to FO2|<;|. Various extensions of PNL have been studied in the literature, including metric, hybrid, and first-order ones. Here, we study the effects of the addition of an equivalence relation ~ to Metric PNL (MPNL~). We first show that finite satisfiability for PNL extended with ~ is still NEXPTIME-complete. Then, we prove that finite satisfiability for MPNL~ can be reduced to the decidable 0-0 reach ability problem for vector addition systems and vice versa (EXPSPACE-hardness immediately follows).

Interval temporal logics provide a general framework for temporal representation and reasoning, where classical (point-based) linear temporal logics can be recovered as special cases. In this paper, we study the effects of the addition of an equivalence relation to one of the most representative interval temporal logics, namely, the logic ABB̅ of Allen's relations meets, begun by, and begins. We first prove that the satisfiability problem for the resulting logic ABB̅ ℕ remains decidable over finite linear orders, but it becomes nonprimitive recursive, while decidability is lost over N. We also show that decidability over can be recovered by restricting to a suitable subset of models. Then, we show that ABB̅ ℕ is expressive enough to define ωS-regular languages, thus establishing a promising connection between interval temporal logics and extended ω-regular languages.

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 propose a mapping from a database conceptual design to a schema for XML that produces highly connected and nested XML structures. We first introduce two alternative definitions of the mapping, one modeling entities as global XML elements and expressing relationships among them in terms of keys and key references (flat design), the other one encoding relationships by properly including the elements for some entities into the elements for other entities (nest design). Then we provide a benchmark evaluation of the two solutions showing that the nest approach, compared to the flat one, leads to improvements in both query and validation performances. This motivates us to systematically investigate the best way to nest XML structures. We identify two different nesting solutions: a maximum depth nesting, that keeps low the number of costly join operations that are necessary to reconstruct information at query time using the mapped schema, and a maximum density nesting, that minimizes the number of schema constraints used in the mapping of the conceptual schema, thus reducing the validation overhead. On the one hand, the problem of finding a maximum depth nesting turns out to be NP-complete and, moreover, it admits no constant ratio approximation algorithm. On the other hand, we devise a graph-theoretic algorithm, NiduX, that solves the maximum density problem in linear time. Interestingly, NiduX finds the optimal solution for the harder maximum depth problem whenever the conceptual design graph is either acyclic or complete. In randomly generated intermediate cases of the graph topology, we experimentally show that NiduX finds a good approximation of the optimal solution.

The propositional logic of temporal neighborhood (PNL) features two modalities that make it possible to access intervals adjacent to the right and to the left of the current one. PNL has been extensively studied in the last years. In particular, decidability and complexity of its satisfiability problem have been systematically investigated, and optimal decision procedures have been developed, for various (classes of) linear orders, including N, Z, and Q. The only missing piece is that for R. It is possible to show that PNL is expressive enough to separate Q and R. Unfortunately, there is no way to reduce the satisfiability problem for PNL over R to that over Q. In this paper, we first prove the NEXPTIME-completeness of the satisfiability problem for PNL over R, and then we devise an optimal tableau system for it.

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.

The introduction of Halpern and Shoham's modal logic of intervals (later on called HS) dates back to 1986. Despite its natural semantics, this logic is undecidable over all interesting classes of temporal structures. This discouraged research in this area until recently, when a number of non trivial decidable fragments have been found. This paper is a contribution toward the complete classification of HS fragments. Different combinations of Allen's interval relations begins (B), meets (A), and later (L), and their inverses A̅, B̅, and L̅, have been considered in the literature. We know from previous work that the combination ABB̅A̅ is decidable over finite linear orders and undecidable everywhere else. We extend these results by showing that ABB̅L̅ is decidable over the class of all (resp., dense, discrete) linear orders, and that it is maximal with respect to decidability over these classes: adding any other interval modality immediately leads to undecidability.

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.

In this paper, we focus our attention on the interval temporal logic of the Allen's relations ``meets'', ``begins'', and ``begun by'' ($\ABB$ for short), interpreted over natural numbers. We first introduce the logic and we show that it is expressive enough to model distinctive interval properties, such as accomplishment conditions, to capture basic modalities of point-based temporal logic, such as the until operator, and to encode relevant metric constraints. Then, we prove that the satisfiability problem for $\ABB$ over natural numbers is decidable by providing a small model theorem based on an original contraction method. Finally, we prove the EXPSPACE-completeness of the problem.

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.

An interval temporal logic is a propositional, multi-modal logic interpreted over interval structures of partial orders. The semantics of each modal operator are given in the standard way with respect to one of the natural accessibility relations defined on such interval structures. In this paper, we consider the modal operators based on the (reflexive) sub-interval relation and the (reflexive) super-interval relation. We show that the satisfiability problems for the interval temporal logics featuring either or both of these modalities, interpreted over interval structures of finite linear orders, are all PSPACE-complete. These results fill a gap in the known complexity results for interval temporal logics.

Product configuration systems are an emerging software technology that supports companies in deploying mass customization strategies. In this paper, we describe a CLP-based reasoning engine that we developed for a commercial configuration system. We

In this article, we develop tableau-based decision procedures for the logics of subinterval structures over dense linear orderings. In particular, we consider the two difficult cases: the relation of strict subintervals (with both endpoints strictly inside the current interval) and the relation of proper subintervals (that can share one endpoint with the current interval). For each of these logics, we establish a small pseudo-model property and construct a sound, complete and terminating tableau that searches systematically for existence of such a pseudo-model satisfying the input formulas. Both constructions are non-trivial, but the latter is substantially more complicated because of the presence of beginning and ending subintervals which require special treatment. We prove PSPACE completeness for both procedures and implement them in the generic tableau-based theorem prover Lotrec.

Interval temporal logics are based on interval structures over linearly (or partially) ordered domains, where time intervals, rather than time instants, are the primitive ontological entities. In this paper we introduce and study Right Propositional Neighborhood Logic over natural numbers with integer constraints for interval lengths, which is a propositional interval temporal logic featuring a modality for the 'right neighborhood' relation between intervals and explicit integer constraints for interval lengths. We prove that it has the bounded model property with respect to ultimately periodic models and is therefore decidable. In addition, we provide an EXP SPACE procedure for satisfiability checking and we prove EXPSPACE-hardness by a reduction from the exponential corridor tiling problem.

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.

Dealing with multiple representations of the same spatial data is widely recognized as a relevant problem in conceptual modeling of spatial information. Unfortunately, existing solutions provide no support to the management of consistency constraints on multiple representations. In this paper, we propose an extension to the ChronoGeoGraph (CGG) conceptual model, which features both a relation of spatial aggregation, that allows one to switch from a spatial entity to its components, and vice versa, and a relation of carto-graphic generalization, that allows one to maintain multiple spatial representations that may differ in resolution, shape, or point of view. A special attention is deserved to the problem of guaranteeing the topological consistency of different representations of the same spatial entity. A short description of the relational encoding of the constructs for multiple representations added to CGG concludes the paper.

Propositional interval temporal logics come into play in many areas of artificial intelligence and computer science. Unfortunately, most of them turned out to be (highly) undecidable. Some positive exceptions, belonging to the classes of neighborhood logics and of logics of subinterval relations, have been recently identified. In this paper, we address the decision problem for the future fragment of Propositional Neighborhood Logic (Right Propositional Neighborhood Logic) interpreted over trees and we positively solve it by providing a tableau-based decision procedure that works in exponential space. Moreover, we prove that the decision problem for the logic is EXPSPACE-hard, thus showing the optimality of the proposed procedure.

Time characterizes every aspect of our life and its management when storing and querying data is very important. In this paper we propose a new temporal query language, called T4SQL, supporting multiple temporal dimensions of data. Besides the well-known valid and transaction times, it encompasses two additional temporal dimensions, namely, availability and event times. The availability time records when information is known and treated as true by the information system; the event times record the occurrence times of both the event that starts the valid time and the event that ends it. T4SQL is capable to deal with different temporal semantics (atemporal aka non-sequenced, current, sequenced, next) with respect to every temporal dimension. Moreover, T4SQL provides a novel temporal grouping clause and an orthogonal management of temporal properties when defining the selection condition(s) and the schema for the output relation.

In this paper we generalize the contraction method, originally proposed by Elgot and Rabin and later extended by Carton and Thomas, from labeled linear orderings to colored deterministic trees. The method we propose rests on a suitable notion of indistinguishability of trees with respect to tree automata that allows us to reduce a number of instances of the acceptance problem for tree automata to decidable instances involving regular trees. We prove that such a method works effectively for a large class of trees, which is closed under noticeable operations and includes all the deterministic trees of the Caucal hierarchy obtained via unfoldings and inverse finite mappings as well as several trees outside such a hierarchy.

A time granularity can be viewed as the partitioning of a temporal domain in groups of elements, where each group is perceived as an indivisible unit. In this paper we explore an automaton-based approach to the management of time granularity that compactly represents time granularities as single-string automata with counters, that is, Buchi automata, extended with counters, that accept a single infinite word. We focus our attention on the equivalence problem for the class of restricted labeled single-string automata (RLA for short). The equivalence problem for RLA is the problem of establishing whether two given RLA represent the same time granularity. The main contribution of the paper is the reduction of the (non-)equivalence problem for RLA to the satisfiability problem for linear diophantine equations with bounds on variables. Since the latter problem has been shown to be NP-complete, we have that the RLA equivalence problem is in co-NP.

Nowadays, the ability of providing an automated support to the management of business processes is commonly recognized as a main competitive factor for companies. One of the most critical resources to deal with is time, but, unfortunately, the time management support offered by most workflow systems is rather limited. In this paper we focus our attention on the modeling and verification of workflows extended with time constraints. We propose timed automata as an effective tool to specify timed workflow schemas and to check their consistency.

In the database literature, different types of temporal functional dependencies (TFDs) have been proposed to constrain the temporal evolution of information. Unfortunately, the lack of a common notation makes it difficult to compare, to integrate, and to possibly extend the various proposals. In this paper, we outline a unifying algebraic framework for TFDs. We first introduce the proposed approach, then we use it to give a uniform account of existing TFDs, and finally we show that it allows one to easily express new meaningful TFDs.

In this paper we focus our attention on the problem of finding propositional interval temporal logics which are expressive enough to express meaningful statements about time intervals and decidable.

In this paper, we address the decision problem for a system of monadic second-order logic interpreted over an /spl omega/-layered temporal structure devoid of both a finest layer and a coarsest one (we call such a structure totally unbounded). We propose an automaton-theoretic method that solves the problem in two steps: first, we reduce the considered problem to the problem of determining, for any given Rabin tree automaton, whether it accepts a fixed vertex-colored tree; then, we exploit a suitable notion of tree equivalence to reduce the latter problem to the decidable case of regular trees.

The ability of providing and relating temporal representations at different ‘grain levels’ of the same reality is an important research theme in computer science and a major requirement for many applications, including formal specification and verification, temporal databases, data mining, problem solving, and natural language understanding. In particular, the addition of a granularity dimension to a temporal logic makes it possible to specify in a concise way reactive systems whose behaviour can be naturally modeled with respect to a (possibly infinite) set of differently-grained temporal domains. Suitable extensions of the monadic second-order theory of $k$ successors have been proposed in the literature to capture the notion of time granularity. In this paper, we provide the monadic second-order theories of downward unbounded layered structures, which are infinitely refinable structures consisting of a coarsest domain and an infinite number of finer and finer domains, and of upward unbounded layered structures, which consist of a finest domain and an infinite number of coarser and coarser domains, with expressively complete and elementarily decidable temporal logic counterparts. We obtain such a result in two steps. First, we define a new class of combined automata, called temporalized automata, which can be proved to be the automata-theoretic counterpart of temporalized logics, and show that relevant properties, such as closure under Boolean operations, decidability, and expressive equivalence with respect to temporal logics, transfer from component automata to temporalized ones. Then, we exploit the correspondence between temporalized logics and automata to reduce the task of finding the temporal logic counterparts of the given theories of time granularity to the easier one of finding temporalized automata counterparts of them.

In this paper, we study the definability and decidability of binary predicates for time granularity with respect to monadic theories over finitely and infinitely layered structures. We focus our attention on the equi-level (resp. equi-column) predicate constraining two time points to belong to the same layer (resp. column) and on the horizontal (resp. vertical) successor predicate relating a time point to its successor within a given layer (resp. column). We give a number of positive and negative results by reduction to/from a wide spectrum of decidable/undecidable problems.

In this paper, a generalization of Kamp's theorem relative to the functional completeness of the until operator is proved. Such a generalization consists in showing the functional completeness of more expressive temporal operators with respect to the extension of the first‐order theory of linear orders MFO[<] with an extra binary relational symbol. The result is motivated by the search of a modal language capable of expressing properties and operators suitable to model time granularity in ω‐layered temporal structures.

Kowalski and Sergot's Event Calculus (EC) is a simple temporal formalism that, given a set of event occurrences, derives the maximal validity intervals (MVIs) over which properties initiated or terminated by these events hold. In this paper, we conduct a systematic analysis of EC by which we gain a better understanding of this formalism and determine ways of augmenting its expressive power. The keystone of this endeavor is the definition of an extendible formal specification of its functionalities. This formalization has the effects of casting determination of MVIs as a model checking problem, of setting the ground for studying and comparing the expressiveness and complexity of various extensions of EC, and of establishing a semantic reference against which to verify the soundness and completeness of implementations. We extend the range of queries accepted by EC, which is limited to Boolean combinations of MVI verification or computation requests, to support arbitrary quantification over events and modal queries. We also admit specifications based on preconditions. We demonstrate the added expressive power by encoding a number of diagnosis problems. Moreover, we provide a systematic comparison of the expressiveness and complexity of the various extended event calculi against each other. Finally, we propose a declarative encoding of these enriched event calculi in the logic programming language λProlog and prove the soundness and completeness of the resulting logic programs.

We investigate modal deduction through translation into standard logic and set theory. In a previous paper, using a set-theoretic translation method, we proved that derivability in the minimal modal logic K, corresponds precisely to derivability in a weak, computationally attractive set theory ω In this paper, this approach is shown equivalent to working with standard first-order translations of modal formulae in a theory of general frames. The employed techniques are mainly model-theoretic and set-theoretic, and they admit extensions to richer languages and modal deductive systems than that of basic modal logic. Some of these extensions are discussed in the last part of the paper.

This article deals with the problem of providing Kowalski and Sergot's event calculus, extended with context dependency, with an efficient implementation in a logic programming framework. Despite a widespread recognition that a positive solution to efficiency issues is necessary to guarantee the computational feasibility of existing approaches to temporal reasoning, the problem of analyzing the complexity of temporal reasoning programs has been largely overlooked. This article provides a mathematical analysis of the efficiency of query and update processing in the event calculus and defines a cached version of the calculus that (i) moves computational complexity from query to update processing and (ii) features an absolute improvement of performance, because query processing in the event calculus costs much more than update processing in the proposed cached version.