Recognizable languages of arrows and cospans

2018 ◽  
Vol 28 (8) ◽  
pp. 1290-1332
Author(s):  
H. J. SANDER BRUGGINK ◽  
BARBARA KÖNIG

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 everymsogl-expressible property is recognizable. This is done by giving an inductive translation of formulas of our logic into automaton functors.

10.29007/t28j ◽  
2018 ◽  
Author(s):  
Loris D'Antoni ◽  
Margus Veanes

We extend weak monadic second-order logic of one successor (WS1S) to symbolic alphabets byallowing character predicates to range over decidable first order theories and not just finite alphabets.We call this extension symbolic WS1S (s-WS1S). We then propose two decision procedures for such alogic: 1) we use symbolic automata to extend the classic reduction from WS1S to finite automata toour symbolic logic setting; 2) we show that every s-WS1S formula can be reduced to a WS1S formulathat preserves satisfiability, at the price of an exponential blow-up.


10.37236/1656 ◽  
2002 ◽  
Vol 9 (1) ◽  
Author(s):  
B. Courcelle ◽  
V. Dussaux

A map is a graph equipped with a circular order of edges around each vertex. These circular orders represent local planar embeddings. The genus of a map is the minimal genus of an orientable surface in which it can be embedded. The maps of genus at most $g$ are characterized by finitely many forbidden maps, relatively to an appropriate ordering related to the minor ordering of graphs. This yields a "noninformative" characterization of these maps, that is expressible in monadic second-order logic. We give another one, which is more informative in the sense that it specifies the relevant surface embedding, in addition to stating its existence.


2017 ◽  
Vol 52 (1) ◽  
pp. 232-245
Author(s):  
Loris D'Antoni ◽  
Margus Veanes

Sign in / Sign up

Export Citation Format

Share Document