Tietojenkäsittelyteorian laboratorio

Virkaanastujaisesitelmä 19.9.2000
Ilkka Niemelä

Laskennallinen logiikka: soveltavaa tietojenkäsittelyteoriaa

Tietojenkäsittelyn koulutus on melkoisten paineiden ja odotusten kohteena. Tietoteollisuudessa valitsee vakava työvoimapula. Näin ei ole vain Suomessa vaan ilmiö on yleismaailmallinen. On esitetty, että esimerkiksi Euroopassa olisi jopa noin 400000 tietotekniikka-ammattilaisen vaje, jonka arvioidaan kasvavan 1.7 miljoonaan vuoteen 2003 mennessä. Työvoimapula on seurausta tietotekniikan taloudellisen merkityksen voimakkaasta kasvusta. On kuitenkin muistettava, että enää ei ole kyse vain tietokoneohjelmistojen käyttämisestä teknisten laskelmien tekemiseen tai tallentamaan tietomassoja vaan tietotekniikkaa löytyy sulautettuna yhä useammassa hyödykkeessä. Kuvaava esimerkki on tietoliikennetekniikka, joka on kovaa vauhtia muuttumassa hyvin ohjelmistopainotteiseksi. Aivan viime vuosina kehitystä on kiihdyttänyt oleellisesti Internetin nopea laajeneminen, joka on tuonut tietoverkot ja niiden palvelut lähelle tavallista kuluttajaa. Tämä on luonut mahdollisuuksia aivan uudentyyppiseen liiketoimintaan. Tietotekniikasta on tullut tämän uuden digitaalitalouden avainteknologia ja se on nostanut tietotekniikan taloudellisen vaikutuksen aivan uudelle tasolle.

Tällainen tilanne asettaa vakavia haasteita tietotekniikan tutkimukselle ja koulutukselle. Kilpailukyvyn säilyttäminen globaaleilla markkinoilla tarkoittaa, että on kyettävä ottamaan käyttöön uusimmat ja tehokkaimmat menetelmät mahdollisimman nopeasti ja pystyttävä hyödyntämään uusin tutkimustieto välittömästi. Keskeinen ongelma tulee olemaan laajojen ja monimutkaisten järjestelmien kehitystyön hallinta.

Koulutuksen kannalta tietotekniikka on myös hyvin haastava toimintakenttä. Alueen kehitys on niin ripeää, että alalla toimivilla lähtökohtana täytyy olla elinikäinen oppiminen. Tämän vuoksi koulutuksen yksi tärkeimmistä tavoitteista on luoda vahva pohja omaksua ja ottaa käyttöön yhä uusia menetelmiä, järjestelmiä ja työskentelytapoja. Tietojenkäsittelyteorian, tietojenkäsittelyn peruslainalaisuuksien ja mallien, ymmärtäminen antaa hyvän pohjan jäsentää ja hyödyntää tietotekniikassa tapahtuvaa kehitystä. Tämä taito on olennainen useimmille alalla toimiville, koska nopea kehitysvauhtia edellyttää jatkuvaa kouluttautumista. Toisaalta tietojenkäsittelyteoria luo perustaa uusille innovaatioille.

Laskennallinen logiikka on eräs keskeisiä tietojenkäsittelyteorian alueita ja logiikkaa on kutsuttu syystä tietotekniikan perusmatematiikaksi, jolla on alalla samanlainen asema kuin differentiaali- ja integraalilaskennalla on monilla muilla insinöoritieteiden alueilla. Logiikka luo pohjan tietokoneiden perustana olevien digitaalipiirien toiminnalle ja niiden suunnittelulle. Logiikalla on keskeinen tehtävä selvitettäessä ongelmien laskennallista vaativuutta ja tietojenkäsittelyn periaatteellisia rajoja. Logiikka on myös tärkeä osa ohjelmointikieliä ja tietokantoja sekä ohjelmistojen määrittely- ja verifiointimenetelmiä. Laskennallinen logiikka on laaja ja vireä tutkimusalue, jolla on kattavat ja syvälliset kytkennät tietojenkäsittelyn teoriaan ja käytäntöön (ks. esim. ACM Transactions on Computational Logic).

Logiikan ja laskennan mallien välinen tiivis yhteys luo puitteet löytää laskennallisen logiikan keinoin uusia vastauksia tietojenkäsittelyn peruskysymykseen: mitä voidaan automatisoida tehokkaasti. Tästä hyvänä esimerkkinä on laskennallisesti vaativiin ongelmiin liittyvästä faasimuutosilmiöstä viime vuosina saadut tutkimustulokset (Nature 400 (1999) 6740, 133-137), jotka pohjautuvat suurelta osalta logiikan perustehtävän, toteutuvuusongelman, laskennallisesta käyttäytymisestä kerättyyn tutkimustietoon. Nämä tulokset ovat johtaneet uusiin algoritmeihin ja sovellutuksiin useilla aloilla.

Kuvaavan esimerkin laskennallisen logiikan uusista sovellutuksista tarjoaa verifiointi, joka liittyy monimutkaisten järjestelmien kehitysprosessin laadunvarmennukseen. Tavoitteena on saavuttaa perinteistä testausta parempi kattavuus luomalla suunnitellusta järjestelmästä laskennallisia malleja jo hyvin varhaisessa vaiheessa suunnittelua ja pyrkiä varmentamaan järjestelmän toimintaa mallien avulla. Verifiointi on kuitenkin laskennallisesti erittäin haastava alue ja sitä on pidetty pitkään laskennallisesti liian vaikeana toteuttaa käytännössä.

1980-lopulla kehitetyt uudet tekniikat Boolen lauseiden käsittelyssä (binääriset päätösdiagrammit) ovat kuitenkin mahdollistaneet logiikkaan perustuvien symbolisten laskennallisten mallien käytön verifioinnissa. Tämä symboliseksi mallintarkastukseksi kutsuttu lähestymistapa yleistyi ensimmäisenä digitaalipiirien suunnittelussa, jossa todettiin 1990-luvun puolivälissä, ettei testaus takaa riittävää laatutasoa piirien yhä monimutkaistuessa. Niinpä suurimmat piiri- ja prosessorivalmistajat ovat panostaneet merkittävästi viime vuosina verifiointimenetelmien käyttöönottoon. Uudet menetelmät, joita on kehitetty mm. faasimuutosilmiöstä saatujen tulosten perusteella, ovat entisestään laajentaneet symbolisen mallintarkastuksen soveltuvuusaluetta.

Tämän kehityksen rinnalla on tapahtunut erittäin ripeää laitteistokehitystä, joka on nostanut tietokoneiden laskentatehoa lähes häkellyttävän nopeasti. Vauhdikkaan menetelmä- ja laitteistokehityksen ansiosta olemme tilanteessa, jossa tehokkaan laskettavuuden rajat laajenevat jatkuvasti ja yhä uusia mielenkiintoisia alueita tulee laskennallisten tarkastelujen piiriin.

Tietotekniikka on jo nyt noussut keskeiseksi kilpailutekijäksi lähes kaikilla teollisuuden aloilla ja sen yhteiskunnallinen merkitys on entisestään korostumassa siirryttäessä kohti tietoyhteiskuntaan. Kilpailu tietotekniikassa on globaalia ja kehitysvauhti erittäin nopeaa. Pitkällä tähtäimellä mukana pysyminen edellyttää kykyä hyödyntää uusimpia menetelmiä ja tutkimustuloksia. Tämä taas tarkoittaa sitä, että tarvitaan huippuluokan tutkimusta ja siihen liittyvää opetusta.