Towards a navigational logic for graphical structures.

*(English)*Zbl 1383.68064
Heckel, Reiko (ed.) et al., Graph transformation, specifications, and nets. In memory of Hartmut Ehrig. Cham: Springer (ISBN 978-3-319-75395-9/pbk; 978-3-319-75396-6/ebook). Lecture Notes in Computer Science 10800, 124-141 (2018).

Summary: One of the main advantages of the Logic of Nested Conditions, defined by Habel and Pennemann, for reasoning about graphs, is its generality: this logic can be used in the framework of many classes of graphs and graphical structures. It is enough that the category of these structures satisfies certain basic conditions.

In a previous paper [“A logic of graph conditions extended with paths”, in: Proceedings of the 7th international workshop on graph computation models, GCM 2016, Vienna, Austria, 4 July 2016. Electronic pre-proceedings. 1–15 (2016), http://gcm2016.inf.uni-due.de/papers/navarro-orejas-pino-lambers.pdf], we extended this logic to be able to deal with graph properties including paths, but this extension was only defined for the category of untyped directed graphs. In addition it seemed difficult to talk about paths abstractly, that is, independently of the given category of graphical structures. In this paper we approach this problem. In particular, given an arbitrary category of graphical structures, we assume that for every object of this category there is an associated edge relation that can be used to define a path relation. Moreover, we consider that edges have some kind of labels and paths can be specified by associating them to a set of label sequences. Then, after the presentation of that general framework, we show how it can be applied to several classes of graphs. Moreover, we present a set of sound inference rules for reasoning in the logic.

For the entire collection see [Zbl 1383.68006].

In a previous paper [“A logic of graph conditions extended with paths”, in: Proceedings of the 7th international workshop on graph computation models, GCM 2016, Vienna, Austria, 4 July 2016. Electronic pre-proceedings. 1–15 (2016), http://gcm2016.inf.uni-due.de/papers/navarro-orejas-pino-lambers.pdf], we extended this logic to be able to deal with graph properties including paths, but this extension was only defined for the category of untyped directed graphs. In addition it seemed difficult to talk about paths abstractly, that is, independently of the given category of graphical structures. In this paper we approach this problem. In particular, given an arbitrary category of graphical structures, we assume that for every object of this category there is an associated edge relation that can be used to define a path relation. Moreover, we consider that edges have some kind of labels and paths can be specified by associating them to a set of label sequences. Then, after the presentation of that general framework, we show how it can be applied to several classes of graphs. Moreover, we present a set of sound inference rules for reasoning in the logic.

For the entire collection see [Zbl 1383.68006].