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

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

In the context of verification of data-aware processes, a formal approach based on satisfiability modulo theories (SMT) has been considered to verify parameterised safety properties. This approach requires a combination of model-theoretic notions and algorithmic techniques based on backward reachability. We introduce here Ontology-Based Processes, which are a variant of one of the most investigated models in this spectrum, namely simple artifact systems (SASs), where, instead of managing a database, we operate over a description logic (DL) ontology. We prove that when the DL is expressed in (a slight extension of) RDFS, it enjoys suitable model-theoretic properties, and that by relying on such DL we can define Ontology-Based Processes to which backward reachability can still be applied. Relying on these results we are able to show that in this novel setting, verification of safety properties is decidable in PSPACE.

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.

Abstract We study the complexity of the validity/derivability problem for combinations of non-normal modal logics in the form of logic fusions, possibly extended with simple interaction axioms. We first present cut-free sequent calculi for these logic combinations. Then, we introduce hypersequent calculi with invertible rules, and show that they allow for a coNP proof search procedure. In the last part of the paper, we consider the case of combinations of logics sharing a universal modality. Using the hypersequent calculi, we show that these logics remain coNP-complete, and also provide an equivalent axiomatisation for them.

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.

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 the complexity of learning query inseparable εℒℋ ontologies in a variant of Angluin's exact learning model. Given a fixed data instance A* and a query language

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.