scholarly journals Twin-width I: Tractable FO Model Checking

2022 ◽  
Vol 69 (1) ◽  
pp. 1-46
Author(s):  
Édouard Bonnet ◽  
Eun Jung Kim ◽  
Stéphan Thomassé ◽  
Rémi Watrigant

Inspired by a width invariant defined on permutations by Guillemot and Marx [SODA’14], we introduce the notion of twin-width on graphs and on matrices. Proper minor-closed classes, bounded rank-width graphs, map graphs, K t -free unit d -dimensional ball graphs, posets with antichains of bounded size, and proper subclasses of dimension-2 posets all have bounded twin-width. On all these classes (except map graphs without geometric embedding) we show how to compute in polynomial time a sequence of d -contractions , witness that the twin-width is at most d . We show that FO model checking, that is deciding if a given first-order formula ϕ evaluates to true for a given binary structure G on a domain D , is FPT in |ϕ| on classes of bounded twin-width, provided the witness is given. More precisely, being given a d -contraction sequence for G , our algorithm runs in time f ( d ,|ϕ |) · |D| where f is a computable but non-elementary function. We also prove that bounded twin-width is preserved under FO interpretations and transductions (allowing operations such as squaring or complementing a graph). This unifies and significantly extends the knowledge on fixed-parameter tractability of FO model checking on non-monotone classes, such as the FPT algorithm on bounded-width posets by Gajarský et al. [FOCS’15].

Author(s):  
Erik D. Demaine ◽  
Fedor V. Fomin ◽  
Mohammad Taghi Hajiaghayi ◽  
Dimitrios M. Thilikos

Author(s):  
Francesco Belardinelli ◽  
Andreas Herzig

We introduce a first-order extension of dynamic logic (FO-DL), suitable to represent and reason about the behaviour of Data-aware Systems (DaS), which are systems whose data content is explicitly exhibited in the system’s description. We illustrate the expressivity of the formal framework by modelling English auctions as DaS, and by specifying relevant properties in FO-DL. Most importantly, we develop an abstraction-based verification procedure, thus proving that the model checking problem for DaS against FO-DL is actually decidable, provided some mild assumptions on the interpretationdomain.


Author(s):  
Jürgen Bohn ◽  
Werner Damm ◽  
Orna Grumberg ◽  
Hardi Hungar ◽  
Karen Laster
Keyword(s):  

2005 ◽  
Vol 1 (1) ◽  
pp. 33-47 ◽  
Author(s):  
Erik D. Demaine ◽  
Fedor V. Fomin ◽  
Mohammadtaghi Hajiaghayi ◽  
Dimitrios M. Thilikos

2011 ◽  
Vol 474-476 ◽  
pp. 924-927 ◽  
Author(s):  
Xiao Xin

Given an undirected graph G=(V, E) with real nonnegative weights and + or – labels on its edges, the correlation clustering problem is to partition the vertices of G into clusters to minimize the total weight of cut + edges and uncut – edges. This problem is APX-hard and has been intensively studied mainly from the viewpoint of polynomial time approximation algorithms. By way of contrast, a fixed-parameter tractable algorithm is presented that takes treewidth as the parameter, with a running time that is linear in the number of vertices of G.


Author(s):  
Jan van den Heuvel ◽  
Stephan Kreutzer ◽  
Michal Pilipczuk ◽  
Daniel A. Quiroz ◽  
Roman Rabinovich ◽  
...  

Sign in / Sign up

Export Citation Format

Share Document