NDLI: Model Checking for Successor-Invariant First-Order Logic on Minor-Closed Graph Classes

Please wait, while we are loading the content...

[Title page iii]

[Copyright notice]

Conference Organization

List of Additional Reviewers

LICS: Logic in Computer Security -- Some Attacker's Models and Related Decision Problems

From Qualitative to Quantitative Proofs of Security Properties Using First-Order Conditional Logic

Duality in Logic and Computation

Timed and Probabilistic I/O Automata

Regular Functions and Cost Register Automata

Presburger Vector Addition Systems

Reasoning about Data Repetitions with Counter Systems

On the Context-Freeness Problem for Vector Addition Systems

Groupoids, Hypergraphs, and Symmetries in Finite Models

An Optimal Gaifman Normal Form Construction for Structures of Bounded Degree

Two-Variable Logic with Counting and Trees

Measurable Spaces and Their Effect Logic

Topological Structure of Quantum Algorithms

On the Query Complexity of Real Functionals

Quantitative Monadic Second-Order Logic

Magnitude Monadic Logic over Words and the Use of Relative Internal Set Theory

Quantitative Reasoning for Proving Lock-Freedom

Model Checking for Successor-Invariant First-Order Logic on Minor-Closed Graph Classes

Dynamic Logic of Propositional Assignments: A Well-Behaved Variant of PDL

Model-Checking Parse Trees

The Complexity of Model Checking Multi-stack Systems

Maximum Matching and Linear Programming in Fixed-Point Logic with Counting

Turing Machines with Atoms

Adding an Equivalence Relation to the Interval Logic ABB: Complexity and Expressiveness

Decidability of Weak Simulation on One-Counter Nets

Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes

Calculating the Fundamental Group of the Circle in Homotopy Type Theory

Type-Based Productivity of Stream Definitions in the Calculus of Constructions

Fibred Data Types

Arbitrary Action Model Logic and Action Model Synthesis

On the Boundary of Behavioral Strategies

A Relatively Complete Generic Hoare Logic for Order-Enriched Effects

Unifying Classical and Intuitionistic Logics for Computational Control

The Cost of Usage in the ?-Calculus

Weighted Relational Models of Typed Lambda-Calculi

Atomic Lambda Calculus: A Typed Lambda-Calculus with Explicit Sharing

Stone Duality for Markov Processes

Trading Performance for Stability in Markov Decision Processes

Solving Partial-Information Stochastic Parity Games

Expressive Completeness for Metric Temporal Logic

One-Path Reachability Logic

Substructure Temporal Logic

Name-Passing Calculi: From Fusions to Preorders and Types

A Compositional Semantics for the Reversible p-Calculus

Pumping by Typing

From Frame Properties to Hypersequent Rules in Modal Logics

The Logic of Exact Covers: Completeness and Uniform Interpolation

Compressing Polarized Boxes

Kripke Semantics for Modal Bilattice Logic

Forcing MSO on Infinite Words in Weak MSO

From Monadic Second-Order Definable String Transformations to Transducers

From Two-Way to One-Way Finite State Transducers

A Characterization Theorem for the Alternation-Free Fragment of the Modal µ-Calculus

Bisimilarity of Pushdown Automata is Nonelementary

Rabin-Mostowski Index Problem: A Step beyond Deterministic Automata

Regular Real Analysis

Instances of Computational Effects: An Algebraic Perspective

Multiversal Polymorphic Algebraic Theories: Syntax, Semantics, Translations, and Equational Logic

A Categorical Treatment of Ornaments

Converging to the Chase -- A Tool for Finite Controllability

Why is it Hard to Obtain a Dichotomy for Consistent Query Answering?

Abstract Machines for Game Semantics, Revisited

[Publisher's information]

Model Checking for Successor-Invariant First-Order Logic on Minor-Closed Graph Classes

Content Provider	ACM Digital Library
Author	Kawarabayashi, Ken-Ichi Kreutzer, Stephan Eickmeyer, Kord
Abstract	Model checking problems for first- and monadic second-order logic on graphs have received considerable attention in the past, not the least due to their connections to problems in algorithmic graph structure theory. While the model checking problem for these logics on general graphs is computationally intractable, it becomes tractable on important classes of graphs such as those of bounded tree-width, planar graphs or more generally, classes of graphs excluding a fixed minor. It is well known that allowing an order relation or successor function can greatly increase the expressive power of the respective logics. This remains true even in cases where we require the formulas to be order- or successor-invariant, that is, while they can use an order relation, their truth in a given graph must not depend on the particular ordering or successor function chosen. Naturally, the question arises whether this increase in expressive power comes at a cost in terms of tractability on specific classes of graphs. In LICS 2012, Engel Mann et al. studied this problem and showed that order-invariant monadic second-order logic (MSO) remains tractable on the same classes of graphs than MSO without an ordering. That is, adding order-invariance to MSO essentially comes at no extra cost in terms of model checking complexity. For successor-invariant first-order logic something similar should be true. However, they only managed to show that successor-invariant first-order logic is tractable on the class of planar graphs which is very far from the best tractability results currently known for first-order logic. In this paper we significantly improve the latter result and show that successor-invariant first-order logic is tractable on any class of graphs excluding a fixed minor. This is much closer to the best results known for FO without an ordering. The proof relies on the construction of k-walks in suitable super graphs of the input graphs, i.e., walks which visit every vertex at least once and at most k times, for some k depending on the excluded minor H. The super graphs may in general contain H minors, but they still exclude some possible larger minorH0, so by results of Flum and Grohe [20] model checking on these graphs is still fixed-parameter tractable.
Starting Page	134
Ending Page	142
Page Count	9
File Format	PDF
ISBN	9780769550206
ISSN	10436871
DOI	10.1109/LICS.2013.19
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2013-06-25
Access Restriction	Subscribed
Content Type	Text
Resource Type	Article
Subject	Software Mathematics

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in