Aika-abstraktio.

Systeemeissä, joissa erilaiset aikavaatimukset ovat olennaisia, on tapana käyttää malleina aika-automaatteja. Yksinkertaistetaan tätä hieman. Meillä on automaatti, joka voi tehdä siirtymiä tilasta toiseen, so, siinä on tilojen joukko S, ja tapahtumien joukko E, ja siirtymä (s,e,s') tarkoittaa, että jos automaatti on tilassa s ja tapahtuu e, niin voidaan siirtyä tilaan s'.

Lisäksi meillä on joukko kelloja. Aika kulkee tasatahtia (on olemassa myös malleja, joissa kellot voivat käydä eri tahtia, mutta sivuutan tässä sen, koska se ei ole tämän abstraktion kannalta olennaista), eli kaikki kellot käyvät samalla nopeudella. Jokainen tapahtuma voi sisältää kelloehdon ja kellovaikutuksen. Ehto on konjunktio väittämistä muotoa "kello x on vähintään k" tai "kello x on enintään k". Kellovaikutus taas on aina jonkin kellojoukon nollaaminen. Rajoitun tässä ns. event recording- automaatteihin (ERA), jossa jokainen tapahtuma voi nollata korkeintaan yhden kellon. ERA:ssa siis jokaisella tapahtumalla voidaan ajatella olevan oma kello. Muut tapahtumat eivät sitä voi muuttaa, mutta tapahtuman ehtona voi toki esiintyä muiden kellojen arvoja.

Jos kellot mallinnetaan reaaliarvoisina muuttujina, niin mitätönkin aika-automaatti tuottaa tietenkin äärettömän - peräti ylinumeroituvan - määrän tiloja. Aika täytyy siis abstrahoida. Tyypillisesti se tehdään esittämällä aika ns. alueina, eli kellojen arvojen välisinä suhteina. Jos esimerkiksi suoritamme ensin tapahtuman "a" ja sitten tapahtuman "b", ja näiden kellot ovat x(a) ja x(b), niin päädymme alueelle, jossa x(b) < x(a), jos taas teemme toisin päin, niin x(b) > x(a).
Jos tapahtuman "a" kelloehto on, että x(b) > 2, niin suorittamalla tapahuman a, päädytään alueelle, jossa tämä pätee.

Tutkimani osittaisjärjestykseen tai oikeastaan kommutatiivisuuteen perustuvat reduktiot eivät toimi liian hienojakoisten aika-abstraktioiden kanssa. Syy on se, että reduktion tarkoituksena on hävittää kahden tapahtuman rinnakkaisuudesta aiheutuvat "turhat" permutaatiot. Aikamalleissa tapahtumien järjestys on ikäänkuin osa todellisuutta. Täytyy kuitenkin muistaa, että tämä on abstraktio: jos meillä on kaksi rinnakkain toimivaa aika-automaattia, niin vaikka periaatteessa a ja b voisivat tapahtua yhtä aikaa, niin lomitetun ajan (jokainen tapahtuma tapahtuu yksinään ja tarkalleen silloin kun se tapahtuu) malleissa tavallaan aina tiedämme "liikaa" näiden tapahtumisjärjestyksestä. Silloinkin kun se ei ole olennaista.

Tämänhetkinen tutkimusaiheenani onkin abstraktio, joka on riittävän hienojakoinen, jotta se säilyttää spesifikaation toteutumisen tarkastamiseen vaadittavan informaation, mutta riittävän karkea, jotta se sallii kommutatiivisuusreduktion silloin, kun se on "oikeasti" mahdollista. Eli abstraktio hävittää informaatiota eri kellojen järjestyksestä silloin, kun se ei ole tarpeen oikeellisuuden säilyttämiseksi. Tehtävä on yllättävän haastava, ja ongelmaa on aina välillä tutkittu ainakin vuodesta 1998 saakka.

En usko, rehellisesti sanoen, että kykenen ratkaisemaan ongelmaa laadullisesti merkittävästi paremmin kuin jo olemassaolevat "ratkaisut" (jotka eivät ole kovin tehokkaita), mutta uskon että voin tehdä joitain sellaisia inkrementaalisia parannuksia, joista on vähäistä käytännön hyötyä.