Decidability and Expressiveness of Finitely Representable ...
Reference
H.J. Sander Bruggink and Mathias Hülsbusch. Decidability and expressiveness of finitely representable recognizable graph languages. In Proceedigs of GT-VMT 2011, Electronic Communications of the EASST, 2011.
Abstract
Recognizable graph languages are a generalization of regular (word) languages to graphs (as well as arbitrary categories). Recently automaton functors were proposed as acceptors of recognizable graph languages. They promise to be a useful tool for the verification of dynamic systems, for example for invariant checking. Since automaton functors may contain an infinite number of finite state sets, one must restrict to finitely representable ones for implementation reasons. In this paper we take into account two such finite representations: primitive recursive automaton functors – in which the automaton functor can be constructed on-the-fly by a primitive recursive function –, and bounded automaton functors – in which the interface size of the graphs (cf. path width) is bounded, so that the automaton functor can be explicitly represented. We show that the language classes of both kinds of automaton functor are closed under boolean operations, and compare the expressiveness of the two paradigms with hyperedge replacement grammars. In addition we show that the emptiness and equivalence problem are decidable for bounded automaton functors, but undecidable for primitive recursive automaton functors.
Suggested BibTeX entry:
@inproceedings{bh:recprops11,
author = {H.J. Sander Bruggink and Mathias H{\"u}lsbusch},
booktitle = {Proceedigs of GT-VMT 2011},
series = {Electronic Communications of the EASST},
title = {Decidability and Expressiveness of Finitely Representable Recognizable Graph Languages},
year = {2011}
}
