Symbolic Model Generation for Graph Properties

  • Sven SchneiderEmail author
  • Leen Lambers
  • Fernando Orejas
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10202)


Graphs are ubiquitous in Computer Science. For this reason, in many areas, it is very important to have the means to express and reason about graph properties. In particular, we want to be able to check automatically if a given graph property is satisfiable. Actually, in most application scenarios it is desirable to be able to explore graphs satisfying the graph property if they exist or even to get a complete and compact overview of the graphs satisfying the graph property.

We show that the tableau-based reasoning method for graph properties as introduced by Lambers and Orejas paves the way for a symbolic model generation algorithm for graph properties. Graph properties are formulated in a dedicated logic making use of graphs and graph morphisms, which is equivalent to first-order logic on graphs as introduced by Courcelle. Our parallelizable algorithm gradually generates a finite set of so-called symbolic models, where each symbolic model describes a set of finite graphs (i.e., finite models) satisfying the graph property. The set of symbolic models jointly describes all finite models for the graph property (complete) and does not describe any finite graph violating the graph property (sound). Moreover, no symbolic model is already covered by another one (compact). Finally, the algorithm is able to generate from each symbolic model a minimal finite model immediately and allows for an exploration of further finite models. The algorithm is implemented in the new tool AutoGraph.


Graph properties Nested graph conditions Model generation Tableau method Satisfiability solving Graph transformation 


  1. 1.
    Bak, K., Diskin, Z., Antkiewicz, M., Czarnecki, K., Wasowski, A.: Clafer: unifying class and feature modeling. SoSyM 15(3), 811–845 (2016)Google Scholar
  2. 2.
    Baudry, B.: Testing model transformations: a case for test generation from input domain models. In: MDE4DRE (2009)Google Scholar
  3. 3.
    Beyhl, T., Blouin, D., Giese, H., Lambers, L.: On the operationalization of graph queries with generalized discrimination networks. In: [5], 170–186Google Scholar
  4. 4.
    Courcelle, B.: The expression of graph properties and graph transformations in monadic second-order logic. In: [31], 313–400Google Scholar
  5. 5.
    Echahed, R., Minas, M. (eds.): ICGT 2016. LNCS, vol. 9761. Springer, Cham (2016)Google Scholar
  6. 6.
    Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of Algebraic Graph Transformation. Springer, Heidelberg (2006)zbMATHGoogle Scholar
  7. 7.
    Ehrig, H., Golas, U., Habel, A., Lambers, L., Orejas, F.: \(\cal{M}\)-adhesive transformation systems with nested application conditions. part 2: embedding, critical pairs and local confluence. Fundam. Inform. 118(1–2), 35–63 (2012)MathSciNetzbMATHGoogle Scholar
  8. 8.
    Ehrig, H., Golas, U., Habel, A., Lambers, L., Orejas, F.: \(\cal{M}\)-adhesive transformation systems with nested application conditions. part 1: parallelism, concurrency and amalgamation. Math. Struct. Comput. Sci. 24(4) (2014)Google Scholar
  9. 9.
    Erling, O., Averbuch, A., Larriba-Pey, J., Chafi, H., Gubichev, A., Prat-Pérez, A., Pham, M., Boncz, P.A.: The LDBC social network benchmark: interactive workload. In: Proceedings of the 2015 ACM SIGMOD International Conference on Management of Data, pp. 619–630. ACM (2015)Google Scholar
  10. 10.
    Gogolla, M., Hilken, F.: Model validation and verification options in a contemporary UML and OCL analysis tool. In: Modellierung 2016. LNI, vol. 254, pp. 205–220. GI (2016)Google Scholar
  11. 11.
    González, C.A., Cabot, J.: Test data generation for model transformations combining partition and constraint analysis. In: Ruscio, D., Varró, D. (eds.) ICMT 2014. LNCS, vol. 8568, pp. 25–41. Springer, Cham (2014). doi: 10.1007/978-3-319-08789-4_3 Google Scholar
  12. 12.
    Habel, A., Heckel, R., Taentzer, G.: Graph grammars with negative application conditions. Fundam. Inform. 26(3/4), 287–313 (1996)MathSciNetzbMATHGoogle Scholar
  13. 13.
    Habel, A., Pennemann, K.: Correctness of high-level transformation systems relative to nested conditions. MSCS 19(2), 245–296 (2009)MathSciNetzbMATHGoogle Scholar
  14. 14.
    Hähnle, R.: Tableaux and related methods. In: Handbook of Automated Reasoning (in 2 vols.), pp. 100–178 (2001)Google Scholar
  15. 15.
    Heckel, R., Wagner, A.: Ensuring consistency of conditional graph rewriting - a constructive approach. ENTCS 2, 118–126 (1995)zbMATHGoogle Scholar
  16. 16.
    Jackson, E.K., Levendovszky, T., Balasubramanian, D.: Reasoning about metamodeling with formal specifications and automatic proofs. In: Whittle, J., Clark, T., Kühne, T. (eds.) MODELS 2011. LNCS, vol. 6981, pp. 653–667. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-24485-8_48 CrossRefGoogle Scholar
  17. 17.
    Jackson, E.K., Sztipanovits, J.: Constructive techniques for meta- and model-level reasoning. In: Engels, G., Opdyke, B., Schmidt, D.C., Weil, F. (eds.) MODELS 2007. LNCS, vol. 4735, pp. 405–419. Springer, Heidelberg (2007). doi: 10.1007/978-3-540-75209-7_28 CrossRefGoogle Scholar
  18. 18.
    Krause, C., Johannsen, D., Deeb, R., Sattler, K., Knacker, D., Niadzelka, A.: An SQL-based query language and engine for graph pattern matching. In: Echahed and Minas [5], 153–169Google Scholar
  19. 19.
    Lack, S., Sobocinski, P.: Adhesive and quasiadhesive categories. ITA 39(3), 511–545 (2005)MathSciNetzbMATHGoogle Scholar
  20. 20.
    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). doi: 10.1007/978-3-319-09108-2_2 Google Scholar
  21. 21.
    Milicevic, A., Near, J.P., Kang, E., Jackson, D.: Alloy*: a general-purpose higher-order relational constraint solver. In: 37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, vol. 1, pp. 609–619 (2015)Google Scholar
  22. 22.
    Mougenot, A., Darrasse, A., Blanc, X., Soria, M.: Uniform random generation of huge metamodel instances. In: Paige, R.F., Hartman, A., Rensink, A. (eds.) ECMDA-FA 2009. LNCS, vol. 5562, pp. 130–145. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-02674-4_10 CrossRefGoogle Scholar
  23. 23.
    Orejas, F., Ehrig, H., Prange, U.: Reasoning with graph constraints. Formal Asp. Comput. 22(3–4), 385–422 (2010)CrossRefzbMATHGoogle Scholar
  24. 24.
    Pennemann, K.: An algorithm for approximating the satisfiability problem of high-level conditions. ENTCS 213, 75–94 (2008)zbMATHGoogle Scholar
  25. 25.
    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). doi: 10.1007/978-3-540-87405-8_20 CrossRefGoogle Scholar
  26. 26.
    Pennemann, K.H.: Development of Correct Graph Transformation Systems, PhD Thesis. Dept. Informatik, Univ. Oldenburg (2009)Google Scholar
  27. 27.
    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). doi: 10.1007/978-3-319-09108-2_3 Google Scholar
  28. 28.
    Radke, H.: Hr* graph conditions between counting monadic second-order and second-order graph formulas. ECEASST 61 (2013)Google Scholar
  29. 29.
    Radke, H., Arendt, T., Becker, J.S., Habel, A., Taentzer, G.: Translating essential OCL invariants to nested graph constraints focusing on set operations. In: Parisi-Presicce, F., Westfechtel, B. (eds.) ICGT 2015. LNCS, vol. 9151, pp. 155–170. Springer, Cham (2015). doi: 10.1007/978-3-319-21145-9_10 CrossRefGoogle Scholar
  30. 30.
    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). doi: 10.1007/978-3-540-30203-2_23 CrossRefGoogle Scholar
  31. 31.
    Rozenberg, G. (ed.): Handbook of Graph Grammars and Computing by Graph Transformations. Foundations, vol. 1. World Scientific, Singapore (1997)Google Scholar
  32. 32.
    Salay, R., Chechik, M.: A generalized formal framework for partial modeling. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 133–148. Springer, Heidelberg (2015). doi: 10.1007/978-3-662-46675-9_9 Google Scholar
  33. 33.
    Schneider, S., Lambers, L., Orejas, F.: Symbolic Model Generation for Graph Properties (Extended Version). No. 115 in Technische Berichte des Hasso-Plattner-Instituts für Softwaresystemtechnik an der Universität Potsdam, Universitätsverlag Potsdam, Hasso Plattner Institute (Germany, Potsdam), 1 edn. (2017)Google Scholar
  34. 34.
    Semeráth, O., Vörös, A., Varró, D.: Iterative and incremental model generation by logic solvers. In: Stevens, P., Wąsowski, A. (eds.) FASE 2016. LNCS, vol. 9633, pp. 87–103. Springer, Heidelberg (2016). doi: 10.1007/978-3-662-49665-7_6 CrossRefGoogle Scholar
  35. 35.
    The Linked Data Benchmark Council (LDBC): Social network benchmark (2016).
  36. 36.
    T.W.W.W.C. (W3C): W3C xml schema definition language (xsd) 1.1 part 1: structures (2012)Google Scholar
  37. 37.
    Wood, P.T.: Query languages for graph databases. SIGMOD Rec. 41(1), 50–60 (2012)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag GmbH Germany 2017

Authors and Affiliations

  1. 1.Hasso Plattner InstitutUniversity of PotsdamPotsdamGermany
  2. 2.Dpto de L.S.I.Universitat Politècnica de CatalunyaBarcelonaSpain

Personalised recommendations