×

Fly-automata, their properties and applications. (English) Zbl 1297.68117

Bouchou-Markhoff, Béatrice (ed.) et al., Implementation and application of automata. 16th international conference, CIAA 2011, Blois, France, July 13–16, 2011. Proceedings. Berlin: Springer (ISBN 978-3-642-22255-9/pbk). Lecture Notes in Computer Science 6807, 264-272 (2011).
Summary: We address the concrete problem of implementing huge bottom-up term automata. Such automata arise from the verification of Monadic Second Order propositions on graphs of bounded tree-width or clique-width. This applies to graphs of bounded tree-width because bounded tree-width implies bounded clique-width. An automaton which has so many transitions that they cannot be stored in a transition table is represented be a fly-automaton in which the transition function is represented by a finite set of meta-rules.
Fly-automata have been implemented inside the Autowrite software and experiments have been run in the domain of graph model checking.
For the entire collection see [Zbl 1218.68010].

MSC:

68Q45 Formal languages and automata
03D05 Automata and formal grammars in connection with logical questions
68Q42 Grammars and rewriting systems
68Q60 Specification and verification (program logics, model checking, etc.)

Software:

Autowrite
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications, draft (2002), http://tata.gforge.inria.fr
[2] Courcelle, B., Durand, I.: Verifying monadic second order graph properties with tree automata. In: Proceedings of the 3rd European Lisp Symposium, pp. 7–21 (May 2010)
[3] Courcelle, B., Durand, I.: Automata for the verification of monadic second-order graph properties (2011) (in preparation) · Zbl 1285.03049
[4] Courcelle, B., Engelfriet, J.: Graph structure and monadic second-order logic, a language theoretic approach. Cambridge University Press, Cambridge (2011), http://www.labri.fr/perso/courcell/Book/CourGGBook.pdf · Zbl 1257.68006
[5] Durand, I.: Autowrite: A tool for term rewrite systems and tree automata. Electronics Notes in Theorical Computer Science 124, 29–49 (2005) · Zbl 1272.68178
[6] Durand, I.: Implementing huge term automata. In: Proceedings of the 4th European Lisp Symposium, pp. 17–27 (March 2011)
[7] Thatcher, J., Wright, J.: Generalized finite automata theory with an application to a decision problem of second-order logic. Mathematical Systems Theory 2, 57–81 (1968) · Zbl 0157.02201
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.