Practical verification of MSO properties of graphs of bounded clique width

Irène Durand

Description

Practical verification of MSO properties of graphs of bounded clique-width Irene Durand (joint work with Bruno Courcelle) LaBRI, Universite de Bordeaux 20 Octobre 2010 Decompositions de graphes, theorie, algorithmes et logiques, 2010

• clique


• width properties


• graph properties


• properties like


• only ?


• free undirected graphs


• finite graphs


• graph theory

Sujets

• Durand
• Courcelle
• Clique
• Graph property
• Graph theory

Informations

• Publié par: pefav
• Publié le: 01 octobre 2010
• Nombre de lectures: 37
• Langue: English

Extrait

Practical verification of MSO properties of graphs of bounded clique-width

Ire`neDurand(jointworkwithBrunoCourcelle)

LaBRI,Universite´deBordeaux

20 Octobre 2010

D´ecompositionsdegraphes,the´orie,algorithmesetlogiques,2010

Objectives

/233

Verify properties of graphs of bounded clique-width

Properties ◮ connectedness, ◮ k-colorability, ◮ existence of cycles ◮ existence of paths ◮ bounds (cardinality, degree, . . . ) ◮    How: usingterm automata

Note that we considerfinitegraphs only

Graphs as relational structures

3/33

For simplicity, we considersimple,loop-free undirectedgraphs Extensionsare easy Every graphGcan be identified with therelational structure (V G edg G ) whereV G is the set of vertices andedg G ⊆ V G × V G the binary symmetric relation that defines edges.

v 8

v 7 v 6 v 2

v 1

v 3

v 5 v 4 V G ={v 1 v 2 v 3 v 4 v 5 v 6 v 7 v 8 } edg G ={(v 1 v 2 )(v 1 v 4 )(v 1 v 5 )(v 1 v 7 )(v 2 v 3 )(v 2 v 6 ) (v 3 v 4 )(v 4 v 5 )(v 5 v 8 )(v 6 v 7 )(v 7 v 8 )}