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

Our concern is the data complexity of answering linear monadic datalog queries whose atoms in the rule bodies can be prefixed by operators of linear temporal logic LTL. We first observe that, for data complexity, answering any connected query with operators ○/○- (at the next/previous moment) is either in AC⁰, or in ACC⁰\AC⁰, or NC¹-complete, or L-hard and in NL. Then we show that the problem of deciding L-hardness of answering such queries is PSpace-complete, while checking membership in the classes AC⁰ and ACC⁰ as well as NC¹-completeness can be done in ExpSpace. Finally, we prove that membership in AC⁰ or in ACC⁰, NC¹-completeness, and L-hardness are undecidable for queries with operators ◇/◇- (sometime in the future/past) provided that NC¹ ≠ NL and L ≠ NL.

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.

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.

Formalisms based on temporal logics interpreted over finite strict linear orders, known in the literature as finite traces , have been used for temporal specification in automated planning, process modelling, (runtime) verification and synthesis of programs, as well as in knowledge representation and reasoning. In this article, we focus on first-order temporal logic on finite traces . We first investigate preservation of equivalences and satisfiability of formulas between finite and infinite traces, by providing a set of semantic and syntactic conditions to guarantee when the distinction between reasoning in the two cases can be blurred. Moreover, we show that the satisfiability problem on finite traces for several decidable fragments of first-order temporal logic is ExpSpace -complete, as in the infinite trace case, while it decreases to NExpTime when finite traces bounded in the number of instants are considered. This leads also to new complexity results for temporal description logics over finite traces. Finally, we investigate applications to planning and verification, in particular by establishing connections with the notions of insensitivity to infiniteness and safety from the literature.

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

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

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 reduce potentially hard existence problems to entailment in the underlying logic. Description (and modal) logics with nominals and/or role inclusions do not enjoy the CIP nor the PBDP, but interpolants and explicit definitions have many applications, in particular in concept learning, ontology engineering, and ontology-based data management. In this article, we show that, even without Beth and Craig, the existence of interpolants and explicit definitions is decidable in description logics with nominals and/or role inclusions such as 𝒜ℒ𝒞𝒪, 𝒜ℒ𝒞ℋ, and 𝒜ℒ𝒞ℋ𝒪ℐ and corresponding hybrid modal logics. However, living without Beth and Craig makes these problems harder than entailment: the existence problems become 2ExpTime -complete in the presence of an ontology or the universal modality, and coNExpTime -complete otherwise. We also analyze explicit definition existence if all symbols (except the one that is defined) are admitted in the definition. In this case, the complexity depends on whether one considers individual or concept names. Finally, we consider the problem of computing interpolants and explicit definitions if they exist and turn the complexity upper bound proof into an algorithm computing them, at least for description logics with role inclusions.

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.

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,<). Our main concern is first-order rewritability of ontology-mediated queries (OMQs) that consist of a 2D ontology and a positive temporal instance query. Our target languages for FO-rewritings are two-sorted FO(<) -- first-order logic with sorts for time instants ordered by the built-in precedence relation < and for the domain of individuals---its extension FO(<, ≡) with the standard congruence predicates t ≡ 0 (mod n), for any fixed n > 1, and FO(RPR) that admits relational primitive recursion. In terms of circuit complexity, FO(<, ≡)- and FO(RPR)-rewritability guarantee answering OMQs in uniform AC0 and NC1, 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.

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 2EXPTIME-complete, 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.

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.

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 and, respectively, . 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.

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.

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.

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.

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

We design temporal description logics (TDLs) suitable for reasoning about temporal conceptual data models and investigate their computational complexity. Our formalisms are based onDL-Litelogics with three types of concept inclusions (ranging from atomic concept inclusions and disjointness to the full Booleans), as well as cardinality constraints and role inclusions. The logics are interpreted over the Cartesian products of object domains and the flow of time (ℤ, <), satisfying the constant domain assumption. Concept and role inclusions of the TBox hold at all moments of time (globally), and data assertions of the ABox hold at specified moments of time. To express temporal constraints of conceptual data models, the languages are equipped with flexible and rigid roles, standard future and past temporal operators on concepts, and operators “always” and “sometime” on roles. The most expressive of our TDLs (which can capture lifespan cardinalities and either qualitative or quantitative evolution constraints) turns out to be undecidable. However, by omitting some of the temporal operators on concepts/roles or by restricting the form of concept inclusions, we construct logics whose complexity ranges between NLogSpaceand PSpace. These positive results are obtained by reduction to various clausal fragments of propositional temporal logic, which opens a way to employ propositional or first-order temporal provers for reasoning about temporal data models.

We design minimal temporal description logics that are capa- ble 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.

Relation Based Access Control (RelBAC) is an access control model that places permissions as first class concepts. Under this model, we discuss in this paper how to formalize typical access control policies with Description Logics. Important security properties, i.e., Separation of Duties (SoD) and Chinese Wall are studied and formally represented in RelBAC. To meet the needs of automated tools for administrators, we show that RelBAC can formalize and answer queries about access control requests and administrative checks resorting to the reasoning services of the underlying Description Logic.

The recently introduced series of description logics under the common moniker `DL-Lite' has attracted attention of the description logic and semantic web communities due to the low computational complexity of inference, on the one hand, and the ability to represent conceptual modeling formalisms, on the other. The main aim of this article is to carry out a thorough and systematic investigation of inference in extensions of the original DL-Lite logics along five axes: by (i) adding the Boolean connectives and (ii) number restrictions to concept constructs, (iii) allowing role hierarchies, (iv) allowing role disjointness, symmetry, asymmetry, reflexivity, irreflexivity and transitivity constraints, and (v) adopting or dropping the unique same assumption. We analyze the combined complexity of satisfiability for the resulting logics, as well as the data complexity of instance checking and answering positive existential queries. Our approach is based on embedding DL-Lite logics in suitable fragments of the one-variable first-order logic, which provides useful insights into their properties and, in particular, computational behavior.

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.

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.

1Bolzano 2Liverpool 3Liverpool 4Bolzano

A class of interval-based temporal languages for uniformly representing and reasoning about actions and plans is presented. Actions are represented by describing what is true while the action itself is occurring, and plans are constructed by temporally relating actions and world states. The temporal languages are members of the family of Description Logics, which are characterized by high expressivity combined with good computational properties. The subsumption problem for a class of temporal Description Logics is investigated and sound and complete decision procedures are given. The basic language TL-F is considered first: it is the composition of a temporal logic TL -- able to express interval temporal networks -- together with the non-temporal logic F -- a Feature Description Logic. It is proven that subsumption in this language is an NP-complete problem. Then it is shown how to reason with the more expressive languages TLU-FU and TL-ALCF. The former adds disjunction both at the temporal and non-temporal sides of the language, the latter extends the non-temporal side with set-valued features (i.e., roles) and a propositionally complete language.

We formally investigate the structural similarities and differences existing between object database models and concept languages establishing a correspondence between the two environments. Object database models deal with two kinds of data: individual objects, which have an identity, and values, which can be basic values or can have complex structures containing both basic values and objects. Concept languages only deal with individual objects. The correspondence points out the different role played by objects and values in both approaches and defines a way of properly mapping database descriptions into concept language descriptions at both a terminological and assertional level. Once the mapping is achieved, object databases can take advantage of both the algorithms and the results concerning their complexity developed in concept languages.