Determining the clique-width or the linear clique-width of an undirected graph reduces to a Boolean satisfiability problem (a SAT problem in short) that can be solved for graphs of moderate size, depending on the available solver. This method is due to Heule and Szeider. We extend it to directed graphs, to vertex-labelled graphs and to the computation of relative clique-width. We have checked that certain proved upper-bounds to clique-width are actually reachable. We also propose open questions about upper-bounds to clique-width that this approach may help to solve. Every existential second-order graph property P has an NP-algorithm and can be formulated as a SAT problem constructed from the graph G for which P has to be checked. However, the resulting instance may be much too large to be solved in practice. We consider particular existential second-order sentences from which SAT problems of polynomial size can be easily constructed and, furthermore, that define hereditary graph properties, i.e. preserved by induced graph inclusion. Motivated by the search of minimal excluded graphs for hereditary graph properties (induced subgraph inclusion is here the relevant partial order on graphs), we examine cases where a SAT problem for an induced subgraph of a graph G can be obtained easily from the corresponding SAT problem for G .

We study the infinite trees that arise, first as complete unfoldings of finite weighted directed graphs, and second, as universal coverings of finite weighted undirected graphs. They are respectively the regular rooted trees and the strongly regular trees, a new notion. A rooted tree is regular if it has finitely many subtrees up to isomorphism. A tree (without root) is strongly regular if it has finitely many rooted trees, up to isomorphism, obtained by taking each of its nodes as a root. We prove the first-order definability of each regular or strongly regular tree with respect to the class of trees (that is not itself first-order definable). We characterize the strongly regular trees among the regular ones and we establish several decidability results.

An order-theoretic forest is a countable partial order such that the set of elements larger than any element is linearly ordered. It is an order-theoretic tree if any two elements have an upper-bound. The order type of a branch can be any countable linear order. Such generalized infinite trees yield convenient definitions of the rank-width and the modular decomposition of countable graphs. We define an algebra based on only four operations that generate up to isomorphism and via infinite terms these order-theoretic trees and forests. We prove that the associated regular objects, those defined by regular terms, are exactly the ones that are the unique models of monadic second-order sentences. Comment: 32 pages, 6 figures

Coverings of undirected graphs are used in distributed computing, and unfoldings of directed graphs in semantics of programs. We study these two notions from a graph theoretical point of view so as to highlight their similarities, as they are both defined in terms of surjective graph homomorphisms. In particular, universal coverings and complete unfoldings are infinite trees that are regular if the initial graphs are finite. Regularity means that a tree has finitely many subtrees up to isomorphism. Two important theorems have been established by Leighton and Norris for coverings of finite graphs. We prove similar results for unfoldings of finite directed graphs. Moreover, we generalize coverings and similarly, unfoldings to graphs and digraphs equipped with finite or infinite weights attached to edges of the covered or unfolded graphs. This generalization yields a canonical “factorization” of the universal covering of any finite graph, that (provably) does not exist without using weights. Introducing ω as an infinite weight provides us with finite descriptions of regular trees having nodes of countably infinite degree. Regular trees (trees having finitely many subtrees up to isomorphism) play an important role in the extension of Formal Language Theory to infinite structures described in finitary ways. Our weighted graphs offer effective descriptions of the above mentioned regular trees and yield decidability results. We also generalize to weighted graphs and their coverings a classical factorization theorem of their characteristic polynomials.

Quasi-trees generalize trees in that the unique "path" between two nodes may be infinite and have any countable order type. They are used to define the rank-width of a countable graph in such a way that it is equal to the least upper-bound of the rank-widths of its finite induced subgraphs. Join-trees are the corresponding directed trees. They are useful to define the modular decomposition of a countable graph. We also consider ordered join-trees, that generalize rooted trees equipped with a linear order on the set of sons of each node. We define algebras with finitely many operations that generate (via infinite terms) these generalized trees. We prove that the associated regular objects (those defined by regular terms) are exactly the ones that are the unique models of monadic second-order sentences. These results use and generalize a similar result by W. Thomas for countable linear orders.

The model-checking problem for monadic second-order logic on graphs is fixed-parameter tractable with respect to tree-width and clique-width. The proof constructs finite deterministic automata from monadic second-order sentences, but this computation produces automata of hyper-exponential sizes, and this is not avoidable. To overcome this difficulty, we propose to consider particular monadic second-order graph properties that are nevertheless interesting for Graph Theory and to interpret automata instead of trying to compile them (joint work with I. Durand). For checking monadic second-order sentences written with edge set quantifications, the appropriate parameter is tree-width. We introduce special tree-width, a graph complexity measure between path-width and tree-width. The corresponding automata are easier to construct than those for tree-width.

This article establishes that the split decomposition of graphs introduced by Cunnigham, is definable in Monadic Second-Order Logic.This result is actually an instance of a more general result covering canonical graph decompositions like the modular decomposition and the Tutte decomposition of 2-connected graphs into 3-connected components. As an application, we prove that the set of graphs having the same cycle matroid as a given 2-connected graph can be defined from this graph by Monadic Second-Order formulas.

Relational structures offer a common framework for handling graphs and hypergraphs of various kinds. Operations like disjoint union, the creation of new relations by means of quantifier-free formulas, and relabellings of relations make it possible to denote them using algebraic expressions. It is known that every monadic second-order property of a structure is verifiable in time proportional to the size of such an algebraic expression defining it. We prove here that this result remains true if we also use in these algebraic expressions a fusion operation that fuses all elements of the domain satisfying some unary predicate. The value mapping from these algebraic expressions to the structures they denote is a monadic second-order definable transduction, which means that the structure is definable inside the tree representing the algebraic expression by monadic second-order formulas. It follows (by using results of other articles) that, with this fusion operation, we cannot generate more graph families, but we can generate them with less unary auxiliary predicates. We also obtain clear-cut characterizations of Vertex Replacement and Hyperedge Replacement context-free graph grammars in terms of four types of operations, amongst which is the fusion of vertices satisfying a specified predicate.

We show that a set of finite graphs of tree-width at most k is recognizable (with respect to the algebra of graphs with an unbounded number of sources) if and only if it is recognizable with respect to the algebra of graphs of tree-width at most k with at most k sources.

The notion of a recognizable set of words, trees or graphs is relative to an algebraic structure on the set of words, trees or graphs respectively. We establish that several algebraic structures yield the same notion of a recognizable set of graphs. This notion is equivalent to that of a fully cutset-regular set of graphs introduced by Fellows and Abrahamson. We also establish that the class of recognizable sets of graphs is closed under the operations considered in these various equivalent definitions. This fact is not a standard consequence of the definition of recognizability.

It is proved that in every undirected graph or, more generally, in every undirected hypergraph of bounded rank, one can specify an orientation of the edges or hyperedges by monadic second-order formulas using quantifications on sets of edges or hyperedges. The proof uses an extension to hypergraphs of the classical notion of a depth-first search spanning tree. Applications are given to the partially open problem of characterizing the classes of graphs (or hypergraphs) having decidable monadic theories, with and without quantifications on sets of edges (or hyperedges).>

article Free Access Share on An algebraic theory of graph reduction Authors: Stefan Arnborg The Royal Institute of Technology, Stockholm, Sweden The Royal Institute of Technology, Stockholm, SwedenView Profile , Bruno Courcelle Bordeaux-1 University, Talence, France Bordeaux-1 University, Talence, FranceView Profile , Andrzej Proskurowski University of Oregon, Eugene, Oregon University of Oregon, Eugene, OregonView Profile , Detlef Seese University of Karlsruhe, Karlsruhe, Germany University of Karlsruhe, Karlsruhe, GermanyView Profile Authors Info & Claims Journal of the ACMVolume 40Issue 5Nov. 1993 pp 1134–1164https://doi.org/10.1145/174147.169807Published:01 November 1993Publication History 88citation1,580DownloadsMetricsTotal Citations88Total Downloads1,580Last 12 Months72Last 6 weeks11 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my Alerts New Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteeReaderPDF

For graphs of degree at most some fixed integer, the same properties can be expressed by monadic second-order formulas with and without quantifications over sets of edges, with and without auxiliary orientations. Similar results hold for partial k-trees for fixed k, and for graphs of tree-width at most k. These results are related to the possibility of testing graph properties in polynomial time for graphs generated by context-free graph-grammars of various types.>

This work presents a unified theory of recursive program schemes, context-free grammars, grammars on arbitrary algebraic structures (and actually of recursive definitions of all kind) in terms of regular systems of equations. Several equivalence relations on regular systems (depending on sets of equational axioms) are defined. They are systematically investigated and characterized (in some cases) in terms of system transformations by folding, unfolding and rewriting according to the equational algebraic laws.

With every language L we associate an increasing function called its rational index. We obtain this function by comparing L with rational languages of increasing complexity. We show that the rational indices of two languages related by a rational transduction are polynomially related. From this, we can define new rational cones of languages in terms of rational indices. We then focus our attention on the rational index of context-free languages and raise several questions closely related to the open problems concerning the subcones of the family of context-free languages.

We examine the possibility of translating an attribute system into a recursive program scheme taking derivation trees as arguments. This is possible if and only if the attribute system is strongly non-circular. The strong non circularity is decidable in polynomial time. Our recursive program schemes allow us to attack the equivalence problem for attribute systems and solve it in a special case properly including the case of purely synthesized systems.

We give conditions on a left-linear Church-Rosser term rewriting system S allowing to define S-normal forms for infinite terms. We obtain a characterization of the S-equivalence of recursive program schemes (i.e. equivalence in all interpretations which validate S considered as a set of axioms). We give sufficient conditions for a recursive program scheme Σ to be S-univocal i.e. to have only one solution up to S-equivalence (considering Σ as a system of equations). For such schemes, we obtain proofs of S-equivalence which do not use any "induction principle". We also consider (SUE)-equivalence where S satisfies the above conditions and E is a set of bilinear equations such that no E-normal form does exist.

To each family C of interpretations corresponds an equivalence relation among program schemes, namely the equivalence of the program schemes for all interpretation of C. A family C is algebraic if any two programs are C-equivalent iff every partial finite computation of one of them is C-equivalent to some partial finite computation of the other. Our main theorem states that a family C is algebraic iff it is represented with respect to the equivalence of programs by a single interpretation (a C-Herbrand interpretation) which is algebraic (in Scott's sense, roughly speaking). We give examples of algebraic and non algebraic families.

Numérisation avec OCR réalisée en 2024. La reconnaissance de caractères du PDF (format PDF/A) peut comporter des erreurs. Pour toutes informations complémentaires et les partages de propriété, merci de contacter le service IES [email protected]