Modeling and verification of dynamic systems operating over a relational representation of states are increasingly investigated problems in AI, Business Process Management, and Database Theory. To make these systems amenable to verification, the amount of information stored in each relational state needs to be bounded, or restrictions are imposed on the preconditions and effects of actions. We introduce the general framework of relational action bases (RABs), which generalizes existing models by lifting both these restrictions: unbounded relational states can be evolved through actions that can quantify both existentially and universally over the data, and that can exploit numerical datatypes with arithmetic predicates. We then study parameterized safety of RABs via (approximated) SMT-based backward search, singling out essential meta-properties of the resulting procedure, and showing how it can be realized by an off-the-shelf combination of existing verification modules of the state-of-the-art MCMT model checker. We demonstrate the effectiveness of this approach on a benchmark of data-aware business processes. Finally, we show how universal invariants can be exploited to make this procedure fully correct.

In order to meet usability requirements, most logic-based applications provide explanation facilities for reasoning services. This holds also for DLs, where research has focused on the explanation of both TBox reasoning and, more recently, query answering. Besides explaining the presence of a tuple in a query answer, it is important to explain also why a given tuple is missing. We address the latter problem for (conjunctive) query answering over DL-Lite ontologies, by adopting abductive reasoning, that is, we look for additions to the ABox that force a given tuple to be in the result. As reasoning taskswe consider existence and recognition of an explanation, and relevance and necessity of a certain assertion for an explanation. We characterize the computational complexity of these problems for subset minimal and cardinality minimal explanations.

In this paper we study verification of situation calculus action theories against first-order mu-calculus with quantification across situations. Specifically, we consider mu-La and mu-Lp, the two variants of mu-calculus introduced in the literature for verification of data-aware processes. The former requires that quantification ranges over objects in the current active domain, while the latter additionally requires that objects assigned to variables persist across situations. Each of these two logics has a distinct corresponding notion of bisimulation. In spite of the differences we show that the two notions of bisimulation collapse for dynamic systems that are generic, which include all those systems specified through a situation calculus action theory. Then, by exploiting this result, we show that for bounded situation calculus action theories, mu-La and mu-Lp have exactly the same expressive power. Finally, we prove decidability of verification of mu-La properties over bounded action theories, using finite faithful abstractions. Differently from the mu-Lp case, these abstractions must depend on the number of quantified variables in the mu-La formula.

In this paper, we overview the recently introduced general framework of Description Logic Based Dynamic Systems, which leverages Levesque's functional approach to model systems that evolve the extensional part of a description logic knowledge base by means of actions. This framework is parametric w.r.t. the adopted description logic and the progression mechanism. In this setting, we discuss verification and adversarial synthesis for specifications expressed in a variant of first-order mu-calculus, with a controlled form of quantification across successive states, and present key decidability results under the natural assumption of state-boundedness.

We study the data complexity of answering conjunctive queries over Description Logic knowledge bases constituted by a TBox and an ABox. In particular, we are interested in characterizing the FO- rewritability and the polynomial tractability boundaries of conjunctive query answering, depending on the expressive power of the DL used to express the knowledge base. What emerges from our complexity analysis is that the Description Logics of the DL-Lite family are essentially the maximal logics allowing for conjunctive query answering through standard database technology.

In this paper we investigate situation calculus action theories extended with ontologies, expressed as description logics TBoxes that act as state constraints. We show that this combination, while natural and desirable, is particularly problematic: it leads to undecidability of the simplest form of reasoning, namely satisfiability, even for the simplest kinds of description logics and the simplest kind of situation calculus action theories.

In the context of verification of data-aware processes (DAPs), a formal approach based on satisfiability modulo theories (SMT) has been considered to verify parameterised safety properties of so-called artifact-centric systems. This approach requires a combination of model-theoretic notions and algorithmic techniques based on backward reachability. We introduce here 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 expressed in (a slight extension of) RDFS. This DL, enjoying suitable model-theoretic properties, allows us to define DL-based SASs to which backward reachability can still be applied, leading to decidability in PSPACE of the corresponding safety problems.

Virtual Knowledge Graphs (VKG) constitute one of the most promising paradigms for integrating and accessing legacy data sources. A critical bottleneck in the integration process involves the definition, validation, and maintenance of mappings that link data sources to a domain ontology. To support the management of mappings throughout their entire lifecycle, we propose a comprehensive catalog of sophisticated mapping patterns that emerge when linking databases to ontologies. To do so, we build on well-established methodologies and patterns studied in data management, data analysis, and conceptual modeling. These are extended and refined through the analysis of concrete VKG benchmarks and real-world use cases, and considering the inherent impedance mismatch between data sources and ontologies. We validate our catalog on the considered VKG scenarios, showing that it covers the vast majority of patterns present therein.

We study query answering in the description logic $\mathcal{SQ}$ supporting qualified number restrictions on both transitive and non-transitive roles. Our main contributions are a tree-like model property for $\mathcal{SQ}$ knowledge bases and, building upon this, an optimal automata-based algorithm for answering positive existential regular path queries in 2ExpTime.

Ontology-based data access (OBDA) is a popular paradigm for querying heterogeneous data sources by connecting them through mappings to an ontology. In OBDA, it is often difficult to reconstruct why a tuple occurs in the answer of a query. We address this challenge by enriching OBDA with provenance semirings, taking inspiration from database theory. In particular, we investigate the problems of (i) deciding whether a provenance annotated OBDA instance entails a provenance annotated conjunctive query, and (ii) computing a polynomial representing the provenance of a query entailed by a provenance annotated OBDA instance. Differently from pure databases, in our case these polynomials may be infinite. To regain finiteness, we consider idempotent semirings, and study the complexity in the case of DL-Lite ontologies. We implement Task (ii) in a state-of-the-art OBDA system and show the practical feasibility of the approach through an extensive evaluation against two popular benchmarks.