Automata and linear temporal logic : translations with transition-based acceptance

 |  Login

Show simple item record

dc.contributor Aalto-yliopisto fi
dc.contributor Aalto University en
dc.contributor.author Tauriainen, Heikki
dc.date.accessioned 2012-02-24T07:41:39Z
dc.date.available 2012-02-24T07:41:39Z
dc.date.issued 2006-10-27
dc.identifier.isbn 951-22-8343-3
dc.identifier.issn 1457-7615
dc.identifier.uri https://aaltodoc.aalto.fi/handle/123456789/2763
dc.description.abstract Automata theory provides powerful tools for designing and implementing decision procedures for temporal logics and their applications to the automatic verification of systems against their logical specifications. Implementing these decision procedures by making use of automata built from the systems and their specifications with translation procedures is challenging in practice due to the tendency of the automata to grow easily unmanageably large as the size of the systems or the logical specifications increases. This thesis develops the theory of translating propositional linear time temporal logic (LTL) into nondeterministic automata via self-loop alternating automata. Unlike nondeterministic automata, self-loop alternating automata are expressively equivalent to LTL and allow a conceptually simple translation of LTL specifications into automata using a set of rules for building automata incrementally from smaller components. The use of generalized transition-based acceptance for automata throughout all constructions gives rise to new optimized translation rules and facilitates designing heuristics for the minimization of automata by making use of language containment tests combined with structural analysis of automata. The generalized definition also supports the translation of self-loop alternating automata into nondeterministic automata by essentially applying the standard subset construction; this construction can be further simplified and optimized when working with automata built from LTL formulas. The translation rules can also be used to identify a syntactic subclass of LTL for which the exponential increase caused by the subset construction in the number of states of the automaton can always be avoided; consequently, the satisfiability problem for this subclass, which is shown to extend related subclasses known from the literature, is NP-complete. Additionally, the emptiness of generalized nondeterministic automata is shown to be testable without giving up generalized transition-based acceptance by using a new variant of the well-known nested depth-first search algorithm with improved worst-case resource requirements. en
dc.description.abstract Automaattiteorian avulla voidaan suunnitella ja toteuttaa temporaalilogiikkojen ratkaisumenetelmiä sekä näiden menetelmien sovellutuksia logiikoilla järjestelmistä esitettyjen oikeellisuusvaatimusten tietokoneavusteiseen verifiointiin. Käytännössä näiden ratkaisumenetelmien toteuttaminen kääntämällä järjestelmät ja niiden oikeellisuusvaatimukset automaateiksi on kuitenkin haasteellista, sillä näistä automaateista tulee järjestelmien tai loogisten vaatimusten koon kasvaessa helposti niin suuria, ettei niitä enää voida käsitellä. Tässä väitöskirjassa kehitetään lineaarisen ajan temporaalilogiikan (LTL) epädeterministisiksi automaateiksi kääntämisen teoriaa käyttämällä käännöksen apuna vain yhden tilan silmukoita sisältäviä alternoivia automaatteja, joilla – toisin kuin epädeterministisillä automaateilla – on sama ilmaisuvoima kuin lineaarisen ajan temporaalilogiikalla. Tätä logiikkaa voidaan kääntää näiksi automaateiksi soveltaen yksinkertaisia sääntöjä automaattien yhdistämiseksi vaiheittain keskenään yhä suuremmiksi automaateiksi. Käyttämällä yleistettyä siirtymäpohjaista hyväksyvyyden määritelmää automaateille kaikissa käännöksen vaiheissa voidaan näin muodostettuja automaatteja sieventää uusin tavoin käyttäen apuna automaattien hyväksymien kielten välisiä sisältyvyyssuhteita sekä automaattien rakenteellisia ominaisuuksia. Yleistetyn määritelmän ansiosta vain yhden tilan silmukoita sisältävät alternoivat automaatit voidaan myös kääntää edelleen epädeterministisiksi automaateiksi soveltamalla yleisesti tunnettua osajoukkokonstruktiota lähes sellaisenaan. Tämä konstruktio voidaan edelleen tehdä yksinkertaisemmin ja tehokkaammin LTL-kaavoista muodostetuille automaateille. Automaattikäännöksessä käytettävien sääntöjen avulla voidaan myös erottaa lineaarisen ajan temporaalilogiikan syntaktinen osajoukko, jonka kaavat onmahdollista kääntää epädeterministisiksi automaateiksi ilman, että automaattien tilojen määrä kasvaa osajoukkokonstruktion tavoin eksponentiaalisesti. Tästä tuloksesta seuraa, että kyseisen LTL:n osajoukon toteutuvuusongelma on NP-täydellinen. Osajoukko on samankaltaisia kirjallisuudessa aiemmin esiteltyjä osajoukkoja aidosti laajempi. Väitöskirjassa esitetään myös, kuinka epädeterministisen automaatin hyväksymän kielen tyhjyys voidaan tarkastaa luopumatta yleistetystä siirtymäpohjaisesta hyväksyvyyden määritelmästä käyttäen algoritmia, joka on uusi, huonoimman tapauksen vaatimuksiltaan tehokkaampi muunnos tunnetusta sisäkkäisestä syvyyshakualgoritmista. fi
dc.format.extent 229
dc.format.mimetype application/pdf
dc.language.iso en en
dc.publisher Helsinki University of Technology en
dc.publisher Teknillinen korkeakoulu fi
dc.relation.ispartofseries Helsinki University of Technology, Laboratory for Theoretical Computer Science. A, Research reports en
dc.relation.ispartofseries 104 en
dc.relation.haspart Additional errata file available. en
dc.subject.other Computer science en
dc.title Automata and linear temporal logic : translations with transition-based acceptance en
dc.type G4 Monografiaväitöskirja fi
dc.description.version reviewed en
dc.contributor.department Department of Computer Science and Engineering en
dc.contributor.department Tietotekniikan osasto fi
dc.subject.keyword linear time temporal logic en
dc.subject.keyword alternating automata en
dc.subject.keyword nondeterministic automata en
dc.subject.keyword transition-based acceptance en
dc.subject.keyword minimization en
dc.subject.keyword nondeterminization en
dc.subject.keyword emptiness checking en
dc.subject.keyword nested depth-first search en
dc.subject.keyword lineaarisen ajan temporaalilogiikka fi
dc.subject.keyword alternoivat automaatit fi
dc.subject.keyword epädeterministiset automaatit fi
dc.subject.keyword siirtymäpohjainen hyväksyvyys fi
dc.subject.keyword automaattien sieventäminen fi
dc.subject.keyword epädeterminisointi fi
dc.subject.keyword tyhjyystarkastus fi
dc.subject.keyword sisäkkäinen syvyyshaku fi
dc.identifier.urn urn:nbn:fi:tkk-008215
dc.type.dcmitype text en
dc.type.ontasot Väitöskirja (monografia) fi
dc.type.ontasot Doctoral dissertation (monograph) en
dc.contributor.lab Laboratory for Theoretical Computer Science en
dc.contributor.lab Tietojenkäsittelytekniikan laboratorio fi


Files in this item

This item appears in the following Collection(s)

Show simple item record

Search archive


Advanced Search

article-iconSubmit a publication

Browse

My Account