Synthesis of Moore machines from LTL specifications
No Thumbnail Available
URL
Journal Title
Journal ISSN
Volume Title
School of Science |
Master's thesis
Checking the digitized thesis and permission for publishing
Instructions for the author
Instructions for the author
Authors
Date
2010
Major/Subject
Tietojenkäsittelyteoria
Mcode
T-79
Degree programme
Language
en
Pages
vii + 48
Series
Abstract
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.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.Description
Supervisor
Heljanko, KeijoThesis advisor
Heljanko, KeijoKeywords
Büchi automata, Büchin tilakone, linear temporal logic, lineaarinen aikalogiikka, program synthesis, tilakonesynteesi, safety game, turvapeli, difference logic, pariteettipeli, parity games, differenssilogiikka