Detail výsledku
Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata
HOLÍK, L.; VOJNAR, T.; BOUAJJANI, A.; HABERMEHL, P.; TOUILI, T. Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata. Implementation and Application of Automata. Lecture Notes in Computer Science. Berlin: Springer Verlag, 2008. p. 57-67. ISBN: 978-3-540-70843-8.
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Holík Lukáš, doc. Mgr., Ph.D., FIT (FIT), UITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Bouajjani Ahmed
Habermehl Peter
Touili Tayssir, Dr., Ph.D.
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Bouajjani Ahmed
Habermehl Peter
Touili Tayssir, Dr., Ph.D.
Abstrakt
We propose new antichain-based algorithms for
checking universality and inclusion of nondeterministic tree automata (NTA).
We have
implemented these algorithms in a prototype tool and our experiments
show that they provide a significant improvement over the traditional
determinisation-based approaches. We use our
antichain-based inclusion checking algorithm to build an abstract regular tree
model checking framework based entirely on NTA. We
show the significantly improved efficiency of this framework through a series of experiments with verifying various programs over dynamic linked tree-shaped data structures.
Klíčová slova
unversality, tree automata, antichain, abstract regular tree model checking
Rok
2008
Strany
57–67
Sborník
Implementation and Application of Automata
Řada
Lecture Notes in Computer Science
Svazek
5148
Konference
13th International Conference on Implementation and Application of Automata -- CIAA'08
ISBN
978-3-540-70843-8
Vydavatel
Springer Verlag
Místo
Berlin
BibTeX
@inproceedings{BUT34275,
author="Lukáš {Holík} and Tomáš {Vojnar} and Ahmed {Bouajjani} and Peter {Habermehl} and Tayssir {Touili}",
title="Antichain-based Universality and Inclusion Testing over Nondeterministic Finite Tree Automata",
booktitle="Implementation and Application of Automata",
year="2008",
series="Lecture Notes in Computer Science",
volume="5148",
pages="57--67",
publisher="Springer Verlag",
address="Berlin",
isbn="978-3-540-70843-8"
}
Projekty
Integrovaný přístup k výchově studentů DSP v oblasti paralelních a distribuovaných systémů, GAČR, Doktorské granty, GD102/05/H050, zahájení: 2005-01-01, ukončení: 2008-12-31, ukončen
Pokročilé formální přístupy v návrhu a automatické verifikaci počítačových systémů, GAČR, Standardní projekty, GA102/07/0322, zahájení: 2007-01-01, ukončení: 2009-12-31, ukončen
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení
Pokročilé formální přístupy v návrhu a automatické verifikaci počítačových systémů, GAČR, Standardní projekty, GA102/07/0322, zahájení: 2007-01-01, ukončení: 2009-12-31, ukončen
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení
Výzkumné skupiny
Pracoviště
Ústav inteligentních systémů
(UITS)