tiistai 10. toukokuuta 2016

Legacy (kerrankin muuta kuin nostelua)

I am hoping that I can be known as a great writer and actor some day, rather than a sex symbol. 
  -Steven Seagal

Jätin hakemuksen dosentuurin myöntämisestä. Minun piti tehdä tämä viisi (5) vuotta sitten, mutta olen lykännyt asiaa koska en ole kokenut sen olevan ajankohtainen. Teoriassa ja käytännössä sovellettujen kriteerien mukaan olisin ollut pätevä jo tuolloin mutta koin etten tarvitse sellaista titteliä mihinkään, ja se käytännössä velvoittaisi minut tiettyihin asioihin. Esimerkiksi Suomen Akatemian tutkimushankkeissa hankkeen vetäjän tulee olla dosentti tai professori suomalaisessa yliopistossa. Koska minä en ole, olen voinut perustellusti jättää esimerkiksi hankehakemukset tekemättä. Olen kuitenkin viime vuodet haamukirjoittanut hankehakemuksia muille, ja esimiehen kanssa käydyn keskustelun perusteella tulimme johtopäätökseen ettei tässä ole mitään järkeä.

Tutkimusurani on ollut melko tylsämielinen. Aloitin aikanaan -- 16 vuotta sitten -- tutkimaan optimointialgoritmeja ja siirryin siitä graafialgoritmeihin ja 2001 alussa perustutkinnon tehtyäni siirryin Verifiointialgoritmien tutkimusryhmään. Verifiointi viittaa siis menetelmiin joilla jonkin järjestelmän kuvauksesta päätellään virheettömyys. Ala on varsin laaja ja "poikkitieteellinen" ja  käyttää laajasti logiikkaa, graafiteoriaa, automaattiteoriaa, algebraa, jne.

Alalla on monta eri tutkimussuuntaa, mutta yhdessä nurkassa on kaksi suuntaa jotka puhuvat samoista asioista eri termein; järjestelmän toiminta voidaan yhtäältä nähdä siten että sen tila on havaittavissa ja ajan yli järjestelmän toiminnan kannalta olennaiset asiat päätellään siitä millaisissa tiloissa järjestelmä on ollut. Toisaalta järjestelmä voidaan ajatella koostuvan tapahtumista (event, action) ilman että tilaa voidaan oikeastaan havainnoida mitenkään. Näiden välillä vallitsee tietyssä mielessä duaalisuus, koska "tila" voidaan karakterisoida jälkimmäisessä niiden tapahtumien joukkona jotka ovat mahdollisia kunakin hetkenä ja "tapahtuma" ensimmäisessä yksinkertaisesti tilan muutoksena.

Tilapohjaisessa hahmotuksessa on helpompi käyttää erilaisia logiikoita, jokaisessa tilassa pätee jokin kaava ja esimerkiksi aikalogiikka kertoo sellaisista asioista kuin "ennen pitkää pätee että X" tai "koskaan ei päde Y" tai "X pätee kunnes Y tulee voimaan" jne. Tapahtumapohjaisissa menetelmissä on helpompaa konstruoida erilaisia algebrallisia relaatioita järjestelmien välille, kuten että "tämä järjestelmä ei tee mitään sellaista mitä tuokaan ei tee" (ns. refinement) ja näiden päälle voidaan rakentaa esimerkiksi induktiivista päättelyä. Kummassakin on omat erilaiset abstrahoinnin menetelmänsä. Olen kirjoittanut aikanaan paljon abstraktiosta koska se on äärimmäisen mielenkiintoinen käsite tässä yhteydessä.

Tilapohjaisissa malleissa on ns. änkytys (engl. stuttering) mikä tarkoittaa tilannetta jossa järjestelmän tila kyllä muuttuu mutta tilan ominaisuudet ovat loogisessa ja malli-teoreettisessa mielessä samat. Tapahtumapohjaisessa maailmassa tätä vastaa ns silent action, tai näkymätön tapahtuma, joka voi muuttaa järjestelmän tilaa, mutta jota ei ulospäin voida havaita.  Abstrahoinnin voidaan ajatella tilapohjaisessa maailmassa tuottavan änkytystä ja tapahtumapohjaisessa maailmassa se taas tuottaa joko näkymättömiä tapahtumia tai epädeterminismiä. Epädeterminismi viittaa siis siihen että tapahtuu jotain mutta lopputuloksena voi olla erilaisia asioita.

Tein väitöskirjani oikeastaan siitä, miten aikalogiikka-tyyppistä spesifiointia voidaan hyödyntää malleissa joissa on myös tapahtumapohjaista informaatiota. Lineaarisen aikalogiikan (LTL) mallintarkastuksessa käytetään hyväksi sitä tosiasiaa että jokainen LTL-kaava voidaan muuttaa ns Büchi- automaatiksi. Automaatti toimii kivasti tilapohjaisten mallien (kuten Kripke-rakenteiden) kanssa, mutta tapahtumapohjaisen mallin erityispiirteet taas hieman tökkivät. Änkytys on yksi ongelmakohta. Lineaarinen aikalogiikka sisältää operaation "seuraavaksi P" (merkitään usein X.P), mikä tarkoittaa että jos järjestelmä vaihtaa tilaa, niin vaihdon jälkeen pätee P. Jos tämä operaattori jätetään pois, niin LTL-kaavat jotka voidaan ilmaista, eivät erottele toimintoja jotka erovat toisistaan (äärellisen) änkytyksen suhteen. Väitöskirjassani "Alternatives to Büchi automata" käsittelin erästä toista, paremmin tapahtumapohjaiseen maailmaan istuvaa, automaattia, ja lisäksi erilaisia algoritmeja, sekä vertailin Büchi-automaatin ja tämän automaatin välistä suorituskykyä käytännössä.

Kun siirryin post-doc tutkimukseeni, halusin tehdä "jotain muuta". Väitöstilaisuudessa vastaväittäjäni esitti erään kysymyksen väitöstutkimukseni ja erään toisen menetelmän (ns Partial Order Reduction) yhdistämisestä, joka jäi vaivaamaan minua. Tutkittuani determinismiä hetken aikaa, siirryin tämän toisen menetelmän pariin vuonna 2008. Nyt, kahdeksan vuotta myöhemmin olen vihdoin kirjoittamassa artikkelia joka vastaa teoriatasolla vastaväittäjäni esittämään kysymykseen. Olin 2014 alamme johtavassa konferenssissa esittelemässä erästä paperiani. Samaan aikaan esimieheni sai palkinnon 90-luvulla tekemästään pioneerityöstä juurikin tämän partial order reduction-aiheen parissa. Kun eräs kaverini esitteli minut joillekin että "He is the new Mr Partial Order Reduction" tajusin että olen mennyt liian pitkälle tähän aiheeseen, minun on pakko vaihtaa alaa.

Toivon mukaan tämä artikkeli on viimeinen jonka aiheesta kirjoitan. Tiedän kyllä ettei se tule olemaan, koska jo nyt kun olen kirjoittanut pari lukua, tajuan että kirjoitettavaa ja tutkittavaa on vaikka kuinka paljon. Tunnen itseni linnuksi (oliko se Harakka vai Varis?) vanhassa Aapisessa, jonka nokka ja pyrstö vuoron perään tarttuvat tervaan.

Täytän 40 kesällä, kuten edellisessä kirjoituksessani sanoin. Minulla on tilastojen valossa vielä 10 vuotta aikaikkunaa jossa voin tehdä merkittäviä uusia avauksia ja 25-30 vuotta aikaa lypsää tutkimustuloksia. En halua hautakiveeni tekstiä "Mr Partial Order Reduction".

1 kommentti:

Teemu Rovio kirjoitti...

http://www.imdb.com/title/tt0116905/quotes?item=qt0372773