Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userMSO Undecidability for some Hereditary Classes of Unbounded Clique-Width
82
0
0.0
(
0
)
Added by
Abhisekh Sankaran
Publication date
2020
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Seeses conjecture for finite graphs states that monadic second-order logic (MSO) is undecidable on all graph classes of unbounded clique-width. We show that to establish this it would suffice to show that grids of unbounded size can be interpreted in two families of graph classes: minimal hereditary classes of unbounded clique-width; and antichains of unbounded clique-width under the induced subgraph relation. We explore a number of known examples of the former category and establish that grids of unbounded size can indeed be interpreted in them.
rate research
Read More
The finite satisfiability problem of monadic second order logic is decidable only on classes of structures of bounded tree-width by the classic result of Seese (1991). We prove the following problem is decidable: Input: (i) A monadic second order logic sentence $alpha$, and (ii) a sentence $beta$ in the two-variable fragment of first order logic extended with counting quantifiers. The vocabularies of $alpha$ and $beta$ may intersect. Output: Is there a finite structure which satisfies $alphalandbeta$ such that the restriction of the structure to the vocabulary of $alpha$ has bounded tree-width? (The tree-width of the desired structure is not bounded.) As a consequence, we prove the decidability of the satisfiability problem by a finite structure of bounded tree-width of a logic extending monadic second order logic with linear cardinality constraints of the form $|X_{1}|+cdots+|X_{r}|<|Y_{1}|+cdots+|Y_{s}|$, where the $X_{i}$ and $Y_{j}$ are monadic second order variables. We prove the decidability of a similar extension of WS1S.
Given a clique-width $k$-expression of a graph $G$, we provide $2^{O(k)}cdot n$ time algorithms for connectivity constraints on locally checkable properties such as Node-Weighted Steiner Tree, Connected Dominating Set, or Connected Vertex Cover. We also propose a $2^{O(k)}cdot n$ time algorithm for Feedback Vertex Set. The best running times for all the considered cases were either $2^{O(kcdot log(k))}cdot n^{O(1)}$ or worse.
Graph polynomials which are definable in Monadic Second Order Logic (MSOL) on the vocabulary of graphs are Fixed-Parameter Tractable (FPT) with respect to clique-width. In contrast, graph polynomials which are definable in MSOL on the vocabulary of hypergraphs are fixed-parameter tractable with respect to tree-width, but not necessarily with respect to clique width. No algorithmic meta-theorem is known for the computation of graph polynomials definable in MSOL on the vocabulary of hypergraphs with respect to clique-width. We define an infinite class of such graph polynomials extending the class of graph polynomials definable in MSOL on the vocabulary of graphs and prove that they are Fixed-Parameter Polynomial Time (FPPT) computable, i.e. that they can be computed in time $O(n^{f(k)})$, where $n$ is the number of vertices and $k$ is the clique-width.
We investigate the parameterized complexity of finding subgraphs with hereditary properties on graphs belonging to a hereditary graph class. Given a graph $G$, a non-trivial hereditary property $Pi$ and an integer parameter $k$, the general problem $P(G,Pi,k)$ asks whether there exists $k$ vertices of $G$ that induce a subgraph satisfying property $Pi$. This problem, $P(G,Pi,k)$ has been proved to be NP-complete by Lewis and Yannakakis. The parameterized complexity of this problem is shown to be W[1]-complete by Khot and Raman, if $Pi$ includes all trivial graphs but not all complete graphs and vice versa; and is fixed-parameter tractable (FPT), otherwise. As the problem is W[1]-complete on general graphs when $Pi$ includes all trivial graphs but not all complete graphs and vice versa, it is natural to further investigate the problem on restricted graph classes. Motivated by this line of research, we study the problem on graphs which also belong to a hereditary graph class and establish a framework which settles the parameterized complexity of the problem for various hereditary graph classes. In particular, we show that: $P(G,Pi,k)$ is solvable in polynomial time when the graph $G$ is co-bipartite and $Pi$ is the property of being planar, bipartite or triangle-free (or vice-versa). $P(G,Pi,k)$ is FPT when the graph $G$ is planar, bipartite or triangle-free and $Pi$ is the property of being planar, bipartite or triangle-free, or graph $G$ is co-bipartite and $Pi$ is the property of being co-bipartite. $P(G,Pi,k)$ is W[1]-complete when the graph $G$ is $C_4$-free, $K_{1,4}$-free or a unit disk graph and $Pi$ is the property of being either planar or bipartite.
In this work we provide algorithmic solutions to five fundamental problems concerning the verification, synthesis and correction of concurrent systems that can be modeled by bounded p/t-nets. We express concurrency via partial orders and assume that behavioral specifications are given via monadic second order logic. A c-partial-order is a partial order whose Hasse diagram can be covered by c paths. For a finite set T of transitions, we let P(c,T,phi) denote the set of all T-labelled c-partial-orders satisfying phi. If N=(P,T) is a p/t-net we let P(N,c) denote the set of all c-partially-ordered runs of N. A (b, r)-bounded p/t-net is a b-bounded p/t-net in which each place appears repeated at most r times. We solve the following problems: 1. Verification: given an MSO formula phi and a bounded p/t-net N determine whether P(N,c)subseteq P(c,T,phi), whether P(c,T,phi)subseteq P(N,c), or whether P(N,c)cap P(c,T,phi)=emptyset. 2. Synthesis from MSO Specifications: given an MSO formula phi, synthesize a semantically minimal (b,r)-bounded p/t-net N satisfying P(c,T,phi)subseteq P(N, c). 3. Semantically Safest Subsystem: given an MSO formula phi defining a set of safe partial orders, and a b-bounded p/t-net N, possibly containing unsafe behaviors, synthesize the safest (b,r)-bounded p/t-net N whose behavior lies in between P(N,c)cap P(c,T,phi) and P(N,c). 4. Behavioral Repair: given two MSO formulas phi and psi, and a b-bounded p/t-net N, synthesize a semantically minimal (b,r)-bounded p/t net N whose behavior lies in between P(N,c) cap P(c,T,phi) and P(c,T,psi). 5. Synthesis from Contracts: given an MSO formula phi^yes specifying a set of good behaviors and an MSO formula phi^no specifying a set of bad behaviors, synthesize a semantically minimal (b,r)-bounded p/t-net N such that P(c,T,phi^yes) subseteq P(N,c) but P(c,T,phi^no ) cap P(N,c)=emptyset.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
