{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T11:43:33Z","timestamp":1749728613868},"reference-count":34,"publisher":"Cambridge University Press (CUP)","issue":"8","license":[{"start":{"date-parts":[[2018,8,8]],"date-time":"2018-08-08T00:00:00Z","timestamp":1533686400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2018,9]]},"abstract":"<jats:p>In this article, we generalize Courcelle's recognizable graph languages and results on monadic second-order logic to more general structures.<\/jats:p><jats:p>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.<\/jats:p><jats:p>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 (<jats:sc>msogl<\/jats:sc>). 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<jats:sc>msogl<\/jats:sc>-expressible property is recognizable. This is done by giving an inductive translation of formulas of our logic into automaton functors.<\/jats:p>","DOI":"10.1017\/s096012951800018x","type":"journal-article","created":{"date-parts":[[2018,8,8]],"date-time":"2018-08-08T01:05:48Z","timestamp":1533690348000},"page":"1290-1332","source":"Crossref","is-referenced-by-count":3,"title":["Recognizable languages of arrows and cospans"],"prefix":"10.1017","volume":"28","author":[{"given":"H. J. SANDER","family":"BRUGGINK","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"BARBARA","family":"K\u00d6NIG","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2018,8,8]]},"reference":[{"key":"S096012951800018X_ref3","doi-asserted-by":"crossref","unstructured":"Blume C. , Sander Bruggink H.J. , Engelke D. and K\u00f6nig 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\u2013278.","DOI":"10.1007\/978-3-642-33654-6_18"},{"key":"S096012951800018X_ref34","unstructured":"Soguet D. (2008). G\u00e9n\u00e9ration automatique d'algorithmes lin\u00e9aires. PhD thesis, Universit\u00e9 Paris-Sud."},{"key":"S096012951800018X_ref14","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2011.07.001"},{"key":"S096012951800018X_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2009.10.003"},{"key":"S096012951800018X_ref4","doi-asserted-by":"publisher","DOI":"10.1016\/j.jvlc.2012.10.002"},{"key":"S096012951800018X_ref9","unstructured":"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."},{"key":"S096012951800018X_ref10","doi-asserted-by":"crossref","unstructured":"Bruggink H.J.S. and K\u00f6nig B. (2008). On the recognizability of arrow and graph languages. In: Proceedings of the International Conference on Graph Transformation, LNCS, vol. 5214, Springer, 336\u2013350.","DOI":"10.1007\/978-3-540-87405-8_23"},{"key":"S096012951800018X_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/602220.602222"},{"key":"S096012951800018X_ref25","unstructured":"Heindel T. (2009). A category theoretical approach to the concurrent semantics of rewriting. PhD thesis, University of Duisburg\u2013Essen."},{"key":"S096012951800018X_ref17","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950600569X"},{"key":"S096012951800018X_ref13","volume-title":"Handbook of Graph Grammars and Computing by Graph Transformation, Vol.1: Foundations","author":"Courcelle","year":"1997"},{"key":"S096012951800018X_ref31","first-page":"164","article-title":"Generic commutative separable algebras and cospans of graphs","volume":"15","author":"Rosebrugh","year":"2005","journal-title":"Theory and Applications of Categories"},{"key":"S096012951800018X_ref26","volume-title":"Categorical Logic and Type Theory","author":"Jacobs","year":"1999"},{"key":"S096012951800018X_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90043-H"},{"key":"S096012951800018X_ref1","unstructured":"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."},{"key":"S096012951800018X_ref11","doi-asserted-by":"crossref","unstructured":"Bruggink H.J.S. and K\u00f6nig B. (2010). A logic on subobjects and recognizability. In: Proceedings of the International Conference on FIP Theoretical Computer Science, vol. 323, Springer, 197\u2013212.","DOI":"10.1007\/978-3-642-15240-5_15"},{"key":"S096012951800018X_ref6","first-page":"81","article-title":"Graph expressions and graph rewritings","volume":"20","author":"Bouderon","year":"1987","journal-title":"Mathematical Systems Theory"},{"key":"S096012951800018X_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/s00200-004-0162-8"},{"key":"S096012951800018X_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)90354-V"},{"key":"S096012951800018X_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-006-0006-z"},{"key":"S096012951800018X_ref30","volume-title":"Handbook of Logic in Computer Science V","author":"Pitts","year":"2001"},{"key":"S096012951800018X_ref29","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-9839-7"},{"key":"S096012951800018X_ref20","first-page":"223","volume-title":"12th International Workshop on Recent Trends in Algebraic Development Techniques","author":"Gadducci","year":"1997"},{"key":"S096012951800018X_ref18","volume-title":"Fundamentals of Algebraic Graph Transformation","author":"Ehrig","year":"2006"},{"key":"S096012951800018X_ref32","doi-asserted-by":"crossref","first-page":"581","DOI":"10.1007\/978-3-540-68679-8_36","volume-title":"Concurrency, Graphs and Models, Essays Dedicated to Ugo Montanari on the Occasion of His 65th Birthday","author":"Rosebrugh","year":"2008"},{"key":"S096012951800018X_ref2","unstructured":"Blume C. , Sander Bruggink H.J. and K\u00f6nig 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."},{"key":"S096012951800018X_ref15","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511977619"},{"key":"S096012951800018X_ref16","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.03.018"},{"key":"S096012951800018X_ref28","doi-asserted-by":"publisher","DOI":"10.1051\/ita:2005028"},{"key":"S096012951800018X_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_31"},{"key":"S096012951800018X_ref23","first-page":"420","article-title":"Composition-representive subsets","volume":"11","author":"Griffing","year":"2003","journal-title":"Theory and Applications of Categories"},{"key":"S096012951800018X_ref8","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.11.022"},{"key":"S096012951800018X_ref27","doi-asserted-by":"crossref","unstructured":"Kuncak V. and Rinard M. (2003). Existential heap abstraction entailment is undecidable. In: Proceedings of the of SAS, LNCS, vol. 2694, Springer.","DOI":"10.1007\/3-540-44898-5_24"},{"key":"S096012951800018X_ref33","doi-asserted-by":"crossref","unstructured":"Sassone V. and Soboci\u0144ski P. (2005). Reactive systems over cospans. In: Proceedings of Logic in Computer Science, IEEE, 311\u2013320.","DOI":"10.1109\/LICS.2005.40"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S096012951800018X","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,21]],"date-time":"2019-10-21T20:29:03Z","timestamp":1571689743000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S096012951800018X\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,8,8]]},"references-count":34,"journal-issue":{"issue":"8","published-print":{"date-parts":[[2018,9]]}},"alternative-id":["S096012951800018X"],"URL":"https:\/\/doi.org\/10.1017\/s096012951800018x","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,8,8]]}}}