Optimised determinisation and completion of finite tree automata

John P. Gallagher, Mai Lise Ajspur, Bishoksan Kafle

Publikation: Artikel i tidsskrift og konference artikel i tidsskriftTidsskriftartikelForskningpeer review

Abstrakt

Determinisation and completion of finite tree automata are important operations with applications in program analysis and verification. However, the complexity of the classical procedures for determinisation and completion is high. They are not practical procedures for manipulating tree automata beyond very small ones. In this paper we develop an algorithm for determinisation and completion of finite tree automata, whose worst-case complexity remains unchanged, but which performs far better than existing algorithms in practice. The critical aspect of the algorithm is that the transitions of the determinised (and possibly completed) automaton are generated in a potentially very compact form called product form, which can reduce the size of the representation dramatically. Furthermore, the representation can often be used directly when manipulating the determinised automaton. The paper contains an experimental evaluation of the algorithm on a large set of tree automata examples.
OriginalsprogEngelsk
TidsskriftJournal of Logical and Algebraic Methods in Programming
Vol/bind95
Sider (fra-til)1-16
ISSN2352-2208
DOI
StatusUdgivet - jan. 2018

Fingeraftryk

Dyk ned i forskningsemnerne om 'Optimised determinisation and completion of finite tree automata'. Sammen danner de et unikt fingeraftryk.

Citationsformater