Towards a Navigational Logic for Graphical Structures
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 , 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.
We are grateful to the anonymous reviewers for their comments that have contributed to improve the paper.
- 1.Barceló, P.: Querying graph databases. In: Proceedings of the 32nd ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS 2013, New York, 22–27 June 2013, pp. 175–188 (2013), https://doi.org/10.1145/2463664.2465216
- 2.Barceló, P., Libkin, L., Reutter, J.L.: Querying graph patterns. In: Proceedings of the 30th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS 2011, 12–16 June 2011, Athens, pp. 199–210 (2011). https://doi.org/10.1145/1989284.1989307
- 4.Cruz, I.F., Mendelzon, A.O., Wood, P.T.: A graphical query language supporting recursion. In: Proceedings SIGMOD 1987 Annual Conference, San Francisco, 27–29 May 1987, pp. 323–330 (1987). https://doi.org/10.1145/38713.38749
- 7.Flick, N.E.: On correctness of graph programs relative to recursively nested conditions. In: Workshop on Graph Computation Models (GCM 2015), vol. 1403, pp. 97–112 (2015). http://ceur-ws.org/Vol-1403/
- 10.Habel, A., Radke, H.: Expressiveness of graph conditions with variables. ECEASST, 30 (2010) https://doi.org/10.14279/tuj.eceasst.30.404
- 13.Libkin, L., Vrgoc, D.: Regular path queries on graphs with data. In: 15th International Conference on Database Theory, ICDT 2012, Berlin, 26–29 March 2012, pp. 74–85 (2012). https://doi.org/10.1145/2274576.2274585
- 14.Navarro, M., Orejas, F., Pino, E., Lambers, L.: A logic of graph conditions extended with paths. In: Workshop on Graph Computation Models (GCM 2016), Vienna (2016)Google Scholar
- 19.Pennemann, K.H.: Development of Correct Graph Transformation Systems, PhD Thesis. Department of Computing Science, University of Oldenburg (2009)Google Scholar
- 22.Trakhtenbrot, B.A.: The impossibility of an algorithm for the decision problem on finite classes (In Russian). Doklady Akademii Nauk SSSR, 70:569–572, 1950. English translation. In: Nine Papers on Logic and Quantum Electrodynamics, AMS Transl. Ser. 2(23), 1–5 (1963)Google Scholar