Abstrakt. I den här artikeln presenterar vi VATA, ett mångsidigt och effektivt open-source trädautomata bibliotek tillämpligt, t.ex., i formell verifiering. Biblioteket stöder både explicit och semi-symbolisk kodning av icke-deterministiska ändliga trädautomata och ger ett effektivt genomförande av standardoperationer på båda. Den semi-symboliska kodningen är avsedd för trädautomata med stora alfabet. För att lagra deras övergångsfunktioner används ett nyligen implementerat MTBDD-bibliotek. För att möjliggöra det bredaste möjliga utbudet av applikationer i biblioteket även för semi-symbolisk kodning, tillhandahåller vi både nedifrån-och-upp och uppifrån-och-ned semi-symboliska representationer. Biblioteket implementerar flera högoptimerade reduktionsalgoritmer baserade på simuleringar nedåt och uppåt samt algoritmer för att testa automatisk inkludering baserad på uppåt och nedåt antikedjor och simuleringar. Vi jämför algoritmernas prestanda på en uppsättning testfall och vi jämför även prestandan hos VATA med våra tidigare implementeringar av trädautomata.
VATA REF ] är ett trädautomat bibliotek för att analysera trädspråk över stora alfabet.
VATA: a library for efficient manipulation of non-deterministic tree automata
{'venue': 'TACAS', 'journal': None, 'mag_field_of_study': ['Computer Science']}