Show simple item record

dc.contributor.advisorMayr, Richard
dc.contributor.advisorEtessami, Kousha
dc.contributor.authorAlmeida, Ricardo Manuel de Oliveira
dc.date.accessioned2018-03-13T12:01:34Z
dc.date.available2018-03-13T12:01:34Z
dc.date.issued2017-11-30
dc.identifier.urihttp://hdl.handle.net/1842/28794
dc.description.abstractWe present PTIME language-preserving techniques for the reduction of non-deterministic tree automata, both for the case of finite trees and for infinite trees. Our techniques are based on new transition removing and state merging results, which rely on binary relations that compare the downward and upward behaviours of states in the automaton. We use downward/upward simulation preorders and the more general but EXPTIME-complete trace inclusion relations, for which we introduce good under-approximations computable in polynomial time. We provide a complete picture of combinations of downward and upward simulation/trace inclusions which can be used in our reduction techniques. We define an algorithm that puts together all the reduction results found for finite trees, and implemented it under the name minotaut, a tool built on top of the well-known tree automata library libvata. We tested minotaut on large collections of automata from program verification provenience, as well as on different classes of randomly generated automata. Our algorithm yields substantially smaller and sparser automata than all previously known reduction techniques, and it is still fast enough to handle large instances. Taking reduction of automata on finite trees one step further, we then introduce saturation, a technique that consists of adding new transitions to an automaton while preserving its language. We implemented this technique on minotaut and we show how it can make subsequent state-merge and transition-removal operations more effective. Thus we obtain a PTIME algorithm that reduces the number of states of tree automata even more than before. Additionally, we explore how minotaut alone can play an important role when performing hard operations like complementation, allowing to obtain smaller complement automata and at lower computation times overall. We then show how saturation can extend this contribution even further. An overview of the tool, highlighting some of its implementation features, is presented as well.en
dc.contributor.sponsorEngineering and Physical Sciences Research Council (EPSRC)en
dc.language.isoenen
dc.publisherThe University of Edinburghen
dc.relation.hasversionRicardo Almeida, Luk´as Hol´ık, and Richard Mayr. Reduction of nondeterministic tree automata. In Marsha Chechik and Jean-Franc¸ois Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd International Conference, TACAS 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings, volume 9636 of Lecture Notes in Computer Science, pages 717–735. Springer, 2016.en
dc.relation.hasversionR. Almeida. MinOTAut. https://github.com/ric-almeida/ heavy-minotaut, 2016.en
dc.relation.hasversionRicardo Almeida. Reducing nondeterministic tree automata by adding transitions. In Jan Bouda, Luk´as Hol´ık, Jan Kofron, Jan Strejcek, and Adam Rambousek, editors, Proceedings 11th Doctoral Workshop on Mathematical and Engineering Methods in Computer Science, MEMICS 2016, Telˇc, Czech Republic, 21st-23rd October 2016., volume 233 of EPTCS, pages 33–51, 2016.en
dc.subjectautomataen
dc.subjectalgorithmsen
dc.subjectreductionen
dc.subjectefficienten
dc.titleEfficient algorithms for hard problems in nondeterministic tree automataen
dc.typeThesis or Dissertationen
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen


Files in this item

This item appears in the following Collection(s)

Show simple item record