Concept

Logic of graphs

In the mathematical fields of graph theory and finite model theory, the logic of graphs deals with formal specifications of graph properties using sentences of mathematical logic. There are several variations in the types of logical operation that can be used in these sentences. The first-order logic of graphs concerns sentences in which the variables and predicates concern individual vertices and edges of a graph, while monadic second-order graph logic allows quantification over sets of vertices or edges. Logics based on least fixed point operators allow more general predicates over tuples of vertices, but these predicates can only be constructed through fixed-point operators, restricting their power. A sentence may be true for some graphs, and false for others; a graph is said to model , written , if is true of the vertices and adjacency relation of . The algorithmic problem of model checking concerns testing whether a given graph models a given sentence. The algorithmic problem of satisfiability concerns testing whether there exists a graph that models a given sentence. Although both model checking and satisfiability are hard in general, several major algorithmic meta-theorems show that properties expressed in this way can be tested efficiently for important classes of graphs. Other topics of research in the logic of graphs include investigations of the probability that a random graph has a property specified within a particular type of logic, and methods for data compression based on finding logical sentences that are modeled by a unique graph. In the first-order logic of graphs, a graph property is expressed as a quantified logical sentence whose variables represent graph vertices, with predicates for equality and adjacency testing. For instance, the condition that a graph does not have any isolated vertices may be expressed by the sentence where the symbol indicates the undirected adjacency relation between two vertices. This sentence can be interpreted as meaning that for every vertex there is another vertex that is adjacent to .

About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.
Related courses (1)
PHYS-512: Statistical physics of computation
The students understand tools from the statistical physics of disordered systems, and apply them to study computational and statistical problems in graph theory, discrete optimisation, inference and m
Related lectures (1)
Belief Propagation: Key Methods and Analysis
Covers Belief Propagation, a key method for both analysis and algorithm.
Related publications (4)

Satisfiability-Based Methods for Digital Circuit Design, Debug, and Optimization

Andrew James Becker

Designing digital circuits well is notoriously difficult. This difficulty stems in part from the very many degrees of freedom inherent in circuit design, typically coupled with the need to satisfy various constraints. In this thesis, we demonstrate how for ...
EPFL2018

Parameterized Systems in BIP: Design and Model Checking

Joseph Sifakis, Simon Bliudze, Qiang Wang

BIP is a component-based framework for system design that has important industrial applications. BIP is built on three pillars: behavior, interaction, and priority. In this paper, we introduce first-order interaction logic (FOIL) that extends BIP to system ...
Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik2016

Bootstrap Percolation in Power-Law Random Graphs

Léo Hamed Amini

A bootstrap percolation process on a graph is an "infection" process which evolves in rounds. Initially, there is a subset of infected nodes and in each subsequent round each uninfected node which has at least infected neighbours becomes infected and remai ...
Springer2014
Show more
Related concepts (7)
Courcelle's theorem
In the study of graph algorithms, Courcelle's theorem is the statement that every graph property definable in the monadic second-order logic of graphs can be decided in linear time on graphs of bounded treewidth. The result was first proved by Bruno Courcelle in 1990 and independently rediscovered by . It is considered the archetype of algorithmic meta-theorems.
Monadic second-order logic
In mathematical logic, monadic second-order logic (MSO) is the fragment of second-order logic where the second-order quantification is limited to quantification over sets. It is particularly important in the logic of graphs, because of Courcelle's theorem, which provides algorithms for evaluating monadic second-order formulas over graphs of bounded treewidth. It is also of fundamental importance in automata theory, where the Büchi–Elgot–Trakhtenbrot theorem gives a logical characterization of the regular languages.
Model checking
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems, where the specification contains liveness requirements (such as avoidance of livelock) as well as safety requirements (such as avoidance of states representing a system crash). In order to solve such a problem algorithmically, both the model of the system and its specification are formulated in some precise mathematical language.
Show more

Graph Chatbot

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.