Alessandro Artale

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

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.

KR Conference 2024 Conference Paper

Non-Rigid Designators in Modal and Temporal Free Description Logics

• Alessandro Artale
• Roman Kontchakov
• Andrea Mazzullo
• Frank Wolter

Definite descriptions, such as ‘the General Chair of KR 2024’, are a semantically transparent device for object identification in knowledge representation. In first-order modal logic, definite descriptions have been widely investigated for their non-rigidity, which allows them to designate different objects (or none at all) at different states. We propose expressive modal description logics with non-rigid definite descriptions and names, and investigate decidability and complexity of the satisfiability problem. We first systematically link satisfiability for the one-variable fragment of first-order modal logic with counting to our modal description logics. Then, we prove a promising NEXPTIME-completeness result for concept satisfiability for the fundamental epistemic multi-agent logic S5n and its neighbours, and show that some expressive logics that are undecidable with constant domain become decidable (but Ackermann-hard) with expanding domains. Finally, we conduct a fine-grained analysis of decidability of temporal logics.

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.

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.

JAIR Journal 2022 Journal Article

First-Order Rewritability and Complexity of Two-Dimensional Temporal Ontology-Mediated Queries

• Alessandro Artale
• Roman Kontchakov
• Alisa Kovtunova
• Vladislav Ryzhikov
• Frank Wolter
• Michael Zakharyaschev

Aiming at ontology-based data access to temporal data, we design two-dimensional temporal ontology and query languages by combining logics from the (extended) DL-Lite family with linear temporal logic LTL over discrete time (Z, 1, and FO(RPR) that admits relational primitive recursion. In terms of circuit complexity, FO( 0 and NC 1, respectively. We proceed in three steps. First, we define a hierarchy of 2D DL-Lite/LTL ontology languages and investigate the FO-rewritability of OMQs with atomic queries by constructing projections onto 1D LTL OMQs and employing recent results on the FO-rewritability of propositional LTL OMQs. As the projections involve deciding consistency of ontologies and data, we also consider the consistency problem for our languages. While the undecidability of consistency for 2D ontology languages with expressive Boolean role inclusions might be expected, we also show that, rather surprisingly, the restriction to Krom and Horn role inclusions leads to decidability (and ExpSpace-completeness), even if one admits full Booleans on concepts. As a final step, we lift some of the rewritability results for atomic OMQs to OMQs with expressive positive temporal instance queries. The lifting results are based on an in-depth study of the canonical models and only concern Horn ontologies.

IJCAI Conference 2022 Conference Paper

On the First-Order Rewritability of Ontology-Mediated Queries in Linear Temporal Logic (Extended Abstract)

• Alessandro Artale
• Roman Kontchakov
• Alisa Kovtunova
• Vladislav Ryzhikov
• Frank Wolter
• Michael Zakharyaschev

We argue that linear temporal logic LTL in tandem with monadic first-order logic can be used as a ba- sic language for ontology-based access to tempo- ral data and obtain a classification of the resulting ontology-mediated queries according to the type of standard first-order queries they can be rewritten to.

AIJ Journal 2021 Journal Article

First-order rewritability of ontology-mediated queries in linear temporal logic

• Alessandro Artale
• Roman Kontchakov
• Alisa Kovtunova
• Vladislav Ryzhikov
• Frank Wolter
• Michael Zakharyaschev

We investigate ontology-based data access to temporal data. We consider temporal ontologies given in linear temporal logic LTL interpreted over discrete time ( Z, < ). Queries are given in LTL or MFO ( < ), monadic first-order logic with a built-in linear order. Our concern is first-order rewritability of ontology-mediated queries (OMQs) consisting of a temporal ontology and a query. By taking account of the temporal operators used in the ontology and distinguishing between ontologies given in full LTL and its core, Krom and Horn fragments, we identify a hierarchy of OMQs with atomic queries by proving rewritability into either FO ( < ), first-order logic with the built-in linear order, or FO ( <, ≡ ), which extends FO ( < ) with the standard arithmetic predicates x ≡ 0 ( mod n ), for any fixed n > 1, or FO ( RPR ), which extends FO ( < ) with relational primitive recursion. In terms of circuit complexity, FO ( <, ≡ ) - and FO ( RPR ) -rewritability guarantee OMQ answering in uniform Image 1 and, respectively, Image 2. We obtain similar hierarchies for more expressive types of queries: positive LTL-formulas, monotone MFO ( < ) - and arbitrary MFO ( < ) -formulas. Our results are directly applicable if the temporal data to be accessed is one-dimensional; moreover, they lay foundations for investigating ontology-based access using combinations of temporal and description logics over two-dimensional temporal data.

AAAI Conference 2021 Conference Paper

Living Without Beth and Craig: Definitions and Interpolants in Description Logics with Nominals and Role Inclusions

• Alessandro Artale
• Jean Christoph Jung
• Andrea Mazzullo
• Ana Ozaki
• Frank Wolter

The Craig interpolation property (CIP) states that an interpolant for an implication exists iff it is valid. The projective Beth definability property (PBDP) states that an explicit definition exists iff a formula stating implicit definability is valid. Thus, the CIP and PBDP transform potentially hard existence problems into deduction problems in the underlying logic. Description Logics with nominals and/or role inclusions do not enjoy the CIP nor PBDP, but interpolants and explicit definitions have many potential applications in ontology engineering and ontology-based data management. In this article we show the following: even without Craig and Beth, the existence of interpolants and explicit definitions is decidable in description logics with nominals and/or role inclusions such as ALCO, ALCH and ALCHIO. However, living without Craig and Beth makes this problem harder than deduction: we prove that the existence problems become 2EXPTIMEcomplete, thus one exponential harder than validity. The existence of explicit definitions is 2EXPTIME-hard even if one asks for a definition of a nominal using any symbol distinct from that nominal, but it becomes EXPTIME-complete if one asks for a definition of a concept name using any symbol distinct from that concept name.

KR Conference 2021 Conference Paper

On Free Description Logics with Definite Descriptions

• Alessandro Artale
• Andrea Mazzullo
• Ana Ozaki
• Frank Wolter

Definite descriptions are phrases of the form ‘the x such that φ’, used to refer to single entities in a context. They are often more meaningful to users than individual names alone, in particular when modelling or querying data over ontologies. We investigate free description logics with both individual names and definite descriptions as terms of the language, while also accounting for their possible lack of denotation. We focus on the extensions of ALC and, respectively, EL with nominals, the universal role, and definite descriptions. We show that standard reasoning in these extensions is not harder than in the original languages, and we characterise the expressive power of concepts relative to first-order formulas using a suitable notion of bisimulation. Moreover, we lay the foundations for automated support for definite descriptions generation by studying the complexity of deciding the existence of definite descriptions for an individual under an ontology. Finally, we provide a polynomial-time reduction of reasoning in other free description logic languages based on dual-domain semantics to the case of partial interpretations.

IJCAI Conference 2019 Conference Paper

Do You Need Infinite Time?

• Alessandro Artale
• Andrea Mazzullo
• Ana Ozaki

Linear temporal logic over finite traces is used as a formalism for temporal specification in automated planning, process modelling and (runtime) verification. In this paper, we investigate first-order temporal logic over finite traces, lifting some known results to a more expressive setting. Satisfiability in the two-variable monodic fragment is shown to be EXPSPACE-complete, as for the infinite trace case, while it decreases to NEXPTIME when we consider finite traces bounded in the number of instants. This leads to new complexity results for temporal description logics over finite traces. We further investigate satisfiability and equivalences of formulas under a model-theoretic perspective, providing a set of semantic conditions that characterise when the distinction between reasoning over finite and infinite traces can be blurred. Finally, we apply these conditions to planning and verification.

TIME Conference 2017 Conference Paper

Ontology-Mediated Query Answering over Temporal Data: A Survey (Invited Talk)

• Alessandro Artale
• Roman Kontchakov
• Alisa Kovtunova
• Vladislav Ryzhikov
• Frank Wolter
• Michael Zakharyaschev

We discuss the use of various temporal knowledge representation formalisms for ontology-mediated query answering over temporal data. In particular, we analyse ontology and query languages based on the linear temporal logic LTL, the multi-dimensional Halpern-Shoham interval temporal logic HS_n, as well as the metric temporal logic MTL. Our main focus is on the data complexity of answering temporal ontology-mediated queries and their rewritability into standard first-order and datalog queries.

IJCAI Conference 2015 Conference Paper

First-Order Rewritability of Temporal Ontology-Mediated Queries

• Alessandro Artale
• Roman Kontchakov
• Alisa Kovtunova
• Vladislav Ryzhikov
• Frank Wolter
• Michael Zakharyaschev

Aiming at ontology-based data access over temporal, in particular streaming data, we design a language of ontology-mediated queries by extending OWL 2 QL and SPARQL with temporal operators, and investigate rewritability of these queries into two-sorted first-order logic with < and PLUS over time.

AAAI Conference 2015 Conference Paper

Tractable Interval Temporal Propositional and Description Logics

• Alessandro Artale
• Roman Kontchakov
• Vladislav Ryzhikov
• Michael Zakharyaschev

We design a tractable Horn fragment of the Halpern-Shoham temporal logic and extend it to interval-based temporal description logics, instance checking in which is P-complete for both combined and data complexity.

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.

IJCAI Conference 2013 Conference Paper

Temporal Description Logic for Ontology-Based Data Access

• Alessandro Artale
• Roman Kontchakov
• Frank Wolter
• Michael Zakharyaschev

Our aim is to investigate ontology-based data access over temporal data with validity time and ontologies capable of temporal conceptual modelling. To this end, we design a temporal description logic, TQL, that extends the standard ontology language OWL 2 QL, provides basic means for temporal conceptual modelling and ensures firstorder rewritability of conjunctive queries for suitably defined data instances with validity time.

LPAR Conference 2013 Conference Paper

The Complexity of Clausal Fragments of LTL

• Alessandro Artale
• Roman Kontchakov
• Vladislav Ryzhikov
• Michael Zakharyaschev

Abstract We introduce and investigate a number of fragments of propositional temporal logic LTL over the flow of time (ℤ, <). The fragments are defined in terms of the available temporal operators and the structure of the clausal normal form of the temporal formulas. We determine the computational complexity of the satisfiability problem for each of the fragments, which ranges from NLogSpace to PTime, NP and PSpace.

ECAI Conference 2012 Conference Paper

DL-Lite with Attributes and Datatypes

• Alessandro Artale
• Vladislav Ryzhikov
• Roman Kontchakov

We extend the DL-Lite languages by means of attributes and datatypes. Attributes-a notion borrowed from data models- associate concrete values from datatypes to abstract objects and in this way complement roles, which describe relationships between abstract objects. The extended languages remain tractable (with a notable exception) even though they contain both existential and (a limited form of) universal quantification. We present complexity results for two most important reasoning problems in DL-Lite: combined complexity of knowledge base satisfiability and data complexity of positive existential query answering.

AAAI Conference 2010 Conference Paper

Past and Future of DL-Lite

• Alessandro Artale
• Roman Kontchakov
• Vladislav Ryzhikov
• Michael Zakharyaschev

We design minimal temporal description logics that are capable of expressing various aspects of temporal conceptual data models and investigate their computational complexity. We show that, depending on the required types of temporal and atemporal constraints, the satisfiability problem for temporal knowledge bases in the resulting logics can be NLOGSPACE-, NP- and PSPACE-complete, as well as undecidable.

KR Conference 2008 Conference Paper

Formalising Temporal Constraints on Part-Whole Relations

• Alessandro Artale
• Nicola Guarino
• C. Maria Keet

Representing part-whole relations and effectively using them in domain ontologies and conceptual data models poses multiple challenges. In this paper we face the issue of imposing temporal constraints on part-whole relationships, introducing a way to account for "essential" and "immutable" parts (and wholes) in addition to the usual "mandatory" parts (and wholes). Our approach is based on i) an explicit temporalization of the part-whole relation, which allows us to introduce a novel notion of "status" for part-whole relationships; ii) an explicit account of the ontological nature of the classes involved in a part-whole relationships, which distinguishes between "rigid" and "anti-rigid" classes. The main novelty in this paper is to resort to a temporal logic approach to capture the above mentioned notions. The formalization proposed here is grounded on the temporal description logic DLRUS and is based on previous successful efforts to formalize temporal conceptual models.

IJCAI Conference 2007 Conference Paper

• Alessandro Artale
• Carsten Lutz
• David Toman

We combine the modal logic S5 with the description logic (DL) ALCQI. The resulting multi-dimensional DL ALCQI_S5 supports reasoning about change by allowing to express that concepts and roles change over time. It cannot, however, discriminate between changes in the past and in the future. Our main technical result is that satisfiability of ALCQI_S5 concepts with respect to general TBoxes (including GCIs) is decidable and 2-ExpTime-complete. In contrast, reasoning in temporal DLs that are able to discriminate between past and future is inherently undecidable. We argue that our logic is sufficient for reasoning about temporal conceptual models with time-stamping constraints.

AAAI Conference 2007 Conference Paper

DL-Lite in the Light of First-Order Logic

• Alessandro Artale
• Roman Kontchakov

The use of ontologies in various application domains, such as Data Integration, the Semantic Web, or ontology-based data management, where ontologies provide the access to large amounts of data, is posing challenging requirements w. r. t. a trade-off between expressive power of a DL and efficiency of reasoning. The logics of the DL-Lite family were specifically designed to meet such requirements and optimized w. r. t. the data complexity of answering complex types of queries. In this paper we propose DL-Litebool, an extension of DL- Lite with full Booleans and number restrictions, and study the complexity of reasoning in DL-Litebool and its significant sub-logics. We obtain our results, together with useful insights into the properties of the studied logics, by a novel reduction to the one-variable fragment of first-order logic. We study the computational complexity of satisfiability and subsumption, and the data complexity of answering positive existential queries (which extend unions of conjunctive queries). Notably, we extend the LOGSPACE upper bound for the data complexity of answering unions of conjunctive queries in DL-Lite to positive queries and to the possibility of expressing also number restrictions, and hence local functionality in the TBox.

TIME Conference 2007 Conference Paper

Temporalising Tractable Description Logics

• Alessandro Artale
• Roman Kontchakov
• Carsten Lutz
• Frank Wolter
• Michael Zakharyaschev

It is known that for temporal languages, such as first-order LTL, reasoning about constant (time-independent) relations is almost always undecidable. This applies to temporal description logics as well: constant binary relations together with general concept subsumptions in combinations of LTL and the basic description logic ALC cause undecidability. In this paper, we explore temporal extensions of two recently introduced families of 'weak' description logics known as DL-Lite and EL. Our results are twofold: temporalisations of even rather expressive variants of DL-Lite turn out to be decidable, while the temporalisation of EL with general concept subsumptions and constant relations is undecidable.

TIME Conference 2004 Conference Paper

Reasoning on Temporal Conceptual Schemas with Dynamic Constraints

• Alessandro Artale

This paper formally clarifies the relevant reasoning problems for temporal EER diagrams. We distinguish between the following reasoning services: (a) entity, relationship and schema satisfiability; (b) liveness and global satisfiability for both entities and relationships; (c) subsumption for either entities or relationships; and (d) logical implication between schemas. We then show that reasoning on temporal models is an undecidable problem as soon as the schema language is able to distinguish between temporal and atemporal constructs, and it has the ability to represent dynamic constraints between entities.

JELIA Conference 2002 Conference Paper

A Temporal Description Logic for Reasoning over Conceptual Schemas and Queries

• Alessandro Artale
• Enrico Franconi
• Frank Wolter
• Michael Zakharyaschev

Abstract This paper introduces a new logical formalism, intended for temporal conceptual modelling, as a natural combination of the well-known description logic \( \mathcal{D}\mathcal{L}\mathcal{R} \) and point-based linear temporal logic with Since and Until. We define a query language (where queries are non-recursive Datalog programs and atoms are complex \( \mathcal{D}\mathcal{L}\mathcal{R}_{\mathcal{U}\mathcal{S}} \) expressions) and investigate the problem of checking query containment under the constraints defined by \( \mathcal{D}\mathcal{L}\mathcal{R}_{\mathcal{U}\mathcal{S}} \) conceptual schemas—i. e. , \( \mathcal{D}\mathcal{L}\mathcal{R}_{\mathcal{U}\mathcal{S}} \) knowledge bases—as well as the problems of schema satisfiability and logical implication.

TIME Conference 1999 Invited Paper

Introducing Temporal Description Logics

• Alessandro Artale
• Enrico Franconi

Description logics are formalisms designed for a logical reconstruction of representation tools such as frames, object oriented and semantic data models, semantic networks, type systems, and feature logics. Nowadays, description logics are also considered the most important unifying formalism for the many object centred representation languages used in areas other than knowledge representation. Important characteristics of description logics are high expressivity, together with decidability, which guarantee that reasoning algorithms always terminate with the correct answers. The article introduces temporal extensions of description logics, through the detailed analysis of a case study, involving the combination of a rather expressive description logic with the basic tense modal logic over a linear, unbounded, and discrete temporal structure. ALCQIT is the temporal description logic considered as the case study. This language is obtained by combining a standard tense logic and the non temporal description logic ALCQI with axioms. We first introduce the non temporal part of the language, and then we present its combination with the tense logic. Finally, we briefly report on how other approaches in extending description logics with time relate to the case study.