Efficient Symbolic Implementation of Graph Automata with Applications ...


Christoph Blume, H.J. Sander Bruggink, Dominik Engelke, and Barbara König. Efficient symbolic implementation of graph automata with applications to invariant checking. In Proceedings of ICGT 2012, 2012.


We introduce graph automata as a more automata-theoretic view on (bounded) automaton functors and we present how automaton-based techniques can be used for invariant checking in graph transformation systems. Since earlier related work on graph automata suffered from the explosion of the size of the automata and the need of approximations due to the non-determinism of the automata, we here employ symbolic BDD-based techniques and recent antichain algorithms for language inclusion to overcome these issues. We have implemented techniques for generating, manipulating and analyzing graph automata and perform an experimental evaluation.

Suggested BibTeX entry:

    author = {Christoph Blume and H.J. Sander Bruggink and Dominik Engelke and Barbara K{\"o}nig},
    booktitle = {Proceedings of ICGT 2012},
    title = {Efficient Symbolic Implementation of Graph Automata with Applications to Invariant Checking},
    year = {2012}

PDF (428 kB)
© University of Duisburg-Essen, Theoretical Computer Science group