Induktio.

Mallintarkastus (model checking) tarkoittaa tekniikkaa, jossa jonkin järjestelmän virheettömyys osoitetaan ns. malliteoreettisella argumentilla. Jos meillä on järjestelmä M ja ominaisuus P, niin mallintarkastus pyrkii toteamaan, päteekö M |= P, eli että järjestelmän kuvaus M on ominaisuuden P malli. 

Vaihtoehtoja järjestelmän mallille on monia, samoin ominaisuus voi olla monella eri tavalla esitetty. Niin kutsutussa eksplisiittisessä mallintarkastuksessa järjestelmä esitetään tilakoneena tms, jonka kaikki tilat tutkitaan ja tarkastetaan että ominaisuus P pätee, tai sitten löydetään virhe, eli jokin järjestelmän suoritus jossa P rikkoutuu.

Symbolisesta mallintarkastuksesta puhutaan usein silloin, kun järjestelmä on esitetty symbolisesti, eli esimerkiksi jonkinlaisten logiikan kaavojen tms avulla siten, että yksittäiselle tilalle ei välttämättä ole mitään esitystä. Symbolinen mallintarkastus oli suosittua 80- ja 90-luvulla ns. binääristen päätöskaavioiden (BDD) ansiosta.  BDD kykenee esittämään joukon järjestelmän tiloja kompaktisti, jos järjestelmä on riittävän säännönmukainen. Järjestelmän tilasiirtymät esitetään symbolisesti loogisena funktiona T ja kun meillä on jokin joukko tiloja S (esitetty esimerkiksi BDD:n avulla), T(S) kuvaa ne tilat joihin voidaan päätyä jos tehdään siirtymiä joukosta S.  Kun BDD:ille on annettu jokin kanoninen esitystapa, niin kahden BDD:n ekvivalenssi on helppo laskea, samoin implikaatio -- eli käytännössä osajoukkorelaatio. Jos T(S) on S:n osajoukko, niin sanomme että S on kiintopiste eli ns. fixed point. Tämä tarkoittaa sitä, että jos tiedämme järjestelmän olevan jossakin S:n tilassa, ja T(S) on S:n osajoukko, niin tiedämme että S sisältää kaikki sellaiset tilat johon järjestelmä voi ylipäätään päätyä.

90-luvun lopulla alkoi tapahtua tietojenkäsittelyssä, kun yhtä aikaa tietokoneet olivat tulleet nopeammiksi ja tehokkaammiksi, ja toisaalta algoritmit kehittyneet. Tunnettu NP-täydellinen ongelma on niin sanottu SAT-ongelma. SAT tarkoittaa ongelmaa, jossa jos meille on annettu propositiologiikan kaava X, niin kysytään, voidaanko propositioille löytää sellaiset arvot että kaava on tosi. Huolimatta ongelman NP-täydellisyydestä, valtavan moni yksittäinen SAT-ongelma itseasiassa ratkeaa hyvinkin tehokkaasti, eli patologiset tapaukset ovat varsin harvinaisia. Armin Biere ja muutama muu keksivät mallintaa järjestelmän propositiologiikan avulla ja keksivät ns. rajoitetun mallintarkastuksen (Bounded Model Checking,BMC). Siinä järjestelmän toiminta esitetään tiettyyn askelmäärärajaan k asti propositiologiikan kaavana X(k), ja tarkastettava ominaisuus P esitetään myös kaavana, ja kysytään, onko kaava (X(k) & !P) SAT instanssi. Jos se on, niin olemme löytäneet virheen, jos ei, niin olemme osoittaneet että virhettä ei ole ensimmäisen k-askeleen jälkeen.

BMC:n ongelma on, että kaavan pituus kasvaa koko ajan eikä siinä sellaisenaan ole mitään fixed point- karakterisointia. Jokainen askel tuo kaavaan lisää muuttujia, ja sitäpaitsi, järjestelmän toiminta voi hyvinkin olla ääretön, jolloin mitään kiintopistettä ei edes teoriassa voi löytää.

Ken McMillan ja muutamat muut keksivät jossain kohtaa soveltaa ns. Craigin interpolantteja BMC:hen. Interpolantti toimii suunnilleen niin, että jos meillä on kaava A & B, joka ei ole SAT, eli se on ristiriitainen, niin löytyy kaava I (vasen interpolantti), jolla on ominaisuudet 1) A => I, 2) I & B ei ole SAT ja 3) I:ssä esiintyy vain sellaisia propositioita jotka ovat yhteisiä A:lle ja B:lle.  Oikea interpolantti olisi symmetrisesti sellainen jossa B => I jne.

Kun järjestelmän toimintaa mallinnetaan jollakin kaavalla, erityisesti, jos A on kaava joka sisältää sekä propositioita joiden on tarkoitus kuvata tiloja että propositioita jotka kuvaavat transitioiden ominaisuuksia ja B kuvaa pelkästään tilojen ominaisuuksia, niin interpolantti esittää jonkin joukon tiloja. Koska A => I pätee, niin ne tilat joista A puhuu, muodostavat niiden tilojen osajoukon joista I puhuu. I on tietyssä mielessä abstraktio joka vangitsee A:n tiloista jotain siitä miksi A & B ei ole SAT. Koska A kuvaa järjestelmän suoritusta johonkin rajaan asti, I on eräänlainen selitys sille, miksi A ei sisällä virhettä. 

Vedän tässä hieman oikoiseksi mutkia, mutta jos suoritamme BMC:tä johonkin rajaan k asti, emmekä löydä virhettä, niin X(k) & !P ei ole SAT. Jos tässä kohtaa etsimme interpolantin I, niin I & !P ei ole SAT ja I esittää joukon tiloja. Kun käytämme propositio- tai predikaattilogiikkaa tilasiirtymien esittämiseen, joudumme aina esittämään joka askelella uusia muuttujia. Jos meillä on joukko muuttujia V, niin tilasiirtymät esitetään kaavalla T(V,V') niin, että joukon V' muuttujat kuvaavat muuttujien arvoja tämän siirtymän jälkeen. Koska interpolantti I esittää myöskin joukon tiloja, yleensä ajattelemme että se on muotoa I(V), mutta V':n muuttujia siinä ei tietenkään esiinny.  Kaava (I(V) & T(V,V')) kuvaa sitä joukkoa tiloja joihin päästään jos lähtötiloina ovat tarkalleen ne tilat joissa pätee I(V). Nyt, jos (I(V) & T(V,V')) implikoi kaavan I(V'), niin olemme itseasiassa löytäneet jällleen kiintopisteen.  Sanotaan myös, että I on induktiivinen relaation T(V,V') suhteen.

Ilman BDD:itäkin mallintarkastus voidaan siis tehdä sellaiseksi että se myös voi todistaa järjestelmän oikeaksi kokonaan, ei vain johonkin rajaan saakka, jos löydämme induktiivisen interpolantin. Voimme tällöin jakaa mallintarkastuksen kolmeen vaiheeseen: 1) Meidän pitää löytää kaava joka esittää jonkin joukon tiloja joista ainakin osaan alkutilasta voidaan päästä, 2) Virheen ja kaavan konjunktion pitää olla ristiriitainen 3) Kaavan pitää olla induktiivinen tilasiirtymärelaation suhteen. BMC-pohjainen mallintarkastus lähtee alkutilasta ja kasvattaa kaavaa johonkin rajaan asti, tämän jälkeen se muodostaa interpolantin. Tämä prosessi takaa että kaksi ensimmäistä ominaisuutta toteutuvat, mutta induktiivisuutta se ei takaa.

Niin sanottu CEGAR (counterexample-guided abstraction refinement) taas perustuu ajatukseen, että tutkimme koko ajan kaavaa joka on sekä induktiivinen että sisältää alkutilan. Alussa tällainen kaava on tautologinen, ja esittää siten kaikkien mahdollisten (ja mahdottomien) tilojen joukon. Se kuitenkin esittää myös virheen. Kaava on siis "liian abstrakti" eikä ota huomioon järjestelmän toiminnan rajoitteita. Algoritmi toimii niin, että tähän reagoidaan lisäämällä jokin rajoite joka varmasti on voimassa transitiorelaatiossa, ja joka ei riko induktiivisuutta, ja tarkastetaan uudelleen. Tässä rikon hieman rajoja, koska näen prosessit samoina, oli kyse sitten eksplisiittisestä tai symbolisesta mallintarkastuksesta. Minulla kesti melkein 14 vuotta ymmärtää että sillä ei ole oikeastaan tässä kohtaa mitään merkitystä; Eksplisiittinen mallintarkastus tavallaan perustuu siihen että järjestelmänkuvauksesta tutkittavana oleva osa on aina "induktiivinen", se vain on niin suuri ettei sitä voida kokonaan tarkastella. Abstraktiolla tuotetaan pienempi malli joka on takuulla induktiivinen mutta saattaa tuoda virhetilan vahingossa malliin.

Kaikkien kaavojen joukossa, joita voimme muodostaa -- tämä on hyvinmääritelty, jos kohta ääretön joukko -- annetun järjestelmän atomisista ominaisuuksista, on mielenkiintoinen rakenne malliteoreettisessa ja algebrallisessa mielessä. Tässä kohtaa olen hyvin mielissäni, että sain opettaa pari vuotta matemaattista logiikkaa,  kumpa olisin saanut tehdä niin jo vuosia aiemmin, olisin ymmärtänyt tämän jo ennen kuin matalalla roikkuvat hedelmät aihepiiristä oli poimittu. Nimittäin, kaavoilla on ns. hilarakenne. Otetaan kaavojen sijaan niiden ekvivalenssiluokat, eli samastetaan kaavat jotka ovat loogisesti yhtäpitäviä. Hilassa on maksimaalinen ja minimaalinen alkio: Identtisesti todet kaavat ja identtisesti epätodet kaavat, eli [T] ja [F].  Osittaisjärjestyrelaationa on se, että jos [P => Q] = [T], niin P < Q.  Kahdella kaavalla A ja B on supremum, [A || B] (A or B) ja infimum [A && B].

Tässä hilassa on monta mielenkiintoista alihilaa. Esimerkiksi jos T(V,V') -- transitiorelaatio -- on fiksattu, niin induktiivisten kaavojen joukko muodostaa alihilan: Sekä True että False ovat induktiivisia, mikä ei ole vaikea todistaa. Myös kahden induktiivisen kaavan disjunktio ja konjunktio ovat induktiivisia. Negaatio ei ole induktiivinen yleisessä tapauksessa, mutta negaation suhteen suljettujen induktiivisten kaavojen joukko on itsessään tämän alihilan alihila, ja se ei ole vaike nähdä myöskään; kyseinen alihila sisältää aina vähintäänkin kaavat True ja False (jotka ovat siis toistensa negaatioita). Joka tapauksessa, merkitään T(V,V'):n suhteen induktiivisten kaavojen alihilaa IL(T).

Ja tästä -- anteeksi pitkä johdanto -- pääsemmekin mielenkiintoiseen asiaan, eli siihen, miten T(V,V') vaikuttaa tähän hilarakenteeseen jos voimme "häiritä" sitä. Nimittäin, oma erikoisalani osittaisjärjestyreduktio (POR, partial order reduction) toimii niin, että tietyissä oloissa voimme eliminoida joitakin transitioita järjestelmästä. Käytännössä tämä tarkoittaa, että luomme kaavan R(V,V') jolla on se ominaisuus että R(V,V') => T(V,V') ja että M(T) |= P jos ja vain jos M(R) |= P. Tässä siis M(T) viittaa malliin joka on rakennettu käyttäen relaatiota T ja M(R) käyttäen relaatiota R.

Kansanviisaus alalla on sanonut, että POR on hyödyllistä eksplisiittisessä mallintarkastuksessa, muttei juurikaan symbolisessa. Kaiken muun huvittavan lisäksi, niiltä osin kun sitä on symbolisessa mallintarkastuksessa ylipäätään käytetty, sen on ajateltu soveltuvan vain asyklisten järjestelmien mallintarkastukseen, koska syklisyys aiheuttaa tietyissä tilanteissa ongelmia oikeellisuuden kannalta. Tämä ongelma kuitenkin ratkaistiin vajaa vuosi sitten käytännössä kokonaan uudella tavalla, jota en nyt tässä ala referoimaan, ja tämä tapa poisti käytännössä ongelman kokonaan.

On helppo todistaa, että jos R(V,V') on rajoittavampi kaava kuin T(V,V'), IL(T) on IL(R):n alihila. Se, mitä aiomme nyt seuraavaksi tehdä, on tutkia jos voisimme löytää IL(R)-alihilalle (tai sen jollekin alihilalle) joukon eräänlaisia kanta-alkoita, joita yhdistämällä konjunktiivisesti ja disjunktiivisesti voimme löytää sellaisen induktiivisen kaavan, joka sisältää alkutilan mutta ei sisällä virhetilaa, ja, jonka avulla vielä voisimme nopeasti löytää todisteet sille että tällaista kaavaa ei ole, mikäli tämä todella on tilanne.