Hostname: page-component-586b7cd67f-t7fkt Total loading time: 0 Render date: 2024-11-26T12:59:51.475Z Has data issue: false hasContentIssue false
  • English
  • Français

Recognizable languages of arrows and cospans

Published online by Cambridge University Press:  08 August 2018

H. J. SANDER BRUGGINK  and
BARBARA KÖNIG
H. J. SANDER BRUGGINK
Affiliation:
Universität Duisburg-Essen, Duisburg, Germany Email: [email protected]
BARBARA KÖNIG
Affiliation:
Universität Duisburg-Essen, Duisburg, Germany Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

In this article, we generalize Courcelle's recognizable graph languages and results on monadic second-order logic to more general structures.

First, we give a category-theoretical characterization of recognizability. A recognizable subset of arrows in a category is defined via a functor into the category of relations on finite sets. This can be seen as a straightforward generalization of finite automata. We show that our notion corresponds to recognizable graph languages if we apply the theory to the category of cospans of graphs.

In the second part of the paper, we introduce a simple logic that allows to quantify over the subobjects of a categorical object. Again, we show that, for the category of graphs, this logic is equally expressive as monadic second-order graph logic (msogl). Furthermore, we show that in the more general setting of hereditary pushout categories, a class of categories closely related to adhesive categories, we can recover Courcelle's result that every msogl-expressible property is recognizable. This is done by giving an inductive translation of formulas of our logic into automaton functors.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 28 , Special Issue 8: Term and Graph Rewriting , September 2018 , pp. 1290 - 1332
Copyright
Copyright © Cambridge University Press 2018 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Andersen, H.R. (1998). An introduction to binary decision diagrams. Version of October 1997 with minor revisions April 1998. Lecture notes, Technical University of Denmark, unpublished manuscript.Google Scholar
Blume, C., Sander Bruggink, H.J. and König, B. (2010). Recognizable graph languages for checking invariants. In: Proceedings of the of Workshop on Graph Transformation and Visual Modeling Techniques, Electronic Communications of the EASST, vol. 29. Available at http://journal.ub.tu-berlin.de/index.php/eceasst/article/view/408.Google Scholar
Blume, C., Sander Bruggink, H.J., Engelke, D. and König, B. (2012). Efficient symbolic implementation of graph automata with applications to invariant checking. In: Proceedings of the of International Conference on Graph Transformation, LNCS, vol. 7562, Springer, 264–278.Google Scholar
Blume, C., Sander Bruggink, H.J., Friedrich, M. and König, B. (2013). Treewidth, pathwidth and cospan decompositions with applications to graph-accepting tree automata. Journal of Visual Languages & Computing 24 (3) 192–206. Available at http://dx.doi.org/10.1016/j.jvlc.2012.10.002.Google Scholar
Bouajjani, A., Jonsson, B., Nilsson, M. and Touili, T. (2000). Regular model checking. In: Proceedings of Computer Aided Verification, LNCS, vol. 1855, Springer, 403–418.Google Scholar
Bouderon, M. and Courcelle, B. (1987). Graph expressions and graph rewritings. Mathematical Systems Theory 20 (1) 81–127.Google Scholar
Bozapalidis, S. and Kalampakas, A. (2006). Recognizability of graph and pattern languages. Acta Informatica 42 (8/9) 553–581.Google Scholar
Bozapalidis, S. and Kalampakas, A. (2008). Graph automata. Theoretical Computer Science 393 (1–3) 147–165.Google Scholar
Bruggink, H.J.S. (2007). Towards a systematic method for proving termination of graph transformation systems (work-in-progress paper). In: Proceedings of Graph Transformation for Concurrency and Verification.Google Scholar
Bruggink, H.J.S. and König, B. (2008). On the recognizability of arrow and graph languages. In: Proceedings of the International Conference on Graph Transformation, LNCS, vol. 5214, Springer, 336–350.Google Scholar
Bruggink, H.J.S. and König, B. (2010). A logic on subobjects and recognizability. In: Proceedings of the International Conference on FIP Theoretical Computer Science, vol. 323, Springer, 197–212.Google Scholar
Courcelle, B. (1990). The monadic second-order logic of graphs I. Recognizable sets of finite graphs. Information and Computation 85 (1) 12–75.Google Scholar
Courcelle, B. (1997). The expression of graph properties and graph transformations in monadic second-order logic. In: Rozenberg, G. (ed.) Handbook of Graph Grammars and Computing by Graph Transformation, Vol.1: Foundations, chapter 5. World Scientific.Google Scholar
Courcelle, B. and Durand, I. (2012). Automata for the verification of monadic second-order graph properties. Journal of Applied Logic 10 (4) 368–409.Google Scholar
Courcelle, B. and Engelfriet, J. (2012). Graph Structure and Monadic Second-Order Logic, A Language-Theoretic Approach, Cambridge University Press.Google Scholar
Courcelle, B. and Weil, P. (2005). The recognizability of sets of graphs is a robust property. Theoretical Computer Science 342 (2–3) 173–228.Google Scholar
Ehrig, H. and König, B. (2006). Deriving bisimulation congruences in the DPO approach to graph rewriting with borrowed contexts. Mathematical Structures in Computer Science 16 (6) 1133–1163.Google Scholar
Ehrig, H., Ehrig, K., Prange, U. and Taentzer, G. (2006). Fundamentals of Algebraic Graph Transformation, Springer.Google Scholar
Flum, J., Frick, M. and Grohe, M. (2002). Query evaluation via tree-decompositions. Journal of the ACM 49 (6) 716–752.Google Scholar
Gadducci, F. and Heckel, R. (1997). An inductive view of graph transformation. In: 12th International Workshop on Recent Trends in Algebraic Development Techniques, LNCS, vol. 1376, Springer, 223–237.Google Scholar
Geser, A., Hofbauer, D. and Waldmann, J. (2004). Match-bounded string rewriting systems. Applicable Algebra in Engineering, Communication and Computing 15 (3–4) 149–171.Google Scholar
Gottlob, G., Pichler, R. and Wei, F. (2010). Bounded treewidth as a key to tractability of knowledge representation and reasoning. Journal of Artificial Intelligence 174 (1) 105–132.Google Scholar
Griffing, G. (2003). Composition-representive subsets. Theory and Applications of Categories 11 (19) 420–437.Google Scholar
Habel, A., Kreowski, H.-J. and Lautemann, C. (1993). A comparison of compatible, finite and inductive graph properties. Theoretical Computer Science 110 (1) 145–168.Google Scholar
Heindel, T. (2009). A category theoretical approach to the concurrent semantics of rewriting. PhD thesis, University of Duisburg–Essen.Google Scholar
Jacobs, B. (1999). Categorical Logic and Type Theory, Studies in Logic and the Foundation of Mathematics, vol. 141, Elsevier.Google Scholar
Kuncak, V. and Rinard, M. (2003). Existential heap abstraction entailment is undecidable. In: Proceedings of the of SAS, LNCS, vol. 2694, Springer.Google Scholar
Lack, S. and Sobociński, P. (2005). Adhesive and quasiadhesive categories. RAIRO – Theoretical Informatics and Applications 39 (3) 511–545.Google Scholar
Mac Lane, S. (1971). Categories for the Working Mathematician, Springer.Google Scholar
Pitts, A. M. (2001). Categorical logic. In: Abramsky, S., Gabbay, D.M. and Maibaum, T.S.E. (eds.) Handbook of Logic in Computer Science V, Oxford University Press.Google Scholar
Rosebrugh, R., Sabadini, N. and Walters, R.F.C. (2005). Generic commutative separable algebras and cospans of graphs. Theory and Applications of Categories 15 (6) 164–177.Google Scholar
Rosebrugh, R., Sabadini, N. and Walters, R.F.C. (2008). Calculating colimits compositionally. In: Degano, P., De Nicola, R. and Meseguer, J. (eds.) Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday, LNCS, vol. 5065, Springer, 581–592.Google Scholar
Sassone, V. and Sobociński, P. (2005). Reactive systems over cospans. In: Proceedings of Logic in Computer Science, IEEE, 311–320.Google Scholar
Soguet, D. (2008). Génération automatique d'algorithmes linéaires. PhD thesis, Université Paris-Sud.Google Scholar