Olettakaamme että olemme tutkimassa jonkinlaisen systeemin S käyttäytymistä. Systeemissä on erilaisia muuttujia, joita voimme ehkä mitata, emme ehkä täydellisesti mutta voimme kuitenkin saada jotain tietoa. Oletetaan että nämä muuttujat ilmaistaan symbolilla x. Tämä on siis periaatteessa vektori kaikesta siitä, mikä systeemissä on olennaista. Oletan tässä että meillä on lisäksi käsite aika, joka on yksi muuttuja, mutta yksinkertaisuuden vuoksi oletan että se ei ole mukana mainitussa x:ssä.
Systeemin tila on jollakin ajanhetkellä muuttujan x arvo. Jos tunnemme systeemin tilan kahtena ajanhetkenä, niin oletamme että systeemi on siirtynyt ensimmäisestä tilasta toiseen; se, miten systeemi siirtyy tilasta toiseen, määrittää systeemin dynamiikan. Melko yleisiä systeemien dynamiikan kuvaamiseen käytettyjä formalismeja ovat esimerkiksi differentiaaliyhtälöt. Jos x koostuu komponenteista x1, x2, ..., xn, niin meillä on tyypillisesti useampia differentiaaliyhtälöitä jotka kuvaavat sitä miten muuttujien kehitys ajan suhteen riippuu toisistaan. Esimerkiksi voisi olla vaikkapa kahden muuttujan systeemi, jossa x1' = x2 ja x2' = -x1. Tämä on hyvin yksinkertainen systeemi, jossa siis x1 kasvaa sitä nopeammin mitä suurempi x2 on ja x2 taas pienenee sitä nopeammin mitä suurempi x1 on; tällainen systeemi on oskilloiva, mutta se ei nyt ole olennaista.
Differentiaaliyhtälöillä kuvataan järjestelmiä, jotka ovat jatkuvia. Jatkuvuus viittaa siis siihen, että aika etenee tasaista tahtia ja muuttujat ovat tyypillisesti reaali- tai kompleksilukuja. Differentiaaliyhtälöillä kuvataan lisäksi järjestelmiä jotka ovat deterministisiä, eli niiden toiminta on tarkalleen määrätty kun tila tunnetaan. Deterministisen sijaan järjestelmä voi olla esimerkiksi stokastinen, jolloin sen toimintaan liittyy jokin satunnainen komponentti, esimerkiksi differentiaaliyhtälössä voi esiintyä satunnaismuuttujia, jolloin saatu yhtälö ei kuvaakaan järjestelmän tilaa ajan funktiona vaan ainoastaan tilan jakaumaa. Kolmas vaihtoehto on, että järjestelmä on epädeterministinen, mikä tarkoittaa että sillä on aidosti useita eri polkuja; tätä käytetään erotuksena stokastisesta siten, että epädeterminismi tulee esimerkiksi mukaan malliin tuntemattomien vuorovaikutusten kautta.
Jatkuvan sijaan järjestelmä voi olla myös diskreetti. Diskreetin järjestelmän tilan määrittämät muuttujat saavat diskreettejä arvoja kuten kokonaisluku- tai boolean arvoja (tosi/epätosi). Järjestelmää jossa on sekä diskreettejä että jatkuvia muuttujia nimitetään hybridijärjestelmiksi. Diskreetin järjestelmän dynamiikkaa voidaan aina kuvat tilasiirtymärelaatiolla, joka kertoo mihin muihin tiloihin jostakin tietystä tilasta voidaan päätyä. Tämä relaatio on funktio jos järjestelmä ei ole epädeterministinen, ja jos järjestelmä on stokastinen, niin funktion arvoina ovat jakaumat tilojen yli.
Predikaattiabstraktio viittaa siihen, että osa muuttujista korvataan predikaateilla. Predikaatti on totuusarvoinen väittämä joka koskee muuttujaa tai muuttujajoukkoa. Esimerkiksi jos meillä on muuttujat x ja y, niin väittämät x < y, x+y > 3, x < 0 jne ovat predikaatteja jotka puhuvat muuttujista x ja y. Tyypillisesti jos me käsittelemme jatkuvaa järjestelmää, predikaattiabstraktio on yksi tapa muuttaa järjestelmä diskreetiksi. Jos esimerkiksi x ja y ovat jatkuvia muuttujia, järjestelmän tilaa saatettaisiin abstrahoida esittämällä se kolmen predikaatin avulla: x < 0, y < 0 ja x2 + y2 < 9. Tällöin meillä olisi kahdeksan erilaista "tilaa" sen mukaan, missä kvadrantissa x ja y ovat ja sen mukaan ovatko ne 3-säteisen ympyrän sisällä vai eivät. Predikaattiabstraktio tuottaa epädeterminismiä vaikka alkuperäinen järjestelmä olisi kuvattu deterministisellä differentiaaliyhtälöllä. Esimerkiksi kun x = 5 ja y = 1, järjestelmä kehittyy niin, että y muuttuu negatiiviseksi, mutta pysyy ympyrän ulkopuolella ja kun x = 1 ja y = 5, y pienenee mutta pysyy positiivisena niin, että järjestelmä siirtyy ympyrän sisäpuolelle. Kumpikin arvoiyhdistelmä on kuitenkin mainittujen predikaattien kannalta "sama", eli abstraktio samastaa eri tavoin käyttäytyviä tiloja.
Jos tunnemme järjestelmän "riittävän hyvin" ja meillä on "riittävän hyvät" abstraktiot siten, että laadullisesti abstraktion tuottama malli kertoo meille "riittävästi", voimme luoda järjestelmän toiminnasta diskreetin mallin ja ennustaa, onko alkuperäisellä systeemillä jokin tietty abstrakti tila johon se päätyisi. Esimerkiksi voiko käydä niin, että sekä x että y ovat negatiivisia ja ympyrän ulkopuolella.
Sivuutan tässä nyt sen problematiikan joka liittyy tilasiirtymärelaation esittämiseen. Huomautan lisäksi että yleisessä tapauksessa tällaiset abstraktiot sisältävät potentiaalisesti satoja tai tuhansia predikaatteja siten, että järjestelmän diskreettienkin tilojen määrä on suurempi kuin koko maailmankaikkeudessa olevien atomien määrä; tällaisen järjestelmän kaikkien tilojen tutkiminen on yksinkertaisesti mahdotonta.
Voimme kuitenkin käyttää tähän logiikkaa, niin erikoiselta kuin se kuulostaakin. Yksi takavuosien menestyksekäs metodi oli niin kutsuttu rajoitettu mallintarkastus eli bounded model checking. Sen ideana on, että me esitämme järjestelmän alkutilan predikaattien avulla, esimerkiksi p1 & p2 & not p3 jne. Tämän lisäksi esitämme tilasiirtymärelaation logiikan kaavana siten, että jos tämänhetkisessä tilassa puhutaan predikaatista p, niin jälkimmäisessä puhutaan predikaatista p'. Esimerkiksi jos p on predikaatti joka vaihtaa totuusarvoaan jokaisessa siirtymässä, tätä merkitään p -> p', joka taas sievenee muotoon not p or p'.
Oletetaan, että "virheellinen tila" voidaan ilmaista kaavalla Y. Jos meillä on jotakin tilajoukkoa kuvaava kaava X ja tilasiirtymän kaava P( ), niin sitä tilajoukkoa joka saavutetaan joukosta X käsin, voidaan ilmaista P(X). (Tämä on siis taas kaava). Kaikki predikaatit esiintyvät tässä kaavassa (se voi olla hyvinkin suuri) pelkkinä propositioina. alkutilan ollessa x, tarkistamme onko kaava X = (x tai P(x) tai P(P(x)) tai ....) yhdessä kaavan Y kanssa mahdollista tehdä todeksi, eli onko kyseinen kaava X ja Y satisfiable eli SAT. Valitettavasti X voi kuvata vain äärellisen määrän askelia (siitä nimitys "bounded") joten tämä menetelmä voi kyllä löytää virheitä, muttei voi todistaa että järjestelmässä ei sellaisia ole.
SAT on NP-täydellinen ongelma, mutta modernit SAT-ratkaisijat ovat niin tehokkaita, ja todellisista järjestelmistä peräisin olevat mallit ovat niin strukturoituja että SAT-ratkaisijat kykenevät ratkomaan tuhansien ja jopa miljoonien klausuulien mittaisia kaavoja, joissa on kymmeniä tuhansia tai satoja tuhansia muuttujia. Toki on aina patologisia tapauksia jotka tyystin tukahduttavat ratkaisijat, mutta ne ovat todellisen maailman malleissa hyvin harvinaisia.
Meidän ei ole kuitenkaan aivan pakko tyytyä siihen ettemme koskaan saisi todistettua järjestelmää täysin oikeaksi. On nimittäin mahdollista toisinaan löytää induktiivisia invariantteja jos sovelletaan abstraktiota luovasti.
Ensimmäinen, yksinkertainen tapa on yrittää löytää ns kiintopiste. Jos kaava X kuvaa kaikkia niitä tiloja joihin voidaan päästä n:llä tai sitä pienemmällä määrällä askelia, ja jos kaava (P(X) tai X) on yhtäpitävä kaavan X kanssa, tiedämme, että kaava X itseasissa kuvaa jo kaikki mahdolliset saavutettavat tilat; jos kaava (X ja Y) on ristiriitainen, ei järjestelmä voi saavuttaa tilaa jossa Y pätee.
Tällainen kiintopiste voi olla kuitenkin niin monen askeleen päässä -- tai mikä pahempaa, järjestelmällä voi olla ääretön määrä mahdollisia tiloja (mikä tosin ei ole mahdollista jos käytämme tiukkaa predikaattiabstraktiota, mutta sivuutan sen nyt) -- että meiltä loppuu muisti tai aika ennenkuin löydämme kiintopisteen. Jos olemme nyt -- jonkin askelmäärän jälkeen -- todenneet että X kuvaa siihen mennessä saavutettavia tiloja, ja X ja Y ei ole SAT, voimme aina löytää tälle kaavalle niinsanotun interpolantin. Interpolantti on kaava Z, joka sisältää vain X:lle ja Y:lle yhteisiä symboleja, X implikoi Z:n ja Z on ristiriidassa Y:n kanssa.
Interpolantti Z voidaan nyt abstrahoida, siis tehdä siitä heikompi, kunhan se on edelleen ristiriidassa Y:n kanssa. Jos tätä merkitään kaavalla Z' niin sopivalla abstraktion valinnalla saatamme esimerkiksi pystyä osoittamaan että kaava Z' onkin kiintopiste -- se on siis induktiivinen invariantti, kaava joka kerran todeksi tultuaan pätee vaikka tekisimme kuinka tilasiirtymiä. Jos tällainen abstraktio löydetään, olemme kertakaikkisesti osoittaneet että Y ei voi toteutua järjestelmässä.
Ei kommentteja:
Lähetä kommentti