Angelo Montanari

AIJ Journal 2026 Journal Article

An optimal pastification algorithm for LTL[X,F] and LTL[X,G]

• Alessandro Artale
• Luca Geatti
• Nicola Gigante
• Alessio Mansutti
• Andrea Mazzullo
• Angelo Montanari

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

AAAI Conference 2026 Conference Paper

Automata-less Monitoring via Trace-Checking

• Andrea Brunello
• Luca Geatti
• Angelo Montanari
• Nicola Saccomanno

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.

AAAI Conference 2026 Conference Paper

Do LLMs Really Struggle at NL-FOL Translation? Revealing Their Strengths via a Novel Benchmarking Strategy

• Andrea Brunello
• Luca Geatti
• Michele Mignani
• Angelo Montanari
• Nicola Saccomanno

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.

ECAI Conference 2025 Conference Paper

Interpretable Early Failure Detection via Machine Learning and Trace Checking-Based Monitoring

• Andrea Brunello
• Luca Geatti
• Angelo Montanari
• Nicola Saccomanno

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.

I&C Journal 2025 Journal Article

Succinctness issues for LTL and safety and cosafety fragments of LTL

• Alessandro Artale
• Luca Geatti
• Nicola Gigante
• Andrea Mazzullo
• Angelo Montanari

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.

IJCAI Conference 2024 Conference Paper

Learning What to Monitor: Using Machine Learning to Improve past STL Monitoring

• Andrea Brunello
• Luca Geatti
• Angelo Montanari
• Nicola Saccomanno

Monitoring is a runtime verification technique that can be used to check whether an execution of a system (trace) satisfies or not a given set of properties. Compared to other formal verification techniques, e. g. , model checking, one needs to specify the properties to be monitored, but a complete model of the system is no longer necessary. First, we introduce the pure past fragment of Signal Temporal Logic (ppSTL), and we use it to define the monitorable safety (G(ppSTL)) and cosafety (F(ppSTL)) fragments of STL, which properly extend the commonly-used bounded-future fragment. Then, we devise a multi-objective genetic programming algorithm to automatically extend the set of properties to monitor on the basis of the history of failure traces collected over time. The framework resulting from the integration of the monitor and the learning algorithm is then experimentally validated on various public datasets. The outcomes of the experimentation confirm the effectiveness of the proposed solution.

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.

KR Conference 2023 Conference Paper

A Singly Exponential Transformation of LTL[X, F] into Pure Past LTL

• Alessandro Artale
• Luca Geatti
• Nicola Gigante
• Andrea Mazzullo
• Angelo Montanari

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.

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.

AAAI Conference 2023 Conference Paper

Complexity of Safety and coSafety Fragments of Linear Temporal Logic

• Alessandro Artale
• Luca Geatti
• Nicola Gigante
• Andrea Mazzullo
• Angelo Montanari

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

TIME Conference 2023 Conference Paper

LTL over Finite Words Can Be Exponentially More Succinct Than Pure-Past LTL, and vice versa

• Alessandro Artale
• Luca Geatti
• Nicola Gigante
• Andrea Mazzullo
• Angelo Montanari

Linear Temporal Logic over finite traces (LTL_𝖿) has proved itself to be an important and effective formalism in formal verification as well as in artificial intelligence. Pure past LTL_𝖿 (pLTL) is the logic obtained from LTL_𝖿 by replacing each (future) temporal operator by a corresponding past one, and is naturally interpreted at the end of a finite trace. It is known that each property definable in LTL_𝖿 is also definable in pLTL, and ǐceversa. However, despite being extensively used in practice, to the best of our knowledge, there is no systematic study of their succinctness. In this paper, we investigate the succinctness of LTL_𝖿 and pLTL. First, we prove that pLTL can be exponentially more succinct than LTL_𝖿 by showing that there exists a property definable with a pLTL formula of size n such that the size of all LTL_𝖿 formulas defining it is at least exponential in n. Then, we prove that LTL_𝖿 can be exponentially more succinct than pLTL as well. This result shows that, although being expressively equivalent, LTL_𝖿 and pLTL are incomparable when succinctness is concerned. In addition, we study the succinctness of Safety-LTL (the syntactic safety fragment of LTL over infinite traces) with respect to its canonical form G(pLTL), whose formulas are of the form G(α), G being the globally operator and α a pLTL formula. We prove that G(pLTL) can be exponentially more succinct than Safety-LTL, and that the same holds for the dual cosafety fragment.

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

TIME Conference 2023 Conference Paper

Qualitative past Timeline-Based Games (Extended Abstract)

• Renato Acampora
• Luca Geatti
• Nicola Gigante
• Angelo Montanari

This extended abstract discusses timeline-based planning, a modeling approach that offers a unique way to model complex systems. Recently, the timeline-based planning framework has been extended to handle general nondeterminism in a game-theoretic setting, resulting in timeline-based games. In this context, the problem of establishing whether a timeline-based game admits a winning strategy and synthesizing such a strategy have been addressed. We propose exploring simpler yet expressive fragments of timeline-based games by leveraging results about the role of past operators in synthesis from temporal logic specifications. The qualitative fragment of timeline-based planning is a good starting point for this exploration. We suggest introducing syntactic restrictions on synchronization rules so that they only constrain the behavior of the system before the current time point, which is expected to lower the complexity of synthesizing timeline-based games to EXPTIME.

TCS Journal 2022 Journal Article

Complexity issues for timeline-based planning over dense time under future and minimal semantics

• Laura Bozzelli
• Angelo Montanari
• Adriano Peron

The problem of timeline-based planning (TP) over dense temporal domains is known to be undecidable in the general case. We first prove that the restriction to the future semantics does not suffice to recover decidability. Then, we introduce two semantic variants of TP, called strong minimal and weak minimal semantics, and show that they allow one 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 one, but the weak minimal variant distinguishes minimality in the past from minimality in the future. Surprisingly, we show that, despite the (apparently) small differences between the two semantics, the TP problem is still undecidable for the strong minimal one, while it is PSPACE-complete for the weak minimal one. 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 us 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. 1

GandALF Workshop 2022 Workshop Paper

Controller Synthesis for Timeline-based Games

• Renato Acampora
• Luca Geatti
• Nicola Gigante
• Angelo Montanari
• Valentino Picotti

In the timeline-based approach to planning, originally born in the space sector, 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, outlining an approach to controller synthesis for timeline-based games.

AIJ Journal 2022 Journal Article

Decidability and complexity of action-based temporal planning over dense time

• Nicola Gigante
• Andrea Micheli
• Angelo Montanari
• Enrico Scala

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

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.

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.

AIIM Journal 2021 Journal Article

AIOSA: An approach to the automatic identification of obstructive sleep apnea events based on deep learning

• Andrea Bernardini
• Andrea Brunello
• Gian Luigi Gigli
• Angelo Montanari
• Nicola Saccomanno

Obstructive Sleep Apnea Syndrome (OSAS) is the most common sleep-related breathing disorder. It is caused by an increased upper airway resistance during sleep, which determines episodes of partial or complete interruption of airflow. The detection and treatment of OSAS is particularly important in patients who suffered a stroke, because the presence of severe OSAS is associated with higher mortality, worse neurological deficits, worse functional outcome after rehabilitation, and a higher likelihood of uncontrolled hypertension. The gold standard test for diagnosing OSAS is polysomnography (PSG). Unfortunately, performing a PSG in an electrically hostile environment, like a stroke unit, on neurologically impaired patients is a difficult task; moreover, the number of strokes per day vastly outnumbers the availability of polysomnographs and dedicated healthcare professionals. Hence, a simple and automated recognition system to identify OSAS cases among acute stroke patients, relying on routinely recorded vital signs, is highly desirable. The vast majority of the work done so far focuses on data recorded in ideal conditions and highly selected patients, and thus it is hardly exploitable in real-life circumstances, where it would be of actual use. In this paper, we propose a novel convolutional deep learning architecture able to effectively reduce the temporal resolution of raw waveform data, like physiological signals, extracting key features that can be used for further processing. We exploit models based on such an architecture to detect OSAS events in stroke unit recordings obtained from the monitoring of unselected patients. Unlike existing approaches, annotations are performed at one-second granularity, allowing physicians to better interpret the model outcome. Results are considered to be satisfactory by the domain experts. Moreover, through tests run on a widely-used public OSAS dataset, we show that the proposed approach outperforms current state-of-the-art solutions.

I&C Journal 2021 Journal Article

Complexity analysis of a unifying algorithm for model checking interval temporal logic

• Laura Bozzelli
• Angelo Montanari
• Adriano Peron

Model checking (MC) for Halpern and Shoham's interval temporal logic HS has been recently shown to be decidable. An intriguing open question is its exact complexity for full HS: it is at least EXPSPACE-hard, and the only known upper bound, which exploits an abstract representation of Kripke structure paths (descriptor), is non-elementary. In this paper, we provide a uniform framework to MC for full HS and meaningful fragments of it, with a specific type of descriptor for each fragment. Then, we devise a general MC alternating algorithm, parameterized by the descriptor's type, 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 its complexity and give tight bounds on the length of certificates. For two types of descriptor, we obtain exponential upper and lower bounds; for the other ones, we provide non-elementary lower bounds.

GandALF Workshop 2021 Workshop Paper

Expressiveness of Extended Bounded Response LTL

• Alessandro Cimatti
• Luca Geatti
• Nicola Gigante
• Angelo Montanari
• Stefano Tonetta

Extended Bounded Response LTL with Past (LTLEBR+P) is a safety fragment of Linear Temporal Logic with Past (LTL+P) that has been recently introduced in the context of reactive synthesis. The strength of LTLEBR+P is a fully symbolic compilation of formulas into symbolic deterministic automata. Its syntax is organized in four levels. The first three levels feature (a particular combination of) future temporal modalities, the last one admits only past temporal operators. At the base of such a structuring there are algorithmic motivations: each level corresponds to a step of the algorithm for the automaton construction. The complex syntax of LTLEBR+P made it difficult to precisely characterize its expressive power, and to compare it with other LTL+P safety fragments. In this paper, we first prove that LTLEBR+P is expressively complete with respect to the safety fragment of LTL+P, that is, any safety language definable in LTL+P can be formalized in LTLEBR+P, and vice versa. From this, it follows that LTLEBR+P and Safety-LTL are expressively equivalent. Then, we show that past modalities play an essential role in LTLEBR+P: we prove that the future fragment of LTLEBR+P is strictly less expressive than full LTLEBR+P.

I&C Journal 2021 Journal Article

One-pass and tree-shaped tableau systems for TPTL and TPTLb+Past

• Luca Geatti
• Nicola Gigante
• Angelo Montanari
• Mark Reynolds

Linear Temporal Logic (LTL) is one of the most commonly used formalisms for representing and reasoning about temporal properties of computations. Its application domains range from formal verification to artificial intelligence. Many real-time extensions of LTL have been proposed over the years, including Timed Propositional Temporal Logic (TPTL), that makes it possible to constrain the temporal ordering of pairs of events as well as the exact time elapsed between them. The paper focuses on TPTL and Bounded TPTL with Past ( Image 1 ), a bounded variant of TPTL enriched with past operators, which has been recently introduced to formalise a meaningful class of timeline-based planning problems. Image 1 allows one to refer to the past while keeping the computational complexity under control: in contrast to the full TPTL with Past (TPTL+P), whose satisfiability problem is non-elementary, the satisfiability problem for Image 1 is Image 2 -complete. The paper deals with the satisfiability problem for TPTL and Image 1 by providing an original tableau system for each of them that suitably generalises Reynolds' one-pass and tree-shaped tableau for LTL. First, we show how to handle past operators, by devising a one-pass and tree-shaped tableau system for LTL with Past (LTL+P). Then, we adapt it to TPTL and Image 1, providing full proofs of the soundness and completeness of the resulting systems. In particular, completeness is proved by exploiting a novel model-theoretic argument that, compared to the one originally employed for the LTL system, provides a deeper understanding of the crucial role of the prune rule of the system.

TIME Conference 2021 Conference Paper

Past Matters: Supporting LTL+Past in the BLACK Satisfiability Checker

• Luca Geatti
• Nicola Gigante
• Angelo Montanari
• Gabriele Venturato

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.

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

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.

TIME Conference 2020 Conference Paper

Complexity of Qualitative Timeline-Based Planning

• Dario Della Monica
• Nicola Gigante
• Salvatore La Torre
• Angelo Montanari

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.

AAAI Conference 2020 Conference Paper

Decidability and Complexity of Action-Based Temporal Planning over Dense Time

• Nicola Gigante
• Andrea Micheli
• Angelo Montanari
• Enrico Scala

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.

I&C Journal 2020 Journal Article

Model checking interval temporal logics with regular expressions

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

In this paper, we investigate the model checking (MC) problem for Halpern and Shoham's modal logic of time intervals (HS) and its fragments, where labeling of intervals is defined by regular expressions. The MC problem for HS has recently emerged as a viable alternative to the traditional (point-based) temporal logic MC. Most expressiveness and complexity results have been obtained by imposing suitable restrictions on interval labeling, namely, by either defining it in terms of interval endpoints, or by constraining a proposition letter to hold over an interval if and only if it holds over each component state (homogeneity assumption). In both cases, the expressiveness of HS gets noticeably limited, in particular when fragments of HS are considered. A possible way to increase the expressiveness of interval temporal logic MC was proposed by Lomuscio and Michaliszyn, who suggested to use regular expressions to define interval labeling, i. e. , the properties that hold true over intervals/computation stretches, based on their component points/system states. In this paper, we provide a systematic account of decidability and complexity issues for model checking HS and its fragments extended with regular expressions. We first prove that MC for (full) HS extended with regular expressions is decidable by an automaton-theoretic argument. Though the exact complexity of full HS MC remains an open issue, the complexity of all relevant proper fragments of HS is here determined. In particular, we provide an asymptotically optimal bound to the complexity of the two syntactically maximal fragments A A ‾ B B ‾ E ‾ and A A ‾ E B ‾ E ‾, by showing that their MC problem is AEX P pol -complete ( AEX P pol is the complexity class of problems decided by exponential-time bounded alternating Turing Machines making a polynomially bounded number of alternations). Moreover, we show that a better result holds for A A ‾ B B ‾, A A ‾ E E ‾ and all their sub-fragments, whose MC problem turns out to be PSPACE-complete.

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.

TCS Journal 2020 Journal Article

On timeline-based games and their complexity

• Nicola Gigante
• Angelo Montanari
• Andrea Orlandini
• Marta Cialdea Mayer
• Mark Reynolds

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 real-world domains. 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 2EXPTIME-complete.

TCS Journal 2020 Journal Article

Timeline-based planning over dense temporal domains

• Laura Bozzelli
• Alberto Molinari
• Angelo Montanari
• Adriano Peron
• Gerhard Woeginger

Planning is one of the most studied problems in computer science. In this paper, we focus on the timeline-based approach, where the domain is modeled by a set of independent, but interacting, components, each one represented by a number of state variables, whose behavior over time (timelines) is governed by a set of temporal constraints (transition functions and synchronization rules). Whereas the time domain is usually assumed to be discrete, here we address decidability and complexity issues for timeline-based planning (TP) over dense time. We first prove that dense TP is undecidable in the general case; then, we show that decidability can be recovered by restricting to synchronization rules with a suitable future semantics. More “tractable” settings can be obtained by additionally constraining the form of intervals used in rules: EXPSPACE-completeness is obtained by avoiding singular intervals, and PSPACE-completeness by admitting only intervals of the forms [ 0, a ] and [ b, + ∞ [. Finally, NP-completeness can be proved for dense TP with purely existential rules only.

TIME Conference 2019 Conference Paper

Complexity Analysis of a Unifying Algorithm for Model Checking Interval Temporal Logic

• Laura Bozzelli
• Angelo Montanari
• Adriano Peron

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.

OVERLAY Workshop 2019 Workshop Paper

Pairing Monitoring with Machine Learning for Smart System Verification and Predictive Maintenance

• Andrea Brunello
• Dario Della Monica
• Angelo Montanari

TIME Conference 2019 Conference Paper

Synthesis of LTL Formulas from Natural Language Texts: State of the Art and Research Directions

• Andrea Brunello
• Angelo Montanari
• Mark Reynolds 0001

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.

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.

TIME Conference 2018 Conference Paper

A Game-Theoretic Approach to Timeline-Based Planning with Uncertainty

• Nicola Gigante
• Angelo Montanari
• Marta Cialdea Mayer
• Andrea Orlandini
• Mark Reynolds 0001

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.

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.

GandALF Workshop 2018 Workshop Paper

Complexity of Timeline-Based Planning over Dense Temporal Domains: Exploring the Middle Ground

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

In this paper, we address complexity issues for timeline-based planning over dense temporal domains. The planning problem is modeled by means of a set of independent, but interacting, components, each one represented by a number of state variables, whose behavior over time (timelines) is governed by a set of temporal constraints (synchronization rules). While the temporal domain is usually assumed to be discrete, here we consider the dense case. Dense timeline-based planning has been recently shown to be undecidable in the general case; decidability (NP-completeness) can be recovered by restricting to purely existential synchronization rules (trigger-less rules). In this paper, we investigate the unexplored area of intermediate cases in between these two extremes. We first show that decidability and non-primitive recursive-hardness can be proved by admitting synchronization rules with a trigger, but forcing them to suitably check constraints only in the future with respect to the trigger (future simple rules). More "tractable" results can be obtained by additionally constraining the form of intervals in future simple rules: EXPSPACE-completeness is guaranteed by avoiding singular intervals, PSPACE-completeness by admitting only intervals of the forms [0, a] and [b, +∞[.

KR Conference 2018 Short Paper

Decidability and Complexity of Timeline-based Planning over Dense Temporal Domains

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

In timeline-based planning, the planning domain is modeled as a set of independent, but interacting, components each one represented by a number of state variables, whose behavior over time (timelines) is governed by temporal constraints (synchronization rules). The temporal domain is typically assumed to be discrete. In this paper, we address decidability and complexity issues for timeline-based planning over dense temporal domains without resorting to any form of discretization. We first prove that the general problem is undecidable, and then we show that decidability can be recovered by constraining the logical structure of synchronization rules.

I&C Journal 2018 Journal Article

Model checking for fragments of Halpern and Shoham's interval temporal logic based on track representatives

• Alberto Molinari
• Angelo Montanari
• Adriano Peron

Model checking allows one to automatically verify a specification of the expected properties of a system against a formal model of its behavior (generally, a Kripke structure). Point-based temporal logics, such as LTL, CTL, and CTL⁎, that describe how the system evolves state-by-state, are commonly used as specification languages. They proved themselves quite successful in a variety of application domains. However, properties constraining the temporal ordering of temporally extended events as well as properties involving temporal aggregations, which are inherently interval-based, can not be properly dealt with by them. Interval temporal logics (ITLs), that take intervals as their primitive temporal entities, turn out to be well-suited for the specification and verification of interval properties of computations (we interpret all the tracks of a Kripke structure as computation intervals). In this paper, we study the model checking problem for some fragments of Halpern and Shoham's modal logic of time intervals (HS). HS features one modality for each possible ordering relation between pairs of intervals (the so-called Allen's relations). First, we describe an EXPSPACE model checking algorithm for the HS fragment of Allen's relations meets, met-by, starts, started-by, and finishes, which exploits the possibility of finding, for each track (of unbounded length), an equivalent bounded-length track representative. While checking a property, it only needs to consider tracks whose length does not exceed the given bound. Then, we prove the model checking problem for such a fragment to be PSPACE-hard. Finally, we identify other well-behaved HS fragments which are expressive enough to capture meaningful interval properties of systems, such as mutual exclusion, state reachability, and non-starvation, and whose computational complexity is less than or equal to that of LTL.

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.

GandALF Workshop 2018 Workshop Paper

One-Pass and Tree-Shaped Tableau Systems for TPTL and TPTLb+Past

• Luca Geatti
• Nicola Gigante
• Angelo Montanari
• Mark Reynolds

In this paper, we propose a novel one-pass and tree-shaped tableau method for Timed Propositional Temporal Logic and for a bounded variant of its extension with past operators. Timed Propositional Temporal Logic (TPTL) is a real-time temporal logic, with an EXPSPACE-complete satisfiability problem, which has been successfully applied to the verification of real-time systems. In contrast to LTL, adding past operators to TPTL makes the satisfiability problem for the resulting logic (TPTL+P) non-elementary. In this paper, we devise a one-pass and tree-shaped tableau for both TPTL and bounded TPTL+P (TPTLb+P), a syntactic restriction introduced to encode timeline-based planning problems, which recovers the EXPSPACE-complete complexity. The tableau systems for TPTL and TPTLb+P are presented in a unified way, being very similar to each other, providing a common skeleton that is then specialised to each logic. In doing that, we characterise the semantics of TPTLb+P in terms of a purely syntactic fragment of TPTL+P, giving a translation that embeds the former into the latter. Soundness and completeness of the system are proved fully. In particular, we give a greatly simplified model-theoretic completeness proof, which sidesteps the complex combinatorial argument used by known proofs for the one-pass and tree-shaped tableau systems for LTL and LTL+P.

LPAR Conference 2017 Conference Paper

A One-Pass Tree-Shaped Tableau for LTL+Past

• Nicola Gigante
• Angelo Montanari
• Mark Reynolds 0001

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.

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.

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.

ICAPS Conference 2017 Conference Paper

Complexity of Timeline-Based Planning

• Nicola Gigante
• Angelo Montanari
• Marta Cialdea Mayer
• Andrea Orlandini

Timeline-based planning is a paradigm that models temporal planning domains as sets of independent, but interacting, components. The behavior of the components can be described by means of a number of state variables whose evolution and interactions over time are governed by a set of temporal constraints. This paradigm is different from the one underlying the common action-based formalisms, such as PDDL, where the focus is on what can be done by an executive agent. Although successfully used in many real-world applications, little work has been done on the expressiveness and complexity of the timeline-based formalism. The present paper provides a characterization of the complexity of non-flexible timeline-based planning, by proving that a general formulation of the problem is EXPSPACE-complete. Such a result extends a previous work where the same complexity bound was proved for a restricted fragment of timeline-based planning that was shown to be expressive enough to capture action-based temporal planning. In addition, we prove that requiring an upper bound to the solution horizon as part of the input decreases the complexity of the problem, that becomes NEXPTIME-complete.

TIME Conference 2017 Conference Paper

Evaluation of Temporal Datasets via Interval Temporal Logic Model Checking

• Dario Della Monica
• David de Frutos-Escrig
• Angelo Montanari
• Aniello Murano
• Guido Sciavicco

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.

GandALF Workshop 2017 Workshop Paper

On the Complexity of Model Checking for Syntactically Maximal Fragments of the Interval Temporal Logic HS with Regular Expressions

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

In this paper, we investigate the model checking (MC) problem for Halpern and Shoham's interval temporal logic HS. In the last years, interval temporal logic MC has received an increasing attention as a viable alternative to the traditional (point-based) temporal logic MC, which can be recovered as a special case. Most results have been obtained under the homogeneity assumption, that constrains a proposition letter to hold over an interval if and only if it holds over each component state. Recently, Lomuscio and Michaliszyn proposed a way to relax such an assumption by exploiting regular expressions to define the behaviour of proposition letters over intervals in terms of their component states. When homogeneity is assumed, the exact complexity of MC is a difficult open question for full HS and for its two syntactically maximal fragments AA'BB'E' and AA'EB'E'. In this paper, we provide an asymptotically optimal bound to the complexity of these two fragments under the more expressive semantic variant based on regular expressions by showing that their MC problem is AEXP_pol-complete, where AEXP_pol denotes the complexity class of problems decided by exponential-time bounded alternating Turing Machines making a polynomially bounded number of alternations.

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

TIME Conference 2016 Invited Paper

Interval Temporal Logics Model Checking

• Angelo Montanari

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.

IJCAI Conference 2016 Conference Paper

Leviathan: A New LTL Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau

• Matteo Bertello
• Nicola Gigante
• Angelo Montanari
• Mark Reynolds

The paper presents Leviathan, an LTL satisfiability checking tool based on a novel one-pass, tree-like tableau system, which is way simpler than existing solutions. Despite the simplicity of the algorithm, the tool has performance comparable in speed and memory consumption with other tools on a number of standard benchmark sets, and, in various cases, it outperforms the other tableau-based tools.

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

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.

TIME Conference 2016 Conference Paper

Timelines Are Expressive Enough to Capture Action-Based Temporal Planning

• Nicola Gigante
• Angelo Montanari
• Marta Cialdea Mayer
• Andrea Orlandini

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.

CSL Conference 2015 Conference Paper

A Model Checking Procedure for Interval Temporal Logics based on Track Representatives

• Alberto Molinari
• Angelo Montanari
• Adriano Peron

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.

TIME Conference 2015 Conference Paper

Complexity of ITL Model Checking: Some Well-Behaved Fragments of the Interval Logic HS

• Alberto Molinari
• Angelo Montanari
• Adriano Peron

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.

I&C Journal 2015 Journal Article

Games, Automata, Logics, and Formal Verification (GandALF 2013)

• Angelo Montanari
• Gabriele Puppis
• Tiziano Villa

TIME Conference 2015 Conference Paper

Undecidability of Chop

• Angelo Montanari
• Emilio Muñoz-Velasco
• Guido Sciavicco

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.

TIME Conference 2014 Conference Paper

Checking Interval Properties of Computations

• Angelo Montanari
• Aniello Murano
• Giuseppe Perelli
• Adriano Peron

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.

ECAI Conference 2014 Conference Paper

DL-Lite and Interval Temporal Logics: a Marriage Proposal

• Alessandro Artale
• Davide Bresolin
• Angelo Montanari
• Guido Sciavicco
• Vladislav Ryzhikov

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 (&Hscr; &Sscr;). 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 &Hscr; &Sscr; with DL-Lite.

Highlights Conference 2014 Conference Abstract

Interval Temporal Logics and Equivalence Relations

• Angelo Montanari

Interval temporal logics provide a general framework for temporal representation and reasoning, where 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 two meaningful fragments of Halpern and Shoham's modal logic of time intervals, namely, AA̅ and AB, interpreted over the class of finite linear orders.

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.

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.

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

JELIA Conference 2014 Conference Paper

On the Expressiveness of the Interval Logic of Allen's Relations Over Finite and Discrete Linear Orders

• Luca Aceto
• Dario Della Monica
• Anna Ingólfsdóttir
• Angelo Montanari
• Guido Sciavicco

Abstract Interval temporal logics 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 associates a modal operator with each binary relation between intervals over a linear order (the so-called Allen’s interval relations). A complete classification of all HS fragments with respect to their relative expressive power has been recently given for the classes of all linear orders and of all dense linear orders. The cases of discrete and finite linear orders turn out to be much more involved. In this paper, we make a significant step towards solving the classification problem over those classes of linear orders. First, we illustrate various non-trivial temporal properties that can be expressed by HS fragments when interpreted over finite and discrete linear orders; then, we provide a complete set of definabilities for the HS modalities corresponding to the Allen’s relations meets, later, begins, finishes, and during, as well as the ones corresponding to their inverse relations. The only missing cases are those of the relations overlaps and overlapped by.

TIME Conference 2013 Conference Paper

A Complete Classification of the Expressiveness of Interval Logics of Allen's Relations over Dense Linear Orders

• Luca Aceto
• Dario Della Monica
• Anna Ingólfsdóttir
• Angelo Montanari
• Guido Sciavicco

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.

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.

LPAR Conference 2013 Conference Paper

An Algorithm for Enumerating Maximal Models of Horn Theories with an Application to Modal Logics

• Luca Aceto
• Dario Della Monica
• Anna Ingólfsdóttir
• Angelo Montanari
• Guido Sciavicco

Abstract The fragment of propositional logic known as Horn theories plays a central role in automated reasoning. The problem of enumerating the maximal models of a Horn theory ( MaxMod ) has been proved to be computationally hard, unless P = NP. To the best of our knowledge, the only algorithm available for it is the one based on a brute-force approach. In this paper, we provide an algorithm for the problem of enumerating the maximal subsets of facts that do not entail a distinguished atomic proposition in a definite Horn theory ( MaxNoEntail ). We show that MaxMod is polynomially reducible to MaxNoEntail (and vice versa), making it possible to solve also the former problem using the proposed algorithm. Addressing MaxMod via MaxNoEntail opens, inter alia, the possibility of benefiting from the monotonicity of the notion of entailment. (The notion of model does not enjoy such a property.) We also discuss an application of MaxNoEntail to expressiveness issues for modal logics, which reveals the effectiveness of the proposed algorithm.

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.

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.

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

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.

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

IJCAI Conference 2011 Conference Paper

Expressiveness of the Interval Logics of Allen's Relations on the Class of All Linear Orders: Complete Classification

• Dario Della Monica
• Valentin Goranko
• Angelo Montanari
• Guido Sciavicco

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 inter-definability equations between these modal operators, and thus obtain a complete classification of the family of 212 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.

TIME Conference 2011 Conference Paper

The Dark Side of Interval Temporal Logic: Sharpening the Undecidability Border

• Davide Bresolin
• Dario Della Monica
• Valentin Goranko
• Angelo Montanari
• Guido Sciavicco

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.

TIME Conference 2011 Conference Paper

The Light Side of Interval Temporal Logic: The Bernays-Schönfinkel's Fragment of CDT

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

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.

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.

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.

ECAI Conference 2010 Conference Paper

Metric Propositional Neighborhood Logics: Expressiveness, Decidability, and Undecidability

• Davide Bresolin
• Dario Della Monica
• Valentin Goranko
• Angelo Montanari
• Guido Sciavicco

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.

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.

TIME Conference 2009 Conference Paper

Undecidability of Interval Temporal Logics with the Overlap Modality

• Davide Bresolin
• Dario Della Monica
• Valentin Goranko
• Angelo Montanari
• Guido Sciavicco

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.

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.

LPAR Conference 2008 Conference Paper

Decidable and Undecidable Fragments of Halpern and Shoham's Interval Temporal Logic: Towards a Complete Classification

• Davide Bresolin
• Dario Della Monica
• Valentin Goranko
• Angelo Montanari
• Guido Sciavicco

Abstract Interval temporal logics are based on temporal structures where time intervals, rather than time instants, are the primitive ontological entities. They employ modal operators corresponding to various relations between intervals, known as Allen’s relations. Technically, validity in interval temporal logics translates to dyadic second-order logic, thus explaining their complex computational behavior. The full modal logic of Allen’s relations, called HS, has been proved to be undecidable by Halpern and Shoham under very weak assumptions on the class of interval structures, and this result was discouraging attempts for practical applications and further research in the field. A renewed interest has been recently stimulated by the discovery of interesting decidable fragments of HS. This paper contributes to the characterization of the boundary between decidability and undecidability of HS fragments. It summarizes known positive and negative results, it describes the main techniques applied so far in both directions, and it establishes a number of new undecidability results for relatively small fragments of HS.

CSL Conference 2008 Conference Paper

Non-finite Axiomatizability and Undecidability of Interval Temporal Logics with C, D, and T

• Ian M. Hodkinson
• Angelo Montanari
• Guido Sciavicco

Abstract Interval logics are an important area of computer science. Although attention has been mainly focused on unary operators, an early work by Venema (1991) introduced an expressively complete interval logic language called CDT, based on binary operators, which has many potential applications and a strong theoretical interest. Many very natural questions about CDT and its fragments, such as (non-)finite axiomatizability and (un-)decidability, are still open (as a matter of fact, only a few undecidability results, including the undecidability of CDT, are known). In this paper, we answer most of these questions, showing that almost all fragments of CDT, containing at least one binary operator, are neither finitely axiomatizable with standard rules nor decidable. A few cases remain open.

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.

TCS Journal 2007 Journal Article

Compact and tractable automaton-based representations of time granularities

• Ugo Dal Lago
• Angelo Montanari
• Gabriele Puppis

Most approaches to time granularity proposed in the literature are based on algebraic and logical formalisms [J. Euzenat, A. Montanari, Time granularity, in: M. Fisher, D. Gabbay, L. Vila (Eds.), Handbook of Temporal Reasoning in Artificial Intelligence, Elsevier, 2005, pp. 59–118]. Here we follow an alternative automaton-based approach, originally outlined in [U. Dal Lago, A. Montanari, Calendars, time granularities, and automata, in: Proceedings of the 7th International Symposium on Spatial and Temporal Databases, SSTD, in: LNCS, vol. 2121, Springer, 2001, pp. 279–298], which makes it possible to deal with infinite time granularities in an effective and efficient way. Such an approach provides a neat solution to fundamental algorithmic problems, such as the granularity equivalence and granule conversion problems, which have been often neglected in the literature. In this paper, we focus our attention on two basic optimization problems for the automaton-based representation of time granularities, namely, the problem of computing the smallest representation of a time granularity and that of computing the most tractable representation of it, that is, the one on which crucial algorithms, such as granule conversion algorithms, run fastest.

TIME Conference 2007 Conference Paper

On the Equivalence of Automaton-Based Representations of Time Granularities

• Ugo Dal Lago
• Angelo Montanari
• Gabriele Puppis

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.

TIME Conference 2006 Conference Paper

An automaton-based approach to the verification of timed workflow schemas

• Elisabetta De Maria
• Angelo Montanari
• Marco Zantoni

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.

TIME Conference 2005 Conference Paper

A Uniform Algebraic Characterization of Temporal Functional Dependencies

• Carlo Combi
• Angelo Montanari
• Rosalba Rossato

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.

LPAR Conference 2005 Conference Paper

An Algorithmic Account of Ehrenfeucht Games on Labeled Successor Structures

• Angelo Montanari
• Alberto Policriti
• Nicola Vitacolonna

Abstract Ehrenfeucht-Fraïssé games are commonly used as a method to measure the expressive power of a logic, but they are also a flexible tool to compare structures. To exploit such a comparison power, explicit conditions characterizing the winning strategies for both players must be provided. We give a necessary and sufficient condition for Duplicator to win games played on finite structures with a successor relation and a finite number of unary predicates. This structural characterization suggests an algorithmic approach to the analysis of games, which can be used to compute the “remoteness” of a game and to determine the optimal moves for both players, that is, to derive algorithms for Spoiler and Duplicator that play optimally. We argue that such an algorithmic solution may be used in contexts where the “degree of similarity” between two structures must be measured, such as the comparison of biological sequences.

TIME Conference 2005 Invited Paper

Propositional Interval Temporal Logics: Some Promising Paths

• Angelo Montanari

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.

TIME Conference 2004 Conference Paper

Decidability of the Theory of the Totally Unbounded omega-Layered Structure

• Angelo Montanari
• Gabriele Puppis

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.

JELIA Conference 2004 Conference Paper

Time Granularities and Ultimately Periodic Automata

• Davide Bresolin
• Angelo Montanari
• Gabriele Puppis

Abstract The relevance of the problem of managing periodic phenomena is widely recognized in the area of knowledge representation and reasoning. One of the most effective attempts at dealing with this problem has been the addition of a notion of time granularity to knowledge representation systems. Different formalizations of such a notion have been proposed in the literature, following algebraic, logical, string-based, and automaton-based approaches. In this paper, we focus our attention on the automaton-based one, which allows one to represent a large class of granularities in a compact and suitable to algorithmic manipulation form. We further develop such an approach to make it possible to deal with (possibly infinite) sets of granularities instead of single ones. We define a new class of automata, called Ultimately Periodic Automata, we give a characterization of their expressiveness, and we show how they can be used to encode and to solve a number of fundamental problems, such as the membership problem, the equivalence problem, and the problem of granularity comparison. Moreover, we give an example of their application to a concrete problem taken from clinical medicine.

TIME Conference 2003 Conference Paper

Definability and decidability of binary predicates for time granularity

• Massimo Franceschet
• Angelo Montanari
• Adriano Peron
• Guido Sciavicco

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.

JELIA Conference 2002 Conference Paper

Decidability of Interval Temporal Logics over Split-Frames via Granularity

• Angelo Montanari
• Guido Sciavicco
• Nicola Vitacolonna

Abstract Logics for time intervals provide a natural framework for representing and reasoning about timing properties in various areas of artificial intelligence and computer science. Unfortunately, most interval temporal logics proposed in the literature have been shown to be (highly) undecidable. Decidable fragments of these logics have been obtained by imposing severe restrictions on their expressive power.

TIME Conference 2000 Conference Paper

A Calculus of Macro-Events: Progress Report

• Iliano Cervesato
• Angelo Montanari

The need for constraining the temporal relationships among sets of related events arises in several temporal reasoning tasks, including monitoring, plan validation, planning and diagnosis. Process constructors provide an effective way of packaging related events into individual conceptual chunks, called macro-events. In this paper, we present a first attempt at defining a calculus of macro-events that extends Kowalski and Sergot's (1985) event calculus with process constructors to express effects triggered by complex combinations of event occurrences. We apply this language to model the operations of a simple gas heater and present a Prolog implementation.

MFCS Conference 2000 Conference Paper

Derivability in Locally Quantified Modal Logics via Translation in Set Theory

• Angelo Montanari
• Alberto Policriti
• Matteo Slanina

Abstract Two of the most active research areas in automated deduction in modal logic are the use of translation methods to reduce its derivability problem to that of classical logic and the extension of existing automated reasoning techniques, developed initially for the propositional case, to first-order modal logics. This paper addresses both issues by extending the translation method for propositional modal logics known as □ -as-Pow (read “box-as-powerset”) to a widely used class of first-order modal logics, namely, the class of locally quantified modal logics. To do this, we prove a more general result that allows us to separate (classical) first-order from modal (propositional) reasoning. Our translation can be seen as an example application of this result, in both definition and proof of adequateness.

TIME Conference 1999 Conference Paper

A Graph-Theoretic Approach to Efficiently Reason about Partially Ordered Events in the Event Calculus

• Massimo Franceschet
• Angelo Montanari

We exploit graph-theoretic techniques to efficiently reason about partially ordered events in the Event Calculus. We replace the traditional generate-and-test reasoning strategy by a more efficient generate-only one that operates on the underlying directed acyclic graph of events representing ordering information by pairing breadth-first and depth-first visits in a suitable way. We prove the soundness and completeness of the proposed strategy, and thoroughly analyze its computational complexity. Furthermore, we show how it can be generalized to deal with the Modal Event Calculus, that provides a uniform modal framework for the basic Event Calculus and its skeptical and credulous variants.

TIME Conference 1998 Conference Paper

Event Calculus with Explicit Quantifiers

• Iliano Cervesato
• Massimo Franceschet
• Angelo Montanari

Kowalski and Sergot's (1986) 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. We extend this calculus to give a semantic foundation to our Quantifiers and Connectives Event Calculus (QCEC). In particular, we extend the range of queries accepted by EC, which has so far been limited to Boolean combinations of MVI verification or computation requests, to admit arbitrary quantification over events and properties. We demonstrate the added expressive power by encoding a medical diagnosis problem as a case study. Moreover, we give a /spl lambda/Prolog implementation of this formalism and analyze the computational complexity of the extended calculus.

TIME Conference 1997 Conference Paper

Modal Event Calculi with Preconditions

• Iliano Cervesato
• Massimo Franceschet
• Angelo Montanari

Kowalski and Sergot's (1986) event calculus (EC) is a simple temporal formalism that, given a set of event occurrences, allows the derivation of the maximal validity intervals (MVIs) over which properties initiated or terminated by those events hold. The limited expressive power of EC is notably augmented by permitting events to initiate or terminate a property only if a given set of preconditions hold at their occurrence time. We define a semantic formalization of the event calculus with preconditions. We gain further expressiveness by considering modal variants of this formalism, and show how to adapt our semantic characterization to encompass the additional operators. We discuss the complexity of MVI validation and describe examples showing that modal event calculi with preconditions can be successfully exploited to deal with real-world applications.

ECAI Conference 1996 Conference Paper

A General Modal Framework for the Event Calculus and its Skeptical and Credulous Variants

• Angelo Montanari
• Luca Chittaro
• Iliano Cervesato

KER Journal 1996 Journal Article

Trends in temporal representation and reasoning

• Luca Chittaro
• Angelo Montanari

Time is one of the most relevant topics in AI. It plays a major role in several of AI research areas, ranging from logical foundations to applications of knowledge-based systems. Despite the ubiquity of time in AI, researchers tend to specialise and focus on time in particular contexts or applications, overlooking meaningful connections between different areas. In an attempt to promote crossfertilisation and reduce isolation, the Temporal Representation and Reasoning (TIME) workshop series was started in 1994. The third edition of the workshop was held on May 19–20 1996 in Key West, FL, with S. D. Goodwin and H. J. Hamilton as General Chairs, and L. Chittaro and A. Montanari as Program Chairs. A particular emphasis was given to the foundational aspects of temporal representation and reasoning through an investigation of the relationships between different approaches to temporal issues in AI, computer science and logic.

TIME Conference 1994 Conference Paper

Efficient Handling of Context Dependency in the Cached Event Calculus

• Luca Chittaro
• Angelo Montanari

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.

ECAI Conference 1994 Conference Paper

Skeptical and Credulous Event Calculi for Supporting Modal Queries

• Luca Chittaro
• Angelo Montanari
• Alessandro Provetti