Show simple item record

dc.contributor.advisorMayr, Richard
dc.contributor.advisorEtessami, Kousha
dc.contributor.authorClemente, Lorenzo
dc.date.accessioned2012-08-07T14:11:00Z
dc.date.available2012-08-07T14:11:00Z
dc.date.issued2012-06-25
dc.identifier.urihttp://hdl.handle.net/1842/6215
dc.description.abstractFinite-state automata are a central computational model in computer science, with numerous and diverse applications. In one such application, viz. model-checking, automata over infinite words play a central rˆole. In this thesis, we concentrate on B¨uchi automata (BA), which are arguably the simplest finite-state model recognizing languages of infinite words. Two algorithmic problems are paramount in the theory of automata: language inclusion and automata minimization. They are both PSPACE-complete, thus under standard complexity-theoretic assumptions no deterministic algorithm with worst case polynomial time can be expected. In this thesis, we develop techniques to tackle these problems. In automata minimization, one seeks the smallest automaton recognizing a given language (“small” means with few states). Despite PSPACE-hardness of minimization, the size of an automaton can often be reduced substantially by means of quotienting. In quotienting, states deemed equivalent according to a given equivalence are merged together; if this merging operation preserves the language, then the equivalence is said to be Good for Quotienting (GFQ). In general, quotienting cannot achieve exact minimization, but, in practice, it can still offer a very good reduction in size. The central topic of this thesis is the design of GFQ equivalences for B¨uchi automata. A particularly successful approach to the design of GFQ equivalences is based on simulation relations. Simulation relations are a powerful tool to compare the local behavior of automata. The main contribution of this thesis is to generalize simulations, by relaxing locality in three perpendicular ways: by fixing the input word in advance (fixed-word simulations, Ch. 3), by allowing jumps (jumping simulations, Ch. 4), and by using multiple pebbles (multipebble simulations for alternating BA, Ch. 5). In each case, we show that our generalized simulations induce GFQ equivalences. For fixed-word simulation, we argue that it is the coarsest GFQ simulation implying language inclusion, by showing that it subsumes a natural hierarchy of GFQ multipebble simulations. From a theoretical perspective, our study significantly extends the theory of simulations for BA; relaxing locality is a general principle, and it may find useful applications outside automata theory. From a practical perspective, we obtain GFQ equivalences coarser than previously possible. This yields smaller quotient automata, which is beneficial in applications. Finally, we show how simulation relations have recently been applied to significantly optimize exact (exponential) language inclusion algorithms (Ch. 6), thus extending their practical applicability.en
dc.contributor.sponsorEngineering and Physical Sciences Research Council (EPSRC)en
dc.language.isoenen
dc.publisherThe University of Edinburghen
dc.relation.hasversionAbdulla, P., Chen, Y.F., Clemente, L., Holik, L., Hong, C.D., Mayr, R., Vojnar, T.: Simulation Subsumption in Ramsey-Based B¨uchi Automata Universality and Inclusion Testing. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification. LNCS, vol. 6174, pp. 132–147. Springer Berlin / Heidelberg, Berlin, Heidelberg (2010), http://dx.doi.org/10.1007/ 978-3-642-14295-6_14 13, 254, 255, 257, 258, 261en
dc.relation.hasversionAbdulla, P., Chen, Y.F., Clemente, L., Holik, L., Hong, C.D., Mayr, R., Vojnar, T.: Advanced Ramsey-based Buechi Automata Inclusion Testing. In: International Conference on Concurrency Theory (Sep 2011) 13, 252, 254, 255, 256, 261, 262, 263en
dc.relation.hasversionClemente, L.: B¨uchi Automata Can Have Smaller Quotients. In: Aceto, L., Henzinger, M., Sgall, J. (eds.) Automata, Languages and Programming, Lecture Notes in Computer Science, vol. 6756, chap. 20, pp. 258–270. Springer Berlin / Heidelberg, Berlin, Heidelberg (2011), http://arxiv.org/pdf/1102. 3285 36, 73, 101en
dc.relation.hasversionClemente, L., Mayr, R.: Multipebble Simulations for Alternating Automata - (Extended Abstract). In: International Conference on Concurrency Theory. LNCS, vol. 6269, pp. 297–312. Springer-Verlag (2010), http://dx.doi. org/10.1007/978-3-642-15375-4_21 xi, 119, 121, 134, 159, 160, 174, 175, 176, 224en
dc.subjectcomputer scienceen
dc.subjectautomata theoryen
dc.subjectsimulation preorderen
dc.subjectminimizationen
dc.titleGeneralized simulation relations with applications in automata theoryen
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