Arrow Research search

Author name cluster

Pietro Sala

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

42 papers
2 author rows

Possible papers

42

I&C Journal 2024 Journal Article

Predictive mining of multi-temporal relations

  • Beatrice Amico
  • Carlo Combi
  • Romeo Rizzi
  • Pietro Sala

In this paper, we propose a methodology for deriving a new kind of approximate temporal functional dependencies, called Approximate Predictive Functional Dependencies (APFDs), based on a three-window framework and on a multi-temporal relational model. Different features are proposed for the Observation Window (OW), where we observe predictive data, for the Waiting Window (WW), and for the Prediction Window (PW), where the predicted event occurs. We then consider the concept of approximation for such APFDs, introduce new error measures, and discuss different strategies for deriving APFDs. We discuss the quality, i. e. , the informative content, of the derived AFDs by considering their entropy and information gain. Moreover, we outline the results in deriving APFDs focusing on the Acute Kidney Injury (AKI). We use real clinical data contained in the MIMIC III dataset related to patients from Intensive Care Units to show the applicability of our approach to real-world data.

Details DOI

GandALF Workshop 2024 Workshop Paper

Reactive Synthesis for Expected Impacts

  • Emanuele Chini
  • Pietro Sala
  • Andrea Simonetti
  • Omid Zare

As business processes become increasingly complex, effectively modeling decision points, their likelihood, and resource consumption is crucial for optimizing operations. To address this challenge, this paper introduces a formal extension of the Business Process Model and Notation (BPMN) that incorporates choices, probabilities, and impacts, referred to as BPMN+CPI. This extension is motivated by the growing emphasis on precise control within business process management, where carefully selecting decision pathways in repeated instances is crucial for conforming to certain standards of multiple resource consumption and environmental impacts. In this context we deal with the problem of synthesizing a strategy (if any) that guarantees that the expected impacts on repeated execution of the input process are below a given threshold. We show that this problem belongs to PSPACE complexity class; moreover we provide an effective procedure for computing a strategy (if present).

PDF Details DOI

GandALF Workshop 2024 Workshop Paper

Synthesis of Timeline-Based Planning Strategies Avoiding Determinization

  • Renato Acampora
  • Dario Della Monica
  • Luca Geatti
  • Nicola Gigante
  • Angelo Montanari
  • Pietro Sala

Qualitative timeline-based planning models domains as sets of independent, but interacting, components whose behaviors over time, the timelines, are governed by sets of qualitative temporal constraints (ordering relations), called synchronization rules. Its plan-existence problem has been shown to be PSPACE-complete; in particular, PSPACE-membership has been proved via reduction to the nonemptiness problem for nondeterministic finite automata. However, nondeterministic automata cannot be directly used to synthesize planning strategies as a costly determinization step is needed. In this paper, we identify a large fragment of qualitative timeline-based planning whose plan-existence problem can be directly mapped into the nonemptiness problem of deterministic finite automata, which can then be exploited to synthesize strategies. In addition, we identify a maximal subset of Allen's relations that fits into such a deterministic fragment.

PDF Details DOI

TCS Journal 2023 Journal Article

An interval temporal logic characterization of extended ω-regular languages

  • Dario Della Monica
  • Angelo Montanari
  • Pietro Sala

Some extensions of ω-regular languages have been proposed in the literature to express asymptotic properties of ω-words which are not captured by ω-regular languages. They include ωB-regular languages, that extend ω-regular languages with boundedness, ωS-regular languages, that enrich ω-regular ones with strong unboundedness, ωBS-regular languages, that combine ωB- and ωS-regular ones, and ωT-regular languages, that include meaningful languages which are not ωBS-regular. Formal definitions of extended ω-regular languages have been given in terms of both suitable classes of automata and extended ω-regular expressions, while satisfactory temporal logic counterparts are still missing. In this paper, we give a characterization of them in terms of interval temporal logics by providing an explicit encoding of expressions into formulas.

Details DOI

TIME Conference 2023 Conference Paper

Discovering Predictive Dependencies on Multi-Temporal Relations

  • Beatrice Amico
  • Carlo Combi
  • Romeo Rizzi
  • Pietro Sala

In this paper, we propose a methodology for deriving a new kind of approximate temporal functional dependencies, called Approximate Predictive Functional Dependencies (APFDs), based on a three-window framework and on a multi-temporal relational model. Different features are proposed for the Observation Window (OW), where we observe predictive data, for the Waiting Window (WW), and for the Prediction Window (PW), where the predicted event occurs. We then discuss the concept of approximation for such APFDs, introduce two new error measures. We prove that the problem of deriving APFDs is intractable. Moreover, we discuss some preliminary results in deriving APFDs from real clinical data using MIMIC III dataset, related to patients from Intensive Care Units.

Details

I&C Journal 2023 Journal Article

Pspace-completeness of the temporal logic of sub-intervals and suffixes

  • Laura Bozzelli
  • Angelo Montanari
  • Adriano Peron
  • Pietro Sala

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 〈 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 〉 ).

Details DOI

TCS Journal 2022 Journal Article

Reactive synthesis from interval temporal logic specifications

  • Angelo Montanari
  • Pietro Sala

In this paper, we deal with the synthesis problem for Halpern and Shoham's interval temporal logic HS extended with an equivalence relation ∼ over time points (HS Image 1 for short). The definition of the problem is analogous to that for M S O ( ω, < ). Given an HS Image 1 formula φ and a finite set Σ φ ⋄ of proposition letters and temporal requests, it consists of determining, whether or not, for all possible valuations of elements in Σ φ ⋄ in every interval structure, there is a valuation of the remaining proposition letters and temporal requests such that the resulting structure is a model for φ. We focus on the decidability and complexity of the problem for some meaningful fragments of HS Image 1, whose modalities are drawn from the set { A ( m e e t s ), A ¯ ( m e t b y ), B ( b e g u n b y ), B ¯ ( b e g i n s ) } interpreted over finite linear orders and N. We prove that, over finite linear orders, the problem is decidable (Ackermann-hard) for Image 2 and undecidable for A A ¯ B B ¯. Moreover, we show that if we replace finite linear orders by N, then it becomes undecidable even for AB B ¯. Finally, we study the generalization of Image 2 to Image 3, where k is the number of distinct equivalence relations. Despite the fact that the satisfiability problem for Image 3, with k > 1, over finite linear orders, is already undecidable, we prove that, under a natural semantic restriction (refinement condition), the synthesis problem turns out to be decidable.

Details DOI

GandALF Workshop 2021 Workshop Paper

Adding the Relation Meets to the Temporal Logic of Prefixes and Infixes makes it EXPSPACE-Complete

  • Laura Bozzelli
  • Angelo Montanari
  • Adriano Peron
  • Pietro Sala

The choice of the right trade-off between expressiveness and complexity is the main issue in interval temporal logic. In their seminal paper, Halpern and Shoham showed that the satisfiability problem for HS (the temporal logic of Allen's relations) is highly undecidable over any reasonable class of linear orders. In order to recover decidability, one can restrict the set of temporal modalities and/or the class of models. In the following, we focus on the satisfiability problem for HS fragments under the homogeneity assumption, according to which any proposition letter holds over an interval if only if it holds at all its points. The problem for full HS with homogeneity has been shown to be non-elementarily decidable, but its only known lower bound is EXPSPACE (in fact, EXPSPACE-hardness has been shown for the logic of prefixes and suffixes BE, which is a very small fragment of it. The logic of prefixes and infixes BD has been recently shown to be PSPACE-complete. In this paper, we prove that the addition of the Allen relation Meets to BD makes it EXPSPACE-complete.

PDF Details DOI

TIME Conference 2021 Conference Paper

Pspace-Completeness of the Temporal Logic of Sub-Intervals and Suffixes

  • Laura Bozzelli
  • Angelo Montanari
  • Adriano Peron
  • Pietro Sala

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⟩).

Details

AIIM Journal 2021 Journal Article

TEDAR: Temporal dynamic signal detection of adverse reactions

  • Antonino Aparo
  • Pietro Sala
  • Vincenzo Bonnici
  • Rosalba Giugno

Computational approaches to detect the signals of adverse drug reactions are powerful tools to monitor the unattended effects that users experience and report, also preventing death and serious injury. They apply statistical indices to affirm the validity of adverse reactions reported by users. The methodologies that scan fixed duration intervals in the lifetime of drugs are among the most used. Here we present a method, called TEDAR, in which ranges of varying length are taken into account. TEDAR has the advantage to detect a greater number of true signals without significantly increasing the number of false positives, which are a major concern for this type of tools. Furthermore, early detection of signals is a key feature of methods to prevent the safety of the population. The results show that TEDAR detects adverse reactions many months earlier than methodologies based on a fixed interval length.

Details DOI

TCS Journal 2020 Journal Article

Beyond ω-regular languages: ωT-regular expressions and their automata and logic counterparts

  • David Barozzini
  • David de Frutos-Escrig
  • Dario Della Monica
  • Angelo Montanari
  • Pietro Sala

In the last years, some extensions of ω-regular languages, namely, ωB-regular (ω-regular languages extended with boundedness), ωS-regular (ω-regular languages extended with strong unboundedness), and ωBS-regular languages (the combination of ωB- and ωS-regular ones), have been proposed in the literature. While the first two classes satisfy a generalized closure property, which states that the complement of an ωB-regular (resp. , ωS-regular) language is an ωS-regular (resp. , ωB-regular) one, the last class is not closed under complementation. The existence of non-ωBS-regular languages that are the complements of some ωBS-regular ones and express fairly natural asymptotic behaviors motivates the search for other significant classes of extended ω-regular languages. In this paper, we present the class of ωT-regular languages, which includes meaningful languages that are not ωBS-regular. We define this new class of languages in terms of ωT-regular expressions. Then, we introduce a new class of automata (counter-check automata) and we prove that (i) their emptiness problem is decidable in PTIME, and (ii) they are expressive enough to capture ωT-regular languages. We also provide an encoding of ωT-regular expressions into S1S+U. Finally, we investigate a stronger variant of ωT-regular languages ( ω T s -regular languages). We characterize the resulting class of languages in terms of ω T s -regular expressions, and we show how to map it into a suitable class of automata, called counter-queue automata. We conclude the paper with a comparison of the expressiveness of ωT- and ω T s -regular languages and of the corresponding automata.

Details DOI

MFCS Conference 2020 Conference Paper

On a Temporal Logic of Prefixes and Infixes

  • Laura Bozzelli
  • Angelo Montanari
  • Adriano Peron
  • Pietro Sala

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.

Details

TIME Conference 2019 Conference Paper

Customizing BPMN Diagrams Using Timelines

  • Carlo Combi
  • Barbara Oliboni
  • Pietro Sala

BPMN (Business Process Model and Notation) is widely used standard modeling technique for representing Business Processes by using diagrams, but lacks in some aspects. Representing execution-dependent and time-dependent decisions in BPMN Diagrams may be a daunting challenge [Carlo Combi et al. , 2017]. In many cases such constraints are omitted in order to preserve the simplicity and the readability of the process model. However, for purposes such as compliance checking, process mining, and verification, formalizing such constraints could be very useful. In this paper, we propose a novel approach for annotating BPMN Diagrams with Temporal Synchronization Rules borrowed from the timeline-based planning field. We discuss the expressivity of the proposed approach and show that it is able to capture a lot of complex temporally-related constraints without affecting the structure of BPMN diagrams. Finally, we provide a mapping from annotated BPMN diagrams to timeline-based planning problems that allows one to take advantage of the last twenty years of theoretical and practical developments in the field.

Details

AIJ Journal 2019 Journal Article

On coarser interval temporal logics

  • Emilio Muñoz-Velasco
  • Mercedes Pelegrín
  • Pietro Sala
  • Guido Sciavicco
  • Ionel Eduard Stan

The primary characteristic of interval temporal logic is that intervals, rather than points, are taken as the primitive ontological entities. Given their generally bad computational behavior of interval temporal logics, several techniques exist to produce decidable and computationally affordable temporal logics based on intervals. In this paper we take inspiration from Golumbic and Shamir's coarser interval algebras, which generalize the classical Allen's Interval Algebra, in order to define two previously unknown variants of Halpern and Shoham's logic (HS) based on coarser relations. We prove that, perhaps surprisingly, the satisfiability problem for the coarsest of the two variants, namely HS 3, not only is decidable, but PSpace-complete in the finite/discrete case, and PSpace-hard in any other case; besides proving its complexity bounds, we implement a tableau-based satisfiability checker for it and test it against a systematically generated benchmark. Our results are strengthened by showing that not all coarser-than-Allen's relations are a guarantee of decidability, as we prove that the second variant, namely HS 7, remains undecidable in all interesting cases.

Details DOI

TCS Journal 2019 Journal Article

Which fragments of the interval temporal logic HS are tractable in model checking?

  • Laura Bozzelli
  • Alberto Molinari
  • Angelo Montanari
  • Adriano Peron
  • Pietro Sala

Since the 80s, model checking (MC) has been applied to the automatic verification of hardware/software systems. Point-based temporal logics, such as LTL, CTL, CTL ⁎, and the like, are commonly used in MC as the specification language; however, there are some inherently interval-based properties of computations, e. g. , temporal aggregations and durations, that cannot be properly dealt with by these logics, as they model a state-by-state evolution of systems. Recently, an MC framework for the verification of interval-based properties of computations, based on Halpern and Shoham's interval temporal logic ( HS, for short) and its fragments, has been proposed and systematically investigated. In this paper, we focus on the boundaries that separate tractable and intractable HS fragments in MC. We first prove that MC for the logic BE of Allen's relations started-by and finished-by is provably intractable, being Expspace-hard. Such a lower bound immediately propagates to full HS. Then, in contrast, we show that other noteworthy HS fragments, i. e. , the logic A A ‾ B B ‾ (resp. , A A ‾ E E ‾ ) of Allen's relations meets, met-by, starts (resp. , finishes), and started-by (resp. , finished-by), are well-behaved, and turn out to have the same complexity as LTL (Pspace-complete). Halfway are the fragments A A ‾ B B ‾ E ‾ and A A ‾ E B ‾ E ‾, whose Expspace membership and Pspace hardness are already known. Here, we give an original proof of Expspace membership, that substantially simplifies the complexity of the constructions previously used for such a result. Contraction techniques—suitably tailored to each HS fragment—are at the heart of our results, enabling us to prove a pair of remarkable small-model properties.

Details DOI

KR Conference 2018 Conference Paper

A novel automata-theoretic approach to timeline-based planning

  • Dario Della Monica
  • Nicola Gigante
  • Angelo Montanari
  • Pietro Sala

Timeline-based planning is a well-established approach successfully employed in a number of application domains. A very restricted fragment, featuring only bounded temporal relations and token durations, is expressive enough to capture action-based temporal planning. As for computational complexity, it has been shown to be EXPSPACE-complete when unbounded temporal relations, but only bounded token durations, are allowed. In this paper, we present a novel automata-theoretic characterisation of timeline-based planning where the existence of a plan is shown to be equivalent to the nonemptiness of the language recognised by a nondeterministic finite-state automaton that suitably encodes all the problem constraints (timelines and synchronisation rules). Besides allowing us to restate known complexity results in a fairly natural and compact way, such an alternative characterisation makes it possible to finally establish the exact complexity of the full version of the problem with unbounded temporal relations and token durations, which was still open and turns out to be EXPSPACE-complete. Moreover, the proposed technique is general enough to cope with (infinite) recurrent goals, which received little attention so far, despite being quite common in real-word application scenarios.

I&C Journal 2018 Journal Article

Model checking for fragments of the interval temporal logic HS at the low levels of the polynomial time hierarchy

  • Laura Bozzelli
  • Alberto Molinari
  • Angelo Montanari
  • Adriano Peron
  • Pietro Sala

Some temporal properties of reactive systems, such as actions with duration and temporal aggregations, which are inherently interval-based, can not be properly expressed by the standard, point-based temporal logics LTL, CTL and CTL⁎, as they give a state-by-state account of system evolution. Conversely, interval temporal logics—which feature intervals, instead of points, as their primitive entities—naturally express them. We study the model checking (MC) problem for Halpern and Shoham's modal logic of time intervals (HS), interpreted on Kripke structures, under the homogeneity assumption. HS is the best known interval-based temporal logic, which has one modality for each of the 13 ordering relations between pairs of intervals (Allen's relations), apart from equality. We focus on MC for some HS fragments featuring modalities for (a subset of) Allen's relations meet, met-by, started-by, and finished-by, showing that it is in P NP. Additionally, we provide some complexity lower bounds to the problem.

Details DOI

GandALF Workshop 2017 Workshop Paper

Beyond ωBS-regular Languages: ωT-regular Expressions and Counter-Check Automata

  • Dario Della Monica
  • Angelo Montanari
  • Pietro Sala

In the last years, various extensions of ω-regular languages have been proposed in the literature, including ωB-regular (ω-regular languages extended with boundedness), ωS-regular (ω-regular languages extended with strict unboundedness), and ωBS-regular languages (the combination of ωB- and ωS-regular ones). While the first two classes satisfy a generalized closure property, namely, the complement of an ωB-regular (resp. , ωS-regular) language is an ωS-regular (resp. , ωB-regular) one, the last class is not closed under complementation. The existence of non-ωBS-regular languages that are the complements of some ωBS-regular ones and express fairly natural properties of reactive systems motivates the search for other well-behaved classes of extended ω-regular languages. In this paper, we introduce the class of ωT-regular languages, that includes meaningful languages which are not ωBS-regular. We first define it in terms of ωT-regular expressions. Then, we introduce a new class of automata (counter-check automata) and we prove that (i) their emptiness problem is decidable in PTIME and (ii) they are expressive enough to capture ωT-regular languages (whether or not ωT-regular languages are expressively complete with respect to counter-check automata is still an open problem). Finally, we provide an encoding of ωT-regular expressions into S1S+U.

PDF Details DOI

IJCAI Conference 2017 Conference Paper

Bounded Timed Propositional Temporal Logic with Past Captures Timeline-based Planning with Bounded Constraints

  • Dario Della Monica
  • Nicola Gigante
  • Angelo Montanari
  • Pietro Sala
  • Guido Sciavicco

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.

PDF Details

TCS Journal 2016 Journal Article

Adding one or more equivalence relations to the interval temporal logic AB B ¯

  • Angelo Montanari
  • Marco Pazzaglia
  • Pietro Sala

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 one or more equivalence relations to one of the most representative interval temporal logics, namely, the logic AB B ¯ of Allen's relations meets, begun by, and begins. We first prove that the satisfiability problem for the extension of AB B ¯ with one equivalence relation remains decidable over finite linear orders, but it becomes nonprimitive recursive. Then, we show that decidability is lost over N. Finally, we show that the addition of two or more equivalence relations makes finite satisfiability for the resulting logic undecidable. 1

Details DOI

GandALF Workshop 2016 Workshop Paper

Model Checking the Logic of Allen's Relations Meets and Started-by is P^NP-Complete

  • Laura Bozzelli
  • Alberto Molinari
  • Angelo Montanari
  • Adriano Peron
  • Pietro Sala

In the plethora of fragments of Halpern and Shoham's modal logic of time intervals (HS), the logic AB of Allen's relations Meets and Started-by is at a central position. Statements that may be true at certain intervals, but at no sub-interval of them, such as accomplishments, as well as metric constraints about the length of intervals, that force, for instance, an interval to be at least (resp. , at most, exactly) k points long, can be expressed in AB. Moreover, over the linear order of the natural numbers N, it subsumes the (point-based) logic LTL, as it can easily encode the next and until modalities. Finally, it is expressive enough to capture the ω-regular languages, that is, for each ω-regular expression R there exists an AB formula Φ such that the language defined by R coincides with the set of models of Φ over N. It has been shown that the satisfiability problem for AB over N is EXPSPACE-complete. Here we prove that, under the homogeneity assumption, its model checking problem is Δ^p_2 = P^NP-complete (for the sake of comparison, the model checking problem for full HS is EXPSPACE-hard, and the only known decision procedure is nonelementary). Moreover, we show that the modality for the Allen relation Met-by can be added to AB at no extra cost (AA'B is P^NP-complete as well).

PDF Details DOI

KR Conference 2016 Conference Paper

Model checking well-behaved fragments of HS: the (almost) final picture

  • Alberto Molinari
  • Angelo Montanari
  • Adriano Peron
  • Pietro Sala

Model checking is one of the most powerful and widespread tools for system verification with applications in many areas of computer science and artificial intelligence. The large majority of model checkers deal with properties expressed in point-based temporal logics, such as LTL and CTL. However, there exist relevant properties of systems which are inherently interval-based. Model checking algorithms for interval temporal logics (ITLs) have recently been proposed to check interval properties of computations. As the model checking problem for full Halpern and Shoham’s ITL (HS for short) turns out to be decidable, but computationally heavy, research has focused on its well-behaved fragments. In this paper, we provide an almost final picture of the computational complexity of model checking for HS fragments with modalities for (a subset of) Allen’s relations meets, met by, starts, and ends.

JELIA Conference 2016 Conference Paper

Prompt Interval Temporal Logic

  • Dario Della Monica
  • Angelo Montanari
  • Aniello Murano
  • Pietro Sala

Abstract Interval temporal logics are expressive formalisms for temporal representation and reasoning, which use time intervals as primitive temporal entities. They have been extensively studied for the past two decades and successfully applied in AI and computer science. Unfortunately, they lack the ability of expressing promptness conditions, as it happens with the commonly-used temporal logics, e. g. , LTL: whenever we deal with a liveness request, such as “something good eventually happens”, there is no way to impose a bound on the delay with which it is fulfilled. In the last years, such an issue has been addressed in automata theory, game theory, and temporal logic. In this paper, we approach it in the interval temporal logic setting. First, we introduce PROMPT- PNL, a prompt extension of the well-studied interval temporal logic PNL, and we prove the undecidability of its satisfiability problem; then, we show how to recover decidability (NEXPTIME-completeness) by imposing a natural syntactic restriction on it.

Details

TIME Conference 2015 Conference Paper

The Price of Evolution in Temporal Databases

  • Carlo Combi
  • Romeo Rizzi
  • Pietro Sala

Temporal Functional Dependencies (TFDs for short) are functional dependencies that predicate on temporal databases characterized by a special temporal dimension called valid time (VT). In [1] Combi et al. proposed a uniform framework that subsumes many of the TFDs proposed in literature and, by the combination of them, allow us to express finer constraints. Some interesting constraints are the Temporally Mixed Functional Dependencies (TMFD for short) that allow one to write constraints on the evolution of the data in the database. The problem of checking a TMFD against an instance of a temporal schema is polynomial. We will show that when approximation comes into play (i. e. , we look for TMFD holding for almost all database tuples) the problem turns out to be NP-Complete. Moreover we introduce a type of association rules build over TMFD called Temporally Mixed Association Rule (TMAR). We prove that verifying TMAR under approximation is still NP-Complete, by reducing it to a novel problem on directed acyclic graphs.

Details

TIME Conference 2014 Conference Paper

Approximate Interval-Based Temporal Dependencies: The Complexity Landscape

  • Pietro Sala

Temporal functional dependencies (TFDs) add valid time to classical functional dependencies (FDs) in order to express data integrity constraints over the flow of time. If the temporal dimension adopted is an interval, we have to deal with interval-based temporal functional dependencies (ITFDs for short), which consider different interval relations between valid times of related tuples. The related approximate problem is when we want to check if our data satisfy, without any constraint for the schema, a given ITFD under a given error threshold 0 ≤ d ≤ 1. This can be rephrased as: given a relation instance r, is it possible to delete at most c · |r| tuples from it in such a way that the resulting instance satisfies the given ITFD? This optimization problem, ITFD-Approx for short, may represent a way to discover (data mining) important dependencies among attribute values in a database as well as a way to control data consistency. In this paper we analyze the complexity of problem ITFD-Approx restricting ourselves to Allen's interval relations: we will see how the complexity of such a problem may significantly change, depending on the considered interval relation.

Details

Highlights Conference 2014 Conference Abstract

Decidability of the Interval Temporal Logic AA̅BB̅ over the Rationals

  • Pietro Sala

The classification of the fragments of Halpern and Shoham's logic with respect to decidability/undecidability of the satisfiability problem is now very close to the end. We settle one of the few remaining questions concerning the fragment AA̅BB̅, which comprises the Allen's interval relations meets and begins and their symmetric versions. We already proved that AA̅BB̅ is decidable over the class of all finite linear orders and undecidable over ordered domains isomorphic to ℕ. In this paper, we first show that AABB is undecidable over ℝ and over the class of all Dedekind-complete linear orders. We then prove that the logic is decidable over ℚ and over the class of all linear orders.

PDF Details

TCS Journal 2014 Journal Article

Interval temporal logics over strongly discrete linear orders: Expressiveness and complexity

  • Davide Bresolin
  • Dario Della Monica
  • Angelo Montanari
  • Pietro Sala
  • Guido Sciavicco

Interval temporal logics provide a natural framework for temporal reasoning about interval structures over linearly ordered domains, where intervals are taken as the primitive ontological entities. Their computational behavior mainly depends on two parameters: the set of modalities they feature and the linear orders over which they are interpreted. In this paper, we identify all fragments of Halpern and Shoham's interval temporal logic HS with a decidable satisfiability problem over the class of strongly discrete linear orders as well as over its relevant subclasses (the class of finite linear orders, Z, N, and Z − ). We classify them in terms of both their relative expressive power and their complexity, which ranges from NP-completeness to non-primitive recursiveness.

Details DOI

GandALF Workshop 2014 Workshop Paper

Interval-based Synthesis

  • Angelo Montanari
  • Pietro Sala

We introduce the synthesis problem for Halpern and Shoham's modal logic of intervals extended with an equivalence relation over time points, abbreviated HSeq. In analogy to the case of monadic second-order logic of one successor, the considered synthesis problem receives as input an HSeq formula phi and a finite set Sigma of propositional variables and temporal requests, and it establishes whether or not, for all possible evaluations of elements in Sigma in every interval structure, there exists an evaluation of the remaining propositional variables and temporal requests such that the resulting structure is a model for phi. We focus our attention on decidability of the synthesis problem for some meaningful fragments of HSeq, whose modalities are drawn from the set A (meets), Abar (met by), B (begins), Bbar (begun by), interpreted over finite linear orders and natural numbers. We prove that the fragment ABBbareq is decidable (non-primitive recursive hard), while the fragment AAbarBBbar turns out to be undecidable. In addition, we show that even the synthesis problem for ABBbar becomes undecidable if we replace finite linear orders by natural numbers.

PDF Details DOI

TIME Conference 2014 Conference Paper

Metric Propositional Neighborhood Logic with an Equivalence Relation

  • Angelo Montanari
  • Marco Pazzaglia
  • Pietro Sala

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

Details

Highlights Conference 2013 Conference Abstract

Adding an equivalence relation to the interval logic complexity and expressiveness

  • Angelo Montanari
  • Pietro Sala

We study the effects of the addition of an equivalence relation to one of the most representative interval temporal logics, namely, the logic ABBbar of Allen's relations "meets", "begun by", and "begins". We first prove that the satisfiability problem for the resulting logic ABBbar-sim remains decidable over finite linear orders, but it becomes nonprimitive recursive, while decidability is lost over $\bbN$. Then, we show that ABBbar-sim is expressive enough to define $\omega{S}$-regular languages.

PDF Details

TCS Journal 2013 Journal Article

Optimal decision procedures for MPNL over finite structures, the natural numbers, and the integers

  • Davide Bresolin
  • Angelo Montanari
  • Pietro Sala
  • Guido Sciavicco

Interval temporal logics provide a natural framework for qualitative and quantitative temporal reasoning over interval structures, where the truth of formulas is defined over intervals rather than points. In this paper, we study the complexity of the satisfiability problem for Metric Propositional Neighborhood Logic (MPNL). MPNL features two modalities to access intervals “to the left” and “to the right” of the current one, respectively, plus an infinite set of length constraints. MPNL has been recently shown to be decidable over finite linear orders and the natural numbers by a doubly exponential procedure, leaving the tightness of the complexity bound as an open problem. We improve such a result by proving that the satisfiability problem for MPNL over finite linear orders and the natural numbers, as well as over the integers, is actually EXPSPACE-complete, even when length constraints are encoded in binary.

Details DOI

TIME Conference 2012 Conference Paper

An Optimal Tableau System for the Logic of Temporal Neighborhood over the Reals

  • Angelo Montanari
  • Pietro Sala

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.

Details

ECAI Conference 2012 Conference Paper

Interval Temporal Logics over Finite Linear Orders: the Complete Picture

  • Davide Bresolin
  • Dario Della Monica
  • Angelo Montanari
  • Pietro Sala
  • Guido Sciavicco

Interval temporal logics provide a natural framework for temporal reasoning about interval structures over linearly ordered domains, where intervals are taken as the primitive ontological entities. In this paper, we identify all fragments of Halpern and Shoham's interval temporal logic HS whose finite satisfiability problem is decidable. We classify them in terms of both relative expressive power and complexity. We show that there are exactly 62 expressively-different decidable fragments, whose complexity ranges from NP-complete to non-primitive recursive (all other HS fragments have been already shown to be undecidable).

Details

GandALF Workshop 2012 Workshop Paper

Interval Temporal Logics over Strongly Discrete Linear Orders: the Complete Picture

  • Davide Bresolin
  • Dario Della Monica
  • Angelo Montanari
  • Pietro Sala
  • Guido Sciavicco

Interval temporal logics provide a general framework for temporal reasoning about interval structures over linearly ordered domains, where intervals are taken as the primitive ontological entities. In this paper, we identify all fragments of Halpern and Shoham's interval temporal logic HS with a decidable satisfiability problem over the class of strongly discrete linear orders. We classify them in terms of both their relative expressive power and their complexity. We show that there are exactly 44 expressively different decidable fragments, whose complexity ranges from NP to EXPSPACE. In addition, we identify some new undecidable fragments (all the remaining HS fragments were already known to be undecidable over strongly discrete linear orders). We conclude the paper by an analysis of the specific case of natural numbers, whose behavior slightly differs from that of the whole class of strongly discrete linear orders. The number of decidable fragments over natural numbers raises up to 47: three undecidable fragments become decidable with a non-primitive recursive complexity.

PDF Details DOI

GandALF Workshop 2011 Workshop Paper

An Optimal Decision Procedure for MPNL over the Integers

  • Davide Bresolin
  • Angelo Montanari
  • Pietro Sala
  • Guido Sciavicco

Interval temporal logics provide a natural framework for qualitative and quantitative temporal reason- ing over interval structures, where the truth of formulae is defined over intervals rather than points. In this paper, we study the complexity of the satisfiability problem for Metric Propositional Neigh- borhood Logic (MPNL). MPNL features two modalities to access intervals "to the left" and "to the right" of the current one, respectively, plus an infinite set of length constraints. MPNL, interpreted over the naturals, has been recently shown to be decidable by a doubly exponential procedure. We improve such a result by proving that MPNL is actually EXPSPACE-complete (even when length constraints are encoded in binary), when interpreted over finite structures, the naturals, and the in- tegers, by developing an EXPSPACE decision procedure for MPNL over the integers, which can be easily tailored to finite linear orders and the naturals (EXPSPACE-hardness was already known).

PDF Details DOI

TIME Conference 2011 Conference Paper

Temporal Functional Dependencies Based on Interval Relations

  • Carlo Combi
  • Pietro Sala

In the last years the representation and management of temporal information has become crucial for several computer applications. In the temporal database literature, every fact stored into a database may be equipped with two temporal dimensions: the valid time, that describes the time when the fact is true in the modeled reality, and the transaction time, that describes the time when the fact is current in the database and it can be retrieved. Temporal functional dependencies (TFDs) add (transaction) valid time to classical functional dependencies (FDs) in order to express database integrity constraints over the flow of time. Currently, proposals dealing with TFDs adopt a point-based approach, where tuples hold at specific time points. Moreover, TFDs may involve the use of different granularities (i. e. , partitions of the time domain), to express integrity constraints as "for each month, the salary of an employee depends only on his role". At the best of our knowledge, there are no proposals dealing with interval-based temporal functional dependencies (ITFDs for short) where the associated valid time is represented by an interval. In this paper, we propose a set of ITFDs based on the Allen's interval relations, we analyze their expressive power with respect to other TFDs proposed in the literature and we propose an algorithm for verifying ITFDs in a database system.

Details

TIME Conference 2010 Conference Paper

A Decidable Spatial Generalization of Metric Interval Temporal Logic

  • Davide Bresolin
  • Pietro Sala
  • Dario Della Monica
  • Angelo Montanari
  • Guido Sciavicco

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.

Details

GandALF Workshop 2010 Workshop Paper

Begin, After, and Later: a Maximal Decidable Interval Temporal Logic

  • Davide Bresolin
  • Pietro Sala
  • Guido Sciavicco

Interval temporal logics (ITLs) are logics for reasoning about temporal statements expressed over intervals, i. e. , periods of time. The most famous ITL studied so far is Halpern and Shoham's HS, which is the logic of the thirteen Allen's interval relations. Unfortunately, HS and most of its fragments have an undecidable satisfiability problem. This discouraged the research in this area until recently, when a number non-trivial decidable ITLs have been discovered. This paper is a contribution towards the complete classification of all different fragments of HS. We consider different combinations of the interval relations Begins, After, Later and their inverses Abar, Bbar, and Lbar. We know from previous works that the combination ABBbarAbar is decidable only when finite domains are considered (and undecidable elsewhere), and that ABBbar is decidable over the natural numbers. We extend these results by showing that decidability of ABBar can be further extended to capture the language ABBbarLbar, which lays in between ABBar and ABBbarAbar, and that turns out to be maximal w. r. t decidability over strongly discrete linear orders (e. g. finite orders, the naturals, the integers). We also prove that the proposed decision procedure is optimal with respect to the complexity class.

PDF Details DOI

TIME Conference 2010 Conference Paper

Decidability of the Logics of the Reflexive Sub-interval and Super-interval Relations over Finite Linear Orders

  • Angelo Montanari
  • Ian Pratt-Hartmann
  • Pietro Sala

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.

Details

CSL Conference 2009 Conference Paper

A Decidable Spatial Logic with Cone-Shaped Cardinal Directions

  • Angelo Montanari
  • Gabriele Puppis
  • Pietro Sala

Abstract We introduce a spatial modal logic based on cone-shaped cardinal directions over the rational plane and we prove that, unlike projection-based ones, such as, for instance, Compass Logic, its satisfiability problem is decidable (PSPACE-complete). We also show that it is expressive enough to subsume meaningful interval temporal logics, thus generalizing previous results in the literature, e. g. , its decidability implies that of the subinterval/superinterval temporal logic interpreted over the rational line.

Details

TIME Conference 2008 Conference Paper

An optimal tableau for Right Propositional Neighborhood Logic over Trees

  • Davide Bresolin
  • Angelo Montanari
  • Pietro Sala

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.

Details

JELIA Conference 2008 Conference Paper

Optimal Tableaux for Right Propositional Neighborhood Logic over Linear Orders

  • Davide Bresolin
  • Angelo Montanari
  • Pietro Sala
  • Guido Sciavicco

Abstract The study of interval temporal logics on linear orders is a meaningful research area in computer science and artificial intelligence. Unfortunately, even when restricted to propositional languages, most interval logics turn out to be undecidable. Decidability has been usually recovered by imposing severe syntactic and/or semantic restrictions. In the last years, tableau-based decision procedures have been obtained for logics of the temporal neighborhood and logics of the subinterval relation over specific classes of temporal structures. In this paper, we develop an optimal NEXPTIME tableau-based decision procedure for the future fragment of Propositional Neighborhood Logic over the whole class of linearly ordered domains.

Details
v2026.09.13