TY  - JOUR
A1  - Orejas, Fernando
A1  - Pino, Elvira
A1  - Navarro, Marisa
A1  - Lambers, Leen
T1  - Institutions for navigational logics for graphical structures
JF  - Theoretical computer science
N2  - We show that a Navigational Logic, i.e., a logic to express properties about graphs and about paths in graphs is a semi-exact institution. In this way, we can use a number of operations to structure and modularize our specifications. Moreover, using the properties of our institution, we also show how to structure single formulas, which in our formalism could be quite complex.
KW  - Institutions
KW  - Graph logics
KW  - Navigational logics
Y1  - 2018
U6  - https://doi.org/10.1016/j.tcs.2018.02.031
SN  - 0304-3975
SN  - 1879-2294
VL  - 741
SP  - 19
EP  - 24
PB  - Elsevier
CY  - Amsterdam
ER  - 
TY  - JOUR
A1  - Schneider, Sven
A1  - Lambers, Leen
A1  - Orejas, Fernando
T1  - Automated reasoning for attributed graph properties
JF  - International Journal on Software Tools for Technology Transfer
N2  - Graphs are ubiquitous in computer science. Moreover, in various application fields, graphs are equipped with attributes to express additional information such as names of entities or weights of relationships. Due to the pervasiveness of attributed graphs, it is highly important to have the means to express properties on attributed graphs to strengthen modeling capabilities and to enable analysis. Firstly, we introduce a new logic of attributed graph properties, where the graph part and attribution part are neatly separated. The graph part is equivalent to first-order logic on graphs as introduced by Courcelle. It employs graph morphisms to allow the specification of complex graph patterns. The attribution part is added to this graph part by reverting to the symbolic approach to graph attribution, where attributes are represented symbolically by variables whose possible values are specified by a set of constraints making use of algebraic specifications. Secondly, we extend our refutationally complete tableau-based reasoning method as well as our symbolic model generation approach for graph properties to attributed graph properties. Due to the new logic mentioned above, neatly separating the graph and attribution parts, and the categorical constructions employed only on a more abstract level, we can leave the graph part of the algorithms seemingly unchanged. For the integration of the attribution part into the algorithms, we use an oracle, allowing for flexible adoption of different available SMT solvers in the actual implementation. Finally, our automated reasoning approach for attributed graph properties is implemented in the tool AutoGraph integrating in particular the SMT solver Z3 for the attribute part of the properties. We motivate and illustrate our work with a particular application scenario on graph database query validation.
KW  - Attributed graphs
KW  - Nested graph conditions
KW  - Model generation
KW  - Tableau method
KW  - Graph queries
Y1  - 2018
U6  - https://doi.org/10.1007/s10009-018-0496-3
SN  - 1433-2779
SN  - 1433-2787
VL  - 20
IS  - 6
SP  - 705
EP  - 737
PB  - Springer
CY  - Heidelberg
ER  - 
TY  - JOUR
A1  - Lambers, Leen
A1  - Born, Kristopher
A1  - Kosiol, Jens
A1  - Strüber, Daniel
A1  - Taentzer, Gabriele
T1  - Granularity of conflicts and dependencies in graph transformation systems
BT  - a two-dimensional approach
JF  - Journal of Logical and Algebraic Methods in Programming
N2  - Conflict and dependency analysis (CDA) is a static analysis for the detection of conflicting and dependent rule applications in a graph transformation system. The state-of-the-art CDA technique, critical pair analysis, provides all potential conflicts and dependencies in minimal context as critical pairs, for each pair of rules. Yet, critical pairs can be hard to understand; users are mainly interested in core information about conflicts and dependencies occurring in various combinations. In this paper, we present an approach to conflicts and dependencies in graph transformation systems based on two dimensions of granularity. The first dimension refers to the overlap considered between the rules of a given rule pair; the second one refers to the represented amount of context information about transformations in which the conflicts occur. We introduce a variety of new conflict notions, in particular, conflict atoms, conflict reasons, and minimal conflict reasons, relate them to the existing conflict notions of critical pairs and initial conflicts, and position all of these notions within our granularity approach. Finally, we introduce dual concepts for dependency analysis. As we discuss in a running example, our approach paves the way for an improved CDA technique. (C) 2018 Elsevier Inc. All rights reserved.
KW  - Graph transformation (double pushout approach)
KW  - Parallel independence
KW  - Critical pair analysis (CPA)
Y1  - 2018
U6  - https://doi.org/10.1016/j.jlamp.2018.11.004
SN  - 2352-2208
VL  - 103
SP  - 105
EP  - 129
PB  - Elsevier
CY  - New York
ER  -