Efficient Implementation of Automaton Functors for the Verification of Graph Transformation Systems

2015/11/03 by Christoph Blume, Blume, Christoph
Computer Science · #Formal Methods in Verification #Model-Driven Software Engineering Techniques #Logic, programming, and type systems

paper · doi:10.14279/tuj.eceasst.38.572

Abstract

In this paper we show new applications for recognizable graph languages to invariant checking. Furthermore we present details about techniques we used for an implementation of a tool suite for (finite) automaton functors which generalize finite automata to the setting of recognizable (graph) languages. In order to develop an efficient implementation we take advantage of Binary Decision Diagrams (BDDs).

Related

• Decidability and Expressiveness of Finitely Representable Recognizable Graph Languages
• Recognizable Graph Languages for Checking Invariants
• Fly-automata, model-checking and recognizability
• Systems of Graph Formulas and their Equivalence to Alternating Graph Automata
• Computations by fly-automata beyond monadic second-order logic