×

zbMATH — the first resource for mathematics

A navigational logic for reasoning about graph properties. (English) Zbl 1455.68147
Summary: Graphs play an important role in many areas of Computer Science. In particular, our work is motivated by model-driven software development and by graph databases. For this reason, it is very important to have the means to express and to reason about the properties that a given graph may satisfy. With this aim, in this paper we present a visual logic that allows us to describe graph properties, including navigational properties, i.e., properties about the paths in a graph. The logic is equipped with a deductive tableau method that we have proved to be sound and complete.
MSC:
68R10 Graph theory (including graph drawing) in computer science
03B70 Logic in computer science
Software:
VAMPIRE
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Courcelle, B., The expression of graph properties and graph transformations in monadic second-order logic, (Rozenberg, G., Handbook of Graph Grammars (1997), World Scientific), 313-400
[2] Cardelli, L.; Gardner, P.; Ghelli, G., A spatial logic for querying graphs, (Widmayer, P.; Ruiz, F. T.; Bueno, R. M.; Hennessy, M.; Eidenbenz, S. J.; Conejo, R., Automata, Languages and Programming, 29th International Colloquium. Automata, Languages and Programming, 29th International Colloquium, ICALP 2002, Malaga, Spain, July 8-13, 2002, Proceedings. Automata, Languages and Programming, 29th International Colloquium. Automata, Languages and Programming, 29th International Colloquium, ICALP 2002, Malaga, Spain, July 8-13, 2002, Proceedings, Lecture Notes in Computer Science, vol. 2380 (2002), Springer), 597-610 · Zbl 1057.68606
[3] Habel, A.; Pennemann, K.-H., Correctness of high-level transformation systems relative to nested conditions, Math. Struct. Comput. Sci., 19, 2, 245-296 (2009) · Zbl 1168.68022
[4] Pennemann, K.-H., Development of Correct Graph Transformation Systems (2009), Department of Computing Science, Univ. of Oldenburg, PhD Thesis
[5] Baumgartner, P.; Fuchs, A.; Tinelli, C., Implementing the model evolution calculus, Int. J. Artif. Intell. Tools, 15, 1, 21-52 (2006)
[6] Riazanov, A.; Voronkov, A., The design and implementation of VAMPIRE, AI Commun., 15, 2-3, 91-110 (2002) · Zbl 1021.68082
[7] Lambers, L.; Orejas, F., Tableau-based reasoning for graph properties, (Graph Transformation - 7th International Conference. Graph Transformation - 7th International Conference, ICGT 2014. Graph Transformation - 7th International Conference. Graph Transformation - 7th International Conference, ICGT 2014, Lecture Notes in Computer Science, vol. 8571 (2014), Springer), 17-32 · Zbl 1425.68316
[8] Schneider, S.; Lambers, L.; Orejas, F., Symbolic model generation for graph properties, (Fundamental Approaches to Software Engineering FASE 2017, Held as Part of ETAPS 2017. Fundamental Approaches to Software Engineering FASE 2017, Held as Part of ETAPS 2017, Lecture Notes in Computer Science, vol. 10202 (2017), Springer), 226-243 · Zbl 1430.68241
[9] Schneider, S.; Lambers, L.; Orejas, F., Automated reasoning for attributed graph properties, Int. J. Softw. Tools Technol. Transf., 20, 4, 705-737 (2018)
[10] Navarro, M.; Orejas, F.; Pino, E., Satisfiability of constraint specifications on XML documents, (Martí-Oliet, N.; Ölveczky, P. C.; Talcott, C. L., Logic, Rewriting, and Concurrency - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday. Logic, Rewriting, and Concurrency - Essays dedicated to José Meseguer on the Occasion of His 65th Birthday, Lecture Notes in Computer Science, vol. 9200 (2015), Springer), 539-561 · Zbl 1321.68352
[11] Lambers, L.; Navarro, M.; Orejas, F.; Pino, E., Towards a navigational logic for graphical structures, (Graph Transformation, Specifications, and Nets - In Memory of Hartmut Ehrig. Graph Transformation, Specifications, and Nets - In Memory of Hartmut Ehrig, Lecture Notes in Computer Science, vol. 10800 (2018), Springer), 124-141 · Zbl 1383.68064
[12] Orejas, F.; Pino, E.; Navarro, M.; Lambers, L., Institutions for navigational logics for graphical structures, Theor. Comput. Sci., 741, 19-24 (2018) · Zbl 1436.03325
[13] Goguen, J.; Burstall, R., Institutions: Abstract model theory for specification and programming, J. ACM, 1, 39, 95-149 (1992) · Zbl 0799.68134
[14] Sannella, D.; Tarlecki, A., Specifications in an arbitrary institution, Inf. Comput., 76, 2/3, 165-210 (1988) · Zbl 0654.68017
[15] Orejas, F.; Ehrig, H.; Prange, U., Reasoning with graph constraints, Form. Asp. Comput., 22, 3-4, 385-422 (2010) · Zbl 1209.68381
[16] Ehrig, H.; Ehrig, K.; Prange, U.; Taentzer, G., Fundamentals of algebraic graph transformation (2006), Springer-Verlag · Zbl 1095.68047
[17] Hähnle, R., Tableaux and related methods, (Robinson, J. A.; Voronkov, A., Handbook of Automated Reasoning (2001), Elsevier and MIT Press), 100-178 · Zbl 1011.68125
[18] Pennemann, K.-H., Resolution-like theorem proving for high-level conditions, (Graph Transformations, 4th International Conference, ICGT 2008. Graph Transformations, 4th International Conference, ICGT 2008, Lecture Notes in Computer Science, vol. 5214 (2008), Springer), 289-304 · Zbl 1175.03008
[19] Trakhtenbrot, B. A., The impossibility of an algorithm for the decision problem on finite classes, Dokl. Akad. Nauk SSSR, 70, 23, 569-572 (1950) · Zbl 0038.15001
[20] Staiger, L., ω languages, (Rozenberg, G.; Salomaa, A., Handbook of Formal Languages, Vol. 3: Beyond Words (1997), Springer-Verlag New York, Inc.: Springer-Verlag New York, Inc. New York, NY, USA), 339-387
[21] Ehrig, H.; Habel, A., Graph grammars with application conditions, (Rozenberg, G.; Salomaa, A., The Book of L (1986), Springer: Springer Berlin), 87-100 · Zbl 0611.68045
[22] Heckel, R.; Wagner, A., Ensuring consistency of conditional graph rewriting - a constructive approach, Electron. Notes Theor. Comput. Sci., 2, 118-126 (1995) · Zbl 0910.68154
[23] Habel, A.; Heckel, R.; Taentzer, G., Graph grammars with negative application conditions, Fundam. Inform., 26, 287-313 (1996) · Zbl 0854.68055
[24] Rensink, A., Representing first-order logic using graphs, (Graph Transformations, Second International Conference, ICGT 2004. Graph Transformations, Second International Conference, ICGT 2004, Lecture Notes in Computer Science, vol. 3256 (2004), Springer), 319-335 · Zbl 1116.03303
[25] A. Habel, H. Radke, Expressiveness of graph conditions with variables, ECEASST 30.
[26] Poskitt, C. M.; Plump, D., Verifying monadic second-order properties of graph programs, (Graph Transformation - 7th International Conference, ICGT 2014. Graph Transformation - 7th International Conference, ICGT 2014, Lecture Notes in Computer Science, vol. 8571 (2014), Springer), 33-48 · Zbl 1425.68080
[27] Angles, R.; Arenas, M.; Barceló, P.; Hogan, A.; Reutter, J.; Vrgoč, D., Foundations of modern query languages for graph databases, ACM Comput. Surv., 50, 5, Article 68 pp. (2017), 1-40
[28] Barceló, P.; Libkin, L.; Reutter, J. L., Querying graph patterns, (Proceedings of the 30th ACM PODS 2011 (2011)), 199-210
[29] Wood, P. T., Query languages for graph databases, SIGMOD Rec., 41, 1, 50-60 (2012)
[30] Barceló, P., Querying graph databases, (Proceedings of the 32nd ACM PODS 2013 (2013)), 175-188
[31] Barceló, P.; Libkin, L.; Reutter, J. L., Querying regular graph patterns, J. ACM, 61, 1, Article 8 pp. (2014), 1-54 · Zbl 1295.68125
[32] Barceló, P.; Romero, M.; Vardi, M. Y., Semantic acyclicity on graph databases, SIAM J. Comput., 45, 4, 1339-1376 (2016) · Zbl 1407.68123
[33] Koch, M.; Mancini, L. V.; Parisi-Presicce, F., Graph-based specification of access control policies, J. Comput. Syst. Sci., 71, 1, 1-33 (2005) · Zbl 1081.68072
[34] Giese, H.; Wagner, R., From model transformation to incremental bidirectional model synchronization, Softw. Syst. Model., 8, 1, 21-43 (2009)
[35] Hofmann, M.; Pierce, B. C.; Wagner, D., Symmetric lenses, in: POPL 2011, 371-384 (2011), ACM · Zbl 1284.18009
[36] Date, C. J., View Updating and Relational Theory (2012), O’Reilly
[37] Schneider, S.; Lambers, L.; Orejas, F., A logic-based incremental approach to graph repair, (Fundamental Approaches to Software Engineering, Held as Part of ETAPS 2019. Fundamental Approaches to Software Engineering, Held as Part of ETAPS 2019, Lecture Notes in Computer Science, vol. 11424 (2019), Springer), 151-167
[38] Orejas, F., Symbolic graphs for attributed graph constraints, J. Symb. Comput., 46, 3, 294-315 (2011) · Zbl 1298.68121
[39] The Linked Data Benchmark Council (LDBC), Social network benchmark (2017), Tech. rep
[40] Lambers, L.; Schneider, S.; Weisgut, M., Model-based testing of read only graph queries, (13th IEEE International Conference on Software Testing, Verification and Validation Workshops. 13th IEEE International Conference on Software Testing, Verification and Validation Workshops, ICSTW 2020, Porto, Portugal, October 24-28, 2020 (2020), IEEE), 24-34
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.