Abstract
Diagrammatic modelling is the foundation of many popular knowledge representation and software development techniques. In Model Driven Software Engineering, domain specific modelling languages are represented as metamodels and domain specific specifications are represented as models. The (meta-)models are represented by graphs and (models) instances are represented by graphs typed by the (meta)model. The typing relation is formalised by graph homomorphisms. Constraints are used to further specify the semantics of models. The state of the art modelling techniques of today have limited support for expressing and reasoning about diagrammatic constraints; constraints are usually expressed in an external textual language, not fully integrated in the metamodelling process. The diagram predicate framework, DPF is a fully diagrammatic meta modelling technique where one can express arbitrary diagrammatic constraints in the form of predicates on graphs. In this paper we build on ideas, successfuly exploited in a variety of logical systems by Orłowska and collaborators, to build a logical reasoning system for diagrammatic specifications. We enrich the expressiveness of DPF specifications to include semantic dependencies between DPF constraints and present a sound and complete reasoning system using a dual tableaux deduction system to determine if DPF specifications are satisfiable. We briefly discuss an extension of the reasoning system which uses the relational approach to encode the existence of certain graph homomorphisms and provide deduction rules to account for necessary properties of these homomorphisms.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
Note that the definition of atomic constraint corresponds to the definition of diagram in category theory (Barr and Wells 1999).
- 2.
Note that \([\![{p}]\!]\) is a subset of graph homomorphisms from the set of graph homomorphisms with any graph O as source and with target \(\alpha ^{\varSigma }(p)\) .
References
Alloy Tools. (2017). Alloy Project website. Retrieved March 26, 2018, from http://alloytools.org/.
Allwein, G. & MacCaull, W. (2001). A Kripke semantics for the logic of Gelfand quantales. Studia Logica, 68(2), 173–228.
Atkinson, C. & Kühne, T. (2001). The essence of multilevel metamodeling. In M. Gogolla & C. Kobryn (Eds.), International Conference on the Unified Modeling Language (Vol. 2185, pp. 19–33). Lecture Notes in Computer Science. New York: Springer.
Barr, M. & Wells, C. (1999). Category Theory for Computing Science (3rd ed.). Montreal: Les Publications CRM.
Buszkowski, W. & Orłowska, E. (1995). Relational Formalization of Dependencies in Information Systems. Preprint.
Calder, T. & Lamo, Y. (2016). A bottom up approach to model based program validation. In D. D. Ruscio, J. de Lara, & A. Pierantonio (Eds.), Proceedings of the \(2^{nd}\)Workshop on Flexible Model Driven Engineering (Vol. 1694, pp. 12–21). CEUR Workshop Proceedings. https://CEUR-WS.org.
Chen, P. P. (1976). The entity-relationship model–toward a unified view of data. ACM Transactions on Database Systems, 1(1), 9–36.
Courcelle, B. & Engelfriet, J. (2012). Graph Structure and Monadic Second-order Logic: A Language-Theoretic Approach. Cambridge: Cambridge University Press.
Diskin, Z. (1997). Generalized Sketches as an Algebraic Graph-based Framework for Semantic Modeling and Database Design. Laboratory for Database Design, University of Latvia: FIS/LDBD-97-03.
Diskin, Z. & Wolter, U. (2008). A diagrammatic logic for object-oriented visual modeling. Electronic Notes in Theoretical Computer Science, 203(6), 19–41.
Ehrig, H., Ehrig, K., Prange, U., & Taentzer, G. (2006). Fundamentals of Algebraic Graph Transformation. Monographs in Theoretical Computer Science, an EATCS series. Berlin: Springer.
Konikowska, B. & Białasik, M. (1999). Reasoning with first order nondeterministic specifications. Acta Informatica, 36(5), 375–403.
Lambers, L. & Orejas, F. (2014). Tableau-based reasoning for graph properties. In H. Giese & B. König (Eds.), Graph Transformation–7th International Conference, ICGT 2014, held as part of STAF 2014, York, UK, July 22–24, 2014. Proceedings (Vol. 8571, pp. 17–32). Lecture Notes in Computer Science. New York: Springer.
Lamo, Y. & Walicki, M. (2006). Quantifier-free logic for nondeterministic theories. Theoretical Computer Science, 355(2), 215–227.
Lamo, Y., Wang, X., Mantz, F., MacCaull, W., & Rutle, A. (2012). DPF workbench: A diagrammatic multi-layer domain specific (meta-)modelling environment. In R. Lee (Ed.), Computer and Information Science 2012 (Vol. 429, pp. 37–52). Berlin: Springer.
MacCaull, W. (1997). Relational proof system for linear and other substructural logics. Logic Journal of IGPL, 5(5), 673–697.
MacCaull, W. (1998a). Relational semantics and a relational proof system for full Lambek calculus. The Journal of Symbolic Logic, 63(2), 623–637.
MacCaull, W. (1998b). Relational tableaux for tree models, language models and information networks. In E. Orłowska (Ed.), Logic at Work: Essays Dedicated to the Memory of Helena Rasiowa. Heidelberg: Physica.
MacCaull, W. (2000). A proof system for dependencies for information relations. Fundamenta Informaticae, 42(1), 1–27.
MacCaull, W. & Orłowska, E. (2002). Correspondence results for relational proof systems with applications to the Lambek calculus. Studia Logica, 71(3), 389–414.
MacCaull, W. & Orłowska, E. (2006). A logic of typed relations and its applications to relational databases. Journal of Logic and Computation, 16(6), 789–815.
Makkai, M. (1997). Generalized sketches as a framework for completeness theorems. Part I. Journal of Pure and Applied Algebra, 115(1), 49–79.
Orejas, F. (2011). Symbolic graphs for attributed graph constraints. Journal of Symbolic Computation, 46(3), 294–315.
Orejas, F., Ehrig, H., & Prange, U. (2010). Reasoning with graph constraints. Formal Aspects of Computing, 22(3–4), 385–422.
Orłowska, E. (1992). Relational proof systems for relevant logics. Journal of Symbolic Logic, 57(4), 1425–1440.
Orłowska, E. (1994). Relational semantics for non-classical logics: Formulas are relations. In J. Woleński (Ed.), Philosophical Logic in Poland (pp. 167–186). Alphen aan den Rijn: Kluwer.
Orłowska, E. (1996). Relational proof systems for modal logics. In H. Wansing (Ed.), Proof Theory of Modal Logics (pp. 55–78). Berlin: Kluwer Academic Publishers.
Orłowska, E. & Golińska-Pilarek, J. (2011). Dual Tableaux: Foundations, Methodology, Case Studies. Trends in Logic. Dordrecht-Heidelberg-London-New York: Springer.
Rabbi, F., Lamo, Y., Yu, I. C., & Kristensen, L. M. (2015). A diagrammatic approach to model completion. In J. Dingel, S. Kokaly, L. Lucio, R. Salay, & H. Vangheluwe (Eds.), Proceedings of the \(4^{th}\)Workshop on the Analysis of Model Transformations (Vol. 1500, pp. 56–65). CEUR Workshop Proceedings. http://CEUR-WS.org.
Rabbi, F., Lamo, Y., & Yu, I. C. (2016a). Towards a categorical approach for metamodelling epistemic game theory. In Proceedings of the ACM/IEEE \(19^{th}\)International Conference on Model Driven Engineering Languages and Systems (pp. 57–64). New York City: ACM.
Rabbi, F., Lamo, Y., Yu, I. C., & Kristensen, L. M. (2016b). Diagrammatic development of domain specific modelling languages with WebDPF. International Journal of Information System Modeling and Design, 7(3), 93–114.
Rasiowa, H. & Sikorski, R. (1963). The Mathematics of Metamathematics. Warsaw: Polish Scientific Publishers.
Rensink, A. (2004). Representing first-order logic using graphs. In H. Ehrig, G. Engels, F. Parisi-Presicce, & G. Rozenberg (Eds.), International Conference on Graph Transformation (Vol. 3256, pp. 319–335). Lecture Notes in Computer Science. Berlin: Springer.
Rossini, A., Rutle, A., Lamo, Y., & Wolter, U. (2010). A formalisation of the copymodify- merge approach to version control in MDE. The Journal of Logic and Algebraic Programming, 79(7), 636–658.
Routley, R. & Meyer, R. (1973). The semantics of entailment. In H. Leblanc (Ed.), Truth, Syntax and Modality (Vol. 68, pp. 199–243). Studies in Logic and the Foundations of Mathematics. New York: Elsevier.
Rumbaugh, J., Jacobson, I., & Booch, G. (2004). The Unified Modeling Language Reference Manual. Pearson Higher Education.
Rutle, A. (2010). Diagram Predicate Framework: A Formal Approach to MDE. Doctoral dissertation, Department of Informatics, University of Bergen.
Rutle, A., MacCaull,W.,Wang, H., & Lamo, Y. (2012). A metamodelling approach to behavioural modelling. In Proceedings of the\(4^{th}\)Workshop on Behaviour Modelling-foundations and Applications. New York City: ACM.
Rutle, A., Rabbi, F., MacCaull, W., & Lamo, Y. (2013). A user-friendly tool for model checking healthcare workflows. Procedia Computer Science, 21, 317–326.
Rutle, A., Rossini, A., Lamo, Y., & Wolter, U. (2009). A diagrammatic formalization of MOF-based modelling languages. In M. Oriol & B. Meyer (Eds.), International Conference on Objects, Components, Models and Patterns (Vol. 33, pp. 37–56). Lecture Notes in Business Information Processing. Berlin: Springer.
Soley, R. (2000, November 20). Model Driven Architecture. Retrieved from https://www.omg.org/~soley/mda.html.
Steinberg, D., Budinsky, F., Merks, E., & Paternostro, M. (2008). EMF: Eclipse Modeling Framework. Hoboken: Addison-Wesley Professional.
Vaziri, M. & Jackson, D. (2000). Some shortcomings of OCL, the object constraint language of UML. In \(34^{th}\)International Conference on Technology of Object-oriented Languages and Systems (pp. 555–562). IEEE.
Wang, X., Büttner, F., & Lamo, Y. (2014). Verification of graph-based model transformations using Alloy. Electronic Communications of the EASST, 67.
Wang, X., Rutle, A., & Lamo, Y. (2015). Towards user-friendly and efficient analysis with Alloy. In M. Famelis, D. Ratiu, M. Seidl, & G. M. K. Selim (Eds.), Proceedings of the 12\(^{th}\) Workshop on Model-driven Engineering, Verification and Validation (Vol. 1514, pp. 28–37). CEUR Workshop Proceedings. http://CEUR-WS.org
Acknowledgements
This paper is the result of discussions initiated when the first author visited StFX in 2013 as “Heaps Chair in Computer Science”. The second author acknowledges support from the Natural Sciences and Engineering Research Council of Canada.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this chapter
Cite this chapter
Lamo, Y., MacCaull, W. (2018). A Reasoning System for Satisfiability of Diagrammatic Specifications. In: Golińska-Pilarek, J., Zawidzki, M. (eds) Ewa Orłowska on Relational Methods in Logic and Computer Science. Outstanding Contributions to Logic, vol 17. Springer, Cham. https://doi.org/10.1007/978-3-319-97879-6_15
Download citation
DOI: https://doi.org/10.1007/978-3-319-97879-6_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-97878-9
Online ISBN: 978-3-319-97879-6
eBook Packages: Religion and PhilosophyPhilosophy and Religion (R0)