×

Finding models through graph saturation. (English) Zbl 1401.68043

Summary: We give a procedure that can be used to automatically satisfy invariants of a certain shape. These invariants may be written with the operations intersection, composition and converse over binary relations, and equality over these operations. We call these invariants sentences that we interpret over graphs. For questions stated through sets of these sentences, this paper gives a semi-decision procedure we call graph saturation. It decides entailment over these sentences, inspired on graph rewriting. We prove correctness of the procedure. Moreover, we show the corresponding decision problem to be undecidable. This confirms a conjecture previously stated by the author [Lect. Notes Comput. Sci. 10226, 159–176 (2017; Zbl 1401.68136)].

MSC:

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
03B70 Logic in computer science
68Q42 Grammars and rewriting systems

Citations:

Zbl 1401.68136

Software:

Z; Ampersand; Alcoa; Alloy
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] Baader, F., The description logic handbook: theory, implementation and applications, (2003), Cambridge University Press · Zbl 1058.68107
[2] Baader, F.; Brandt, S.; Lutz, C., Pushing the \(\mathcal{EL}\) envelope, (Proceedings of the 19th International Joint Conference on Artificial Intelligence, IJCAI’05, (2005), Morgan Kaufmann Publishers Inc. San Francisco, CA, USA), 364-369
[3] Baader, F.; Brandt, S.; Lutz, C., Pushing the \(\mathcal{EL}\) envelope further, (Proceedings of the Fourth OWLED Workshop on OWL: Experiences and Directions, Washington, DC, USA, (April 2008))
[4] Freyd, P.; Scedrov, A., Categories, allegories, (1990), North-Holland Publishing Co. · Zbl 0698.18002
[5] Jackson, D., Alloy: a lightweight object modelling notation, ACM Trans. Softw. Eng. Methodol., 11, 2, 256-290, (2002)
[6] Jackson, D.; Schechter, I.; Shlyakhter, I., Alcoa: the alloy constraint analyzer, (ICSE, (2000))
[7] Joosten, S. J.C., Parsing and printing of and with triples, (International Conference on Relational and Algebraic Methods in Computer Science, (2017), Springer), 159-176 · Zbl 1401.68136
[8] Joosten, S., Software development in relation algebra with ampersand, (Pous, D.; Struth, G.; Höfner, P., Relational and Algebraic Methods in Computer Science: 16th International Conference, RAMICS, (2017), Springer International Publishing) · Zbl 1486.68042
[9] Kahl, W., A relation-algebraic approach to graph structure transformation, (International Conference on Relational Methods in Computer Science, (2001), Springer), 1-14 · Zbl 1027.68612
[10] Krisnadhi, A.; Lutz, C., Data complexity in the \(\mathcal{EL}\) family of description logics, (Logic for Programming, Artificial Intelligence, and Reasoning, (2007), Springer), 333-347 · Zbl 1137.68593
[11] Robinson, J. A., A machine-oriented logic based on the resolution principle, J. ACM, 12, 1, 23-41, (Jan 1965) · Zbl 0139.12303
[12] Schmidt, G.; Ströhlein, T., Relation algebras: concept of points and representability, Discrete Math., 54, 1, 83-92, (1985) · Zbl 0575.03040
[13] Spivey, J., The Z notation: A reference manual, International Series in Computer Science, (1992), Prentice Hall New York · Zbl 0777.68003
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.