Optimised determinisation and completion of finite tree automata

John Patrick Gallagher, Mai Ajspur, Bishoksan Kafle

Research output: Contribution to journalJournal articleResearchpeer-review

Abstract

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.
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.
LanguageEnglish
JournalJournal of Logic and Algebraic Programming
Volume95
Pages1-16
ISSN1567-8326
DOIs
StatePublished - Jan 2018

Keywords

  • finite tree automata
  • Algorithms

Cite this

@article{e06480f8b32041c09b6a50ed3570b147,
title = "Optimised determinisation and completion of finite tree automata",
abstract = "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.",
keywords = "finite tree automata, Algorithms",
author = "Gallagher, {John Patrick} and Mai Ajspur and Bishoksan Kafle",
year = "2018",
month = "1",
doi = "10.1016/j.jlamp.2017.10.004",
language = "English",
volume = "95",
pages = "1--16",
journal = "Journal of Logic and Algebraic Programming",
issn = "1567-8326",
publisher = "Elsevier BV North-Holland",

}

Optimised determinisation and completion of finite tree automata. / Gallagher, John Patrick; Ajspur, Mai; Kafle, Bishoksan.

In: Journal of Logic and Algebraic Programming, Vol. 95, 01.2018, p. 1-16.

Research output: Contribution to journalJournal articleResearchpeer-review

TY - JOUR

T1 - Optimised determinisation and completion of finite tree automata

AU - Gallagher,John Patrick

AU - Ajspur,Mai

AU - Kafle,Bishoksan

PY - 2018/1

Y1 - 2018/1

N2 - 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.

AB - 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.

KW - finite tree automata

KW - Algorithms

U2 - 10.1016/j.jlamp.2017.10.004

DO - 10.1016/j.jlamp.2017.10.004

M3 - Journal article

VL - 95

SP - 1

EP - 16

JO - Journal of Logic and Algebraic Programming

T2 - Journal of Logic and Algebraic Programming

JF - Journal of Logic and Algebraic Programming

SN - 1567-8326

ER -