Fly-Automata, Their Properties and Applications

摘要

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.