haku: @instructor Heljanko, Keijo / yhteensä: 44
viite: 26 / 44
| Tekijä: | Ellonen, Sakari |
| Työn nimi: | Synthesis of Moore machines from LTL specifications |
| Mooren koneiden syntetisointi LTL-määrittelyistä | |
| Julkaisutyyppi: | Diplomityö |
| Julkaisuvuosi: | 2010 |
| Sivut: | vii + 48 Kieli: eng |
| Koulu/Laitos/Osasto: | Informaatio- ja luonnontieteiden tiedekunta |
| Oppiaine: | Tietojenkäsittelyteoria (T-79) |
| Valvoja: | Heljanko, Keijo |
| Ohjaaja: | Heljanko, Keijo |
| OEVS: | Sähköinen arkistokappale on luettavissa Aalto Thesis Databasen kautta.
Ohje Digitaalisten opinnäytteiden lukeminen Aalto-yliopiston Harald Herlin -oppimiskeskuksen suljetussa verkossaOppimiskeskuksen suljetussa verkossa voi lukea sellaisia digitaalisia ja digitoituja opinnäytteitä, joille ei ole saatu julkaisulupaa avoimessa verkossa. Oppimiskeskuksen yhteystiedot ja aukioloajat: https://learningcentre.aalto.fi/fi/harald-herlin-oppimiskeskus/ Opinnäytteitä voi lukea Oppimiskeskuksen asiakaskoneilla, joita löytyy kaikista kerroksista.
Kirjautuminen asiakaskoneille
Opinnäytteen avaaminen
Opinnäytteen lukeminen
Opinnäytteen tulostus
|
| Sijainti: | P1 Ark Aalto | Arkisto |
| Avainsanat: | Büchi automata linear temporal logic program synthesis safety game difference logic parity games Büchin tilakone lineaarinen aikalogiikka tilakonesynteesi turvapeli pariteettipeli differenssilogiikka |
| Tiivistelmä (fin): | Mooren kone on äärellinen tilakone. jolla on ulostuloja. Niitä käytetään yleisesti mallintamaan digitaalisia piirejä. LTL-synteesiongelma on ratkaista, onko olemassa Mooren konetta, joka toteuttaisi annetun lineaarisen aikalogiikalla (LTL) ilmaistun määrittelyn. Mikäli on, annetaan toteuttava Mooren kone vastauksena. Jos tilakoneet voitaisiin syntetisoida määrittelystä automaattisesti, vapautuisi kehittäjä kirjoittamasta toteutusta käsin. Syntetisointi mahdollistaa myös määrittelyjen ristiriidattomuuden ja kattavuuden analysoinnin. mikä vaikuttaa tällä hetkellä realistisemmalta tavoitteelta kuin ohjelmoinnin täydellinen automatisointi. Synteesialgoritmi huomaa. mikäli määrittely on sisäisesti ristiriitainen eikä siis ole ollenkaan toteutettavissa. ja toisaalta syntetisoidun tilakoneen odottamaton käytös voi auttaa löytämään määrittelyn puutteita. Synteesiongelman laskennallinen vaativuus todettiin kuitenkin yleisessä tapauksessa hyvin korkeaksi, mikä ei ole kannustanut tutkijoita uhraamaan merkittäviä resursseja varsinkaan käytännön ratkaisujen etsimiseen, vaikka teoria onkin vuosikymmenten kuluessa kehittynyt. Tämä diplomityö esittelee kolme lähestymistapaa synteesiongelmaan: Ensimmäinen on klassisin, ja perustuu omega-tilakoneiden determinisointiin. Toinen palauttaa ongelman voittostrategian etsimiseen turvapelissä. jossa syntetisoija häviää, mikäli syötteen antava ympäristö rikkoo määrittelyä. Kolmas menetelmä palauttaa ongelman differenssilogiikan instanssiksi. joka on toteutuva jos ja vain jos on olemassa korkeintaan annetun vakion kokoinen Mooren kone, joka toteuttaa määrittelyn. Kaikki kolme menetelmää on toteutettu ja koeteltu muutamilla määrittelyillä. Tärkein tutkimustulos on. että vain turvapeliin perustuva menetelmä pystyy ratkaisemaan ongelman ei-triviaaleille määrittelyille. Kaksi muuta lähestymistapaa eivät löydä ratkaisua tämän työn määrittelyille ajan ja muistin mielekkäissä rajoissa. Toisaalta differenssilogiikkamenetelmän merkittävä etu on. että sillä voi löytää pienimmän mahdollisen ratkaisun. |
| Tiivistelmä (eng): | Moore machine is a finite state machine with output and it is a common model for digital circuits. The LTL synthesis problem is to decide whether there exists a Moore machine which satisfies a given specification expressed in the Linear Temporal Logic (LTL), and if so, give such a machine. If we could synthesize Moore machines automatically from their specification, the developer would he freed from manually writing the implementation. Automated synthesis also allows one to analyze the consistency and completeness of specifications, which currently seems a more realistic aim than to completely replace manual programming. A synthesis algorithm detects if a specification is not realizable, and unintended behaviour of a synthesized program may lead one to discover under specification issues. However, the high computational complexity of the problem in the general case has discouraged researchers and little of the theory developed during the past decades has been put into practice. This Thesis presents three approaches to the synthesis problem: The first one is a classic, based on deterministic omega-automata. The second one reduces the problem to determining winning strategies in a safety game, where the synthesizer loses if the environment giving inputs violates the specification. The third one is a reduction to an instance of Difference Logic which is certifiable if and only if there exists a program of size at most a predefined bound. All three have been implemented and experimental data is provided on their applicability to some benchmarks. The main result is that the safety game approach can be considered relatively efficient and viable also for non-trivial specifications, whereas the other two do not scale up on our benchmarks. On the other hand, the Difference Logic approach has to its considerable advantage that it produces minimal Moore machines which implement the specification. |
| ED: | 2011-01-18 |
INSSI tietueen numero: 41489
+ lisää koriin
INSSI