Monadic second order logic and node relations on graphs and trees
Let \(\Sigma\) and \(\Gamma\) be alphabets of node and edge labels. A directed graph over \((\Sigma, \Gamma)\) is a triple \((V,E, \text{lab})\), where \(V\) is a finite set of nodes, \(E \subseteq V\times \Gamma \times V\) is a finite set of labeled edges, \(\text{lab}: V\to \Sigma\) is a node-labelling function. Monadic second-order (MSO) logic has node variables \(x,y, \dots\), node-set variables \(X,Y, \dots\), and for every \((\Sigma, \Gamma)\) four types of atomic formulas: \(x=y\); \(x\in X\); \(\text{lab}_\sigma (x)\), \(\sigma \in \Sigma\), denoting that node \(x\) has label \(\sigma\); \(\text{edg}_\gamma (x,y)\), \(\gamma\in \Gamma\), denoting that there is the edge \((x,\gamma,y)\). A graph-walking automaton \(A\) is a finite-state machine that walks on a graph from node to node, following the edges of the graph along or against the direction of the edges. Automaton \(A\) can test the labels of the current node and current edge and any MSO definable property of the current node (the property is given by an MSO formula with unique free node variable). A pair of nodes \((u,v)\) is in the binary relation defined by \(A\) if \(A\), having an initial state in \(u\), can reach \(v\) in a final state. It is shown that if a binary relation on the nodes of a graph can be computed by a finite-state graph-walking automaton, then it can be defined by an MSO formula, but, in general, not vice versa. For the entire collection see [Zbl 0868.00014].
- The monadic second-order logic of graphs. VII: Graphs as relational structures
- Monadic second-order logic, graph coverings and unfoldings of transition systems
- A comparison of tree transductions defined by monadic second order logic and by attribute grammars
- Monadic second-order logic on tree-like structures
- Existential monadic second order logic on random rooted trees
- Attribute grammars for unranked trees as a query language for structured documents
- An operational and denotational approach to non-context-freeness
- Linear-bounded composition of tree-walking tree transducers: linear size increase and complexity
- Verification of agent navigation in partially-known environments
- XML navigation and transformation by tree-walking automata and transducers with visible and invisible pebbles
- Branch-width, parse trees, and monadic second-order logic for matroids.
- Fusion in relational structures and the verification of monadic second-order properties
- scientific article; zbMATH DE number 1290983 (Why is no real title available?)
- Monadic Second-Order Logic and Transitive Closure Logics over Trees
- GETGRATS: a summary of scientific results (with annotated bibliography)
This page was built for publication: Monadic second order logic and node relations on graphs and trees
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4362731)
