|
Version (January 2011) of Autograph is available!
|
|
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
Sources with ASDF files of current release (1.0): Autograph.tgz
Current sources with ASDF files: Autograph
Contact information
Should you have any comments or suggestions regarding Autograph,
or ideas on new functionalities that you would like to see in future
releases of Autograph, please send them to
idurand@labri.fr.
Other Releases
Bibliography
B. Courcelle.
Graph Structure and Monadic Second-Order Logic. 2009
To be published by 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