# Autograph is now part of TRAG

## What is Autograph

Autograph is a project carried out at the LaBRI (Laboratoire Bordelais de Recherche en Informatique) at the University of Bordeaux. Autograph is an experimental tool written in Common Lisp for verifying properties of graphs of bounded clique-width. It is written in Steele Bank Common Lisp ( SBCL). It uses the Autowrite library which provides the operations needed to create and manipulate automata. The following famous theorem connects the problem of verifying graph properties with term automata.

Theorem
Monadic second-order model checking is for tree-width [Courcelle (1990)]
and clique-width [Courcelle, Makowski, Rotics (2001)].

Tree-width and clique-width are graph complexity measures based on graph decompositions. A decomposition produces a term representation of the graph. For a graph property expressed in monadic second order logic (MSO), the algorithm verifying the property takes the form of a term automaton which recognizes the terms denoting graphs satisfying the property.

## Main features of Autograph

Basic automata for graph properties
• Singleton()
• edge(X1,X2)
• subset(X1,X2)
• equality(X1,X2)
Polynomial
• Stable()
• Partition(X1,...Xn)
• k-cardinality()
Non polynomial
• k-Coloring(C1,...,Cn) compilable up to cwd=4 (for k=3)
• Connectedness() compilable up to cwd=3
• Clique() compilable up to cwd=4
• Path(X1,X2) compilable up to cwd=4
• Acyclic() not compilable
Combination of previous automata (non polynomial)
• k-Colorability() compilable up to k=3 (cwd=2), k=2 (cwd=3)
• Acyclic-Colorability() not compilable (uses Acyclic)
• k-Chord-Free-Cycle()
• k-Max-Degre()
• k-Vertex-Cover()
• Composition of automata
• homomorphisms and inverse-homomorphisms
• determinization
• reduction and minimization (for table-automata only)
• boolean operations (union, intersection, complementation)

## Obtaining Autograph

Autograph is now part if the TRAG project (Term Rewriting Automata and Graphs) available on BitBucket:
` git clone https://idurand@bitbucket.org/idurand/trag.git `

## Bibliography

B. Courcelle. Graph Structure and Monadic Second-Order Logic. 2011
Cambridge University Press

B. Courcelle and I. Durand. Verifying monadic second order graph properties with tree automata. Proceedings of the 3rd European Lisp Symposium, pages 7-21, 2010
I. Durand. Implementing huge term automata. Submitted to the 4th European Lisp Symposium, 2011.

## Pointers to relevant sites

Here are some pointers to other sites with similar interests, listed by topic.

### Sites and people

Steele Bank Common Lisp (SBCL)
Irčne Durand
Bruno Courcelle