Towards a Navigational Logic for Graphical Structures

  • Leen Lambers
  • Marisa Navarro
  • Fernando Orejas
  • Elvira PinoEmail author
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10800)


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 [14], 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. 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),
  2. 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).
  3. 3.
    Courcelle, B.: The expression of graph properties and graph transformations in monadic second-order logic. In: Rozenberg, G. (ed.) Handbook of Graph Grammars, pp. 313–400. World Scientific, River Edge (1997). Google Scholar
  4. 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).
  5. 5.
    Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Springer, Heidelberg (2006)zbMATHGoogle Scholar
  6. 6.
    Ehrig, H., Habel, A.: Graph grammars with application conditions. In: Rozenberg, G., Salomaa, A. (eds.) The Book of L, pp. 87–100. Springer, Heidelberg (1986)CrossRefGoogle Scholar
  7. 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).
  8. 8.
    Habel, A., Heckel, R., Taentzer, G.: Graph grammars with negative application conditions. Fundamenta Informaticae 26, 287–313 (1996). MathSciNetzbMATHGoogle Scholar
  9. 9.
    Habel, A., Pennemann, K.H.: Correctness of high-level transformation systems relative to nested conditions. Math. Struct. Comput. Sci. 19(2), 245–296 (2009). MathSciNetCrossRefzbMATHGoogle Scholar
  10. 10.
    Habel, A., Radke, H.: Expressiveness of graph conditions with variables. ECEASST, 30 (2010)
  11. 11.
    Heckel, R., Wagner, A.: Ensuring consistency of conditional graph rewriting - a constructive approach. Electr. Notes Theor. Comput. Sci. 2, 118–126 (1995). CrossRefzbMATHGoogle Scholar
  12. 12.
    Lambers, L., Orejas, F.: Tableau-Based Reasoning for Graph Properties. In: Giese, H., König, B. (eds.) ICGT 2014. LNCS, vol. 8571, pp. 17–32. Springer, Cham (2014). Google Scholar
  13. 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).
  14. 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
  15. 15.
    Orejas, F.: Attributed graph constraints. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 274–288. Springer, Heidelberg (2008). CrossRefGoogle Scholar
  16. 16.
    Orejas, F.: Symbolic graphs for attributed graph constraints. J. Symb. Comput. 46(3), 294–315 (2011). MathSciNetCrossRefzbMATHGoogle Scholar
  17. 17.
    Orejas, F., Ehrig, H., Prange, U.: Reasoning with graph constraints. Formal Asp. Comput. 22(3–4), 385–422 (2010). CrossRefzbMATHGoogle Scholar
  18. 18.
    Pennemann, K.-H.: Resolution-like theorem proving for high-level conditions. In: Ehrig, H., Heckel, R., Rozenberg, G., Taentzer, G. (eds.) ICGT 2008. LNCS, vol. 5214, pp. 289–304. Springer, Heidelberg (2008). CrossRefGoogle Scholar
  19. 19.
    Pennemann, K.H.: Development of Correct Graph Transformation Systems, PhD Thesis. Department of Computing Science, University of Oldenburg (2009)Google Scholar
  20. 20.
    Poskitt, C.M., Plump, D.: Verifying monadic second-order properties of graph programs. In: Giese, H., König, B. (eds.) ICGT 2014. LNCS, vol. 8571, pp. 33–48. Springer, Cham (2014). Google Scholar
  21. 21.
    Rensink, A.: Representing first-order logic using graphs. In: Ehrig, H., Engels, G., Parisi-Presicce, F., Rozenberg, G. (eds.) ICGT 2004. LNCS, vol. 3256, pp. 319–335. Springer, Heidelberg (2004). CrossRefGoogle Scholar
  22. 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
  23. 23.
    Wood, P.T.: Query languages for graph databases. SIGMOD Rec. 41(1), 50–60 (2012). CrossRefGoogle Scholar

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Hasso Plattner Institut, University of PotsdamPotsdamGermany
  2. 2.Universidad del País Vasco (UPV/EHU)San SebastiánSpain
  3. 3.Universitat Politècnica de CatalunyaBarcelonaSpain

Personalised recommendations