Graph databases are now playing an important role because they allow us to overcome some limitations of relational databases. In particular, in graph databases we are interested not only on the data contained but also on its topology. As a consequence, most graph database queries are navigational, asking whether some nodes are connected by edges or paths. Up to now, most foundational work has concentrated on the study of computational models and query languages, analyzing their expressivity, computability, and complexity. However, in our work we address a different kind of foundational work. We are not concerned with expressibility, efficiency or feasibility issues, but with correctness. More precisely, given an algorithm or an implementation for solving queries, how can we be sure that the answers obtained are correct (soundness) and that all possible correct answers are obtained by our implementation (completeness). In this sense, in this paper we first present a core query language, similar to Cypher or G-Core. Then, we define a simple logic whose formulas are precisely the database queries, and whose satisfaction relation defines what is a correct answer. Finally, we define an operational semantics, which could be seen as an abstract implementation of our language, showing that the semantics is correct, i.e. sound and complete with respect to our logic.

In the context of software model-driven development, artifacts are specified by several models describing different aspects, e.g., different views, dynamic behavior, structure, distributed information, etc. Then, maintaining and repairing consistency of the whole specification are crucial issues if the models can be separately developed and updated. Model Synchronization is the process of restoring consistency after the update of one or several of the models. In the present work, we approach the case when conflicts may arise due to concurrently updating different models. Specifically, based on the Triple Graph Grammar approach, we propose an incremental algorithm $$\mathtt{CSynch}$$ for solving conflicts and repairing consistency. In addition, we identify and formalize when a synchronizing solution can be considered adequate and show that our procedure $$\mathtt{CSynch}$$ is sound and complete.

The aim of this paper is to present a generic framework for the modelling of componentbased systems using architectural connectors. More precisely, concepts of component, connector and architecture are presented in a formal generic way, which are independent of any semi-formal or formal modelling approach. The idea is that one could use this framework to define component and connector notions for every given modelling formalism. As a main result, we define the semantics of architectures using graph transformation, showing that the semantics is independent of the order in which the connections are computed, and that the semantics is compatible with transformation. In the continuation of this paper, we show the applicability of our ideas. In particular, our framework is instantiated by Petri nets and CSP, including a case study using Petri Nets.

The aim of this paper is to show how the generic approach to connector architectures, presented in the first part of this work, can be applied to a given modeling formalism to define architectural component and connector notions associated to that formalism. Starting with a review of the generic approach, in this second part of the paper we consider two modeling formalisms: elementary Petri nets and CSP. As main results we show that both cases satisfy the axioms of our component framework, so that the results concerning the semantics of architectures can be applied. Moreover, a small case study in terms of Petri Nets is presented in order to show how the results can be applied to a connector architecture based on Petri nets.