# Symbolic Model Generation for Graph Properties

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

## Abstract

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.

## Keywords

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

## References

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)
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)
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: Google Scholar
12. 12.
Habel, A., Heckel, R., Taentzer, G.: Graph grammars with negative application conditions. Fundam. Inform. 26(3/4), 287–313 (1996)
13. 13.
Habel, A., Pennemann, K.: Correctness of high-level transformation systems relative to nested conditions. MSCS 19(2), 245–296 (2009)
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)
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:
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:
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)
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: 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:
23. 23.
Orejas, F., Ehrig, H., Prange, U.: Reasoning with graph constraints. Formal Asp. Comput. 22(3–4), 385–422 (2010)
24. 24.
Pennemann, K.: An algorithm for approximating the satisfiability problem of high-level conditions. ENTCS 213, 75–94 (2008)
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:
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: 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:
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:
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: 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:
35. 35.
The Linked Data Benchmark Council (LDBC): Social network benchmark (2016). http://ldbcouncil.org/benchmarks/snb
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)